singletons-base-3.2: tests/compile-and-dump/Singletons/AsPattern.golden
Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| maybePlus :: Maybe Nat -> Maybe Nat
maybePlus (Just n) = Just (plus (Succ Zero) n)
maybePlus p@Nothing = p
bar :: Maybe Nat -> Maybe Nat
bar x@(Just _) = x
bar Nothing = Nothing
baz_ :: Maybe Baz -> Maybe Baz
baz_ p@Nothing = p
baz_ p@(Just (Baz _ _ _)) = p
tup :: (Nat, Nat) -> (Nat, Nat)
tup p@(_, _) = p
foo :: [Nat] -> [Nat]
foo p@[] = p
foo p@[_] = p
foo p@(_ : _ : _) = p
data Baz = Baz Nat Nat Nat |]
======>
maybePlus :: Maybe Nat -> Maybe Nat
maybePlus (Just n) = Just (plus (Succ Zero) n)
maybePlus p@Nothing = p
bar :: Maybe Nat -> Maybe Nat
bar x@(Just _) = x
bar Nothing = Nothing
data Baz = Baz Nat Nat Nat
baz_ :: Maybe Baz -> Maybe Baz
baz_ p@Nothing = p
baz_ p@(Just (Baz _ _ _)) = p
tup :: (Nat, Nat) -> (Nat, Nat)
tup p@(_, _) = p
foo :: [Nat] -> [Nat]
foo p@[] = p
foo p@[_] = p
foo p@(_ : (_ : _)) = p
type BazSym0 :: (~>) Nat ((~>) Nat ((~>) Nat Baz))
data BazSym0 :: (~>) Nat ((~>) Nat ((~>) Nat Baz))
where
BazSym0KindInference :: SameKind (Apply BazSym0 arg) (BazSym1 arg) =>
BazSym0 a0123456789876543210
type instance Apply BazSym0 a0123456789876543210 = BazSym1 a0123456789876543210
instance SuppressUnusedWarnings BazSym0 where
suppressUnusedWarnings = snd ((,) BazSym0KindInference ())
type BazSym1 :: Nat -> (~>) Nat ((~>) Nat Baz)
data BazSym1 (a0123456789876543210 :: Nat) :: (~>) Nat ((~>) Nat Baz)
where
BazSym1KindInference :: SameKind (Apply (BazSym1 a0123456789876543210) arg) (BazSym2 a0123456789876543210 arg) =>
BazSym1 a0123456789876543210 a0123456789876543210
type instance Apply (BazSym1 a0123456789876543210) a0123456789876543210 = BazSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (BazSym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) BazSym1KindInference ())
type BazSym2 :: Nat -> Nat -> (~>) Nat Baz
data BazSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: (~>) Nat Baz
where
BazSym2KindInference :: SameKind (Apply (BazSym2 a0123456789876543210 a0123456789876543210) arg) (BazSym3 a0123456789876543210 a0123456789876543210 arg) =>
BazSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (BazSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = Baz a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (BazSym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) BazSym2KindInference ())
type BazSym3 :: Nat -> Nat -> Nat -> Baz
type family BazSym3 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Baz where
BazSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = Baz a0123456789876543210 a0123456789876543210 a0123456789876543210
type family Let0123456789876543210PSym0 where
Let0123456789876543210PSym0 = Let0123456789876543210P
type family Let0123456789876543210P where
Let0123456789876543210P = NilSym0
data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym0KindInference :: SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
type instance Apply Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym0KindInference ())
type family Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 where
Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210
type family Let0123456789876543210P wild_0123456789876543210 where
Let0123456789876543210P wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) NilSym0
data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym0KindInference :: SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
type instance Apply Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym0KindInference ())
data Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym1KindInference :: SameKind (Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 arg) =>
Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
type instance Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym1KindInference ())
data Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym2KindInference :: SameKind (Apply (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 arg) =>
Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
type instance Apply (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym2KindInference ())
type family Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 where
Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) (Apply (Apply (:@#@$) wild_0123456789876543210) wild_0123456789876543210)
data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym0KindInference :: SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
type instance Apply Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym0KindInference ())
data Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym1KindInference :: SameKind (Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 arg) =>
Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
type instance Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym1KindInference ())
type family Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 where
Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply Tuple2Sym0 wild_0123456789876543210) wild_0123456789876543210
type family Let0123456789876543210PSym0 where
Let0123456789876543210PSym0 = Let0123456789876543210P
type family Let0123456789876543210P where
Let0123456789876543210P = NothingSym0
data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym0KindInference :: SameKind (Apply Let0123456789876543210PSym0 arg) (Let0123456789876543210PSym1 arg) =>
Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210
type instance Apply Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym0KindInference ())
data Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym1KindInference :: SameKind (Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 arg) =>
Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
type instance Apply (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym1KindInference ())
data Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
where
Let0123456789876543210PSym2KindInference :: SameKind (Apply (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) arg) (Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 arg) =>
Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
type instance Apply (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210PSym2KindInference ())
type family Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where
Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 where
Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 = Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789876543210) wild_0123456789876543210) wild_0123456789876543210)
data Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210
where
Let0123456789876543210XSym0KindInference :: SameKind (Apply Let0123456789876543210XSym0 arg) (Let0123456789876543210XSym1 arg) =>
Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210
type instance Apply Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210XSym0 where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210XSym0KindInference ())
type family Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 where
Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210
type family Let0123456789876543210X wild_0123456789876543210 where
Let0123456789876543210X wild_0123456789876543210 = Apply JustSym0 wild_0123456789876543210
type family Let0123456789876543210PSym0 where
Let0123456789876543210PSym0 = Let0123456789876543210P
type family Let0123456789876543210P where
Let0123456789876543210P = NothingSym0
type FooSym0 :: (~>) [Nat] [Nat]
data FooSym0 :: (~>) [Nat] [Nat]
where
FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
FooSym0 a0123456789876543210
type instance Apply FooSym0 a0123456789876543210 = Foo a0123456789876543210
instance SuppressUnusedWarnings FooSym0 where
suppressUnusedWarnings = snd ((,) FooSym0KindInference ())
type FooSym1 :: [Nat] -> [Nat]
type family FooSym1 (a0123456789876543210 :: [Nat]) :: [Nat] where
FooSym1 a0123456789876543210 = Foo a0123456789876543210
type TupSym0 :: (~>) (Nat, Nat) (Nat, Nat)
data TupSym0 :: (~>) (Nat, Nat) (Nat, Nat)
where
TupSym0KindInference :: SameKind (Apply TupSym0 arg) (TupSym1 arg) =>
TupSym0 a0123456789876543210
type instance Apply TupSym0 a0123456789876543210 = Tup a0123456789876543210
instance SuppressUnusedWarnings TupSym0 where
suppressUnusedWarnings = snd ((,) TupSym0KindInference ())
type TupSym1 :: (Nat, Nat) -> (Nat, Nat)
type family TupSym1 (a0123456789876543210 :: (Nat, Nat)) :: (Nat,
Nat) where
TupSym1 a0123456789876543210 = Tup a0123456789876543210
type Baz_Sym0 :: (~>) (Maybe Baz) (Maybe Baz)
data Baz_Sym0 :: (~>) (Maybe Baz) (Maybe Baz)
where
Baz_Sym0KindInference :: SameKind (Apply Baz_Sym0 arg) (Baz_Sym1 arg) =>
Baz_Sym0 a0123456789876543210
type instance Apply Baz_Sym0 a0123456789876543210 = Baz_ a0123456789876543210
instance SuppressUnusedWarnings Baz_Sym0 where
suppressUnusedWarnings = snd ((,) Baz_Sym0KindInference ())
type Baz_Sym1 :: Maybe Baz -> Maybe Baz
type family Baz_Sym1 (a0123456789876543210 :: Maybe Baz) :: Maybe Baz where
Baz_Sym1 a0123456789876543210 = Baz_ a0123456789876543210
type BarSym0 :: (~>) (Maybe Nat) (Maybe Nat)
data BarSym0 :: (~>) (Maybe Nat) (Maybe Nat)
where
BarSym0KindInference :: SameKind (Apply BarSym0 arg) (BarSym1 arg) =>
BarSym0 a0123456789876543210
type instance Apply BarSym0 a0123456789876543210 = Bar a0123456789876543210
instance SuppressUnusedWarnings BarSym0 where
suppressUnusedWarnings = snd ((,) BarSym0KindInference ())
type BarSym1 :: Maybe Nat -> Maybe Nat
type family BarSym1 (a0123456789876543210 :: Maybe Nat) :: Maybe Nat where
BarSym1 a0123456789876543210 = Bar a0123456789876543210
type MaybePlusSym0 :: (~>) (Maybe Nat) (Maybe Nat)
data MaybePlusSym0 :: (~>) (Maybe Nat) (Maybe Nat)
where
MaybePlusSym0KindInference :: SameKind (Apply MaybePlusSym0 arg) (MaybePlusSym1 arg) =>
MaybePlusSym0 a0123456789876543210
type instance Apply MaybePlusSym0 a0123456789876543210 = MaybePlus a0123456789876543210
instance SuppressUnusedWarnings MaybePlusSym0 where
suppressUnusedWarnings = snd ((,) MaybePlusSym0KindInference ())
type MaybePlusSym1 :: Maybe Nat -> Maybe Nat
type family MaybePlusSym1 (a0123456789876543210 :: Maybe Nat) :: Maybe Nat where
MaybePlusSym1 a0123456789876543210 = MaybePlus a0123456789876543210
type Foo :: [Nat] -> [Nat]
type family Foo (a :: [Nat]) :: [Nat] where
Foo '[] = Let0123456789876543210PSym0
Foo '[wild_0123456789876543210] = Let0123456789876543210PSym1 wild_0123456789876543210
Foo ('(:) wild_0123456789876543210 ('(:) wild_0123456789876543210 wild_0123456789876543210)) = Let0123456789876543210PSym3 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210
type Tup :: (Nat, Nat) -> (Nat, Nat)
type family Tup (a :: (Nat, Nat)) :: (Nat, Nat) where
Tup '(wild_0123456789876543210,
wild_0123456789876543210) = Let0123456789876543210PSym2 wild_0123456789876543210 wild_0123456789876543210
type Baz_ :: Maybe Baz -> Maybe Baz
type family Baz_ (a :: Maybe Baz) :: Maybe Baz where
Baz_ 'Nothing = Let0123456789876543210PSym0
Baz_ ('Just (Baz wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)) = Let0123456789876543210PSym3 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210
type Bar :: Maybe Nat -> Maybe Nat
type family Bar (a :: Maybe Nat) :: Maybe Nat where
Bar ('Just wild_0123456789876543210) = Let0123456789876543210XSym1 wild_0123456789876543210
Bar 'Nothing = NothingSym0
type MaybePlus :: Maybe Nat -> Maybe Nat
type family MaybePlus (a :: Maybe Nat) :: Maybe Nat where
MaybePlus ('Just n) = Apply JustSym0 (Apply (Apply PlusSym0 (Apply SuccSym0 ZeroSym0)) n)
MaybePlus 'Nothing = Let0123456789876543210PSym0
sFoo ::
(forall (t :: [Nat]).
Sing t -> Sing (Apply FooSym0 t :: [Nat]) :: Type)
sTup ::
(forall (t :: (Nat, Nat)).
Sing t -> Sing (Apply TupSym0 t :: (Nat, Nat)) :: Type)
sBaz_ ::
(forall (t :: Maybe Baz).
Sing t -> Sing (Apply Baz_Sym0 t :: Maybe Baz) :: Type)
sBar ::
(forall (t :: Maybe Nat).
Sing t -> Sing (Apply BarSym0 t :: Maybe Nat) :: Type)
sMaybePlus ::
(forall (t :: Maybe Nat).
Sing t -> Sing (Apply MaybePlusSym0 t :: Maybe Nat) :: Type)
sFoo SNil
= let
sP :: Sing @_ Let0123456789876543210PSym0
sP = SNil
in sP
sFoo
(SCons (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
SNil)
= let
sP ::
Sing @_ (Let0123456789876543210PSym1 wild_0123456789876543210)
sP
= applySing
(applySing (singFun2 @(:@#@$) SCons) sWild_0123456789876543210)
SNil
in sP
sFoo
(SCons (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
(SCons (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
(sWild_0123456789876543210 :: Sing wild_0123456789876543210)))
= let
sP ::
Sing @_ (Let0123456789876543210PSym3 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)
sP
= applySing
(applySing (singFun2 @(:@#@$) SCons) sWild_0123456789876543210)
(applySing
(applySing (singFun2 @(:@#@$) SCons) sWild_0123456789876543210)
sWild_0123456789876543210)
in sP
sTup
(STuple2 (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
(sWild_0123456789876543210 :: Sing wild_0123456789876543210))
= let
sP ::
Sing @_ (Let0123456789876543210PSym2 wild_0123456789876543210 wild_0123456789876543210)
sP
= applySing
(applySing
(singFun2 @Tuple2Sym0 STuple2) sWild_0123456789876543210)
sWild_0123456789876543210
in sP
sBaz_ SNothing
= let
sP :: Sing @_ Let0123456789876543210PSym0
sP = SNothing
in sP
sBaz_
(SJust (SBaz (sWild_0123456789876543210 :: Sing wild_0123456789876543210)
(sWild_0123456789876543210 :: Sing wild_0123456789876543210)
(sWild_0123456789876543210 :: Sing wild_0123456789876543210)))
= let
sP ::
Sing @_ (Let0123456789876543210PSym3 wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210)
sP
= applySing
(singFun1 @JustSym0 SJust)
(applySing
(applySing
(applySing (singFun3 @BazSym0 SBaz) sWild_0123456789876543210)
sWild_0123456789876543210)
sWild_0123456789876543210)
in sP
sBar
(SJust (sWild_0123456789876543210 :: Sing wild_0123456789876543210))
= let
sX ::
Sing @_ (Let0123456789876543210XSym1 wild_0123456789876543210)
sX = applySing (singFun1 @JustSym0 SJust) sWild_0123456789876543210
in sX
sBar SNothing = SNothing
sMaybePlus (SJust (sN :: Sing n))
= applySing
(singFun1 @JustSym0 SJust)
(applySing
(applySing
(singFun2 @PlusSym0 sPlus)
(applySing (singFun1 @SuccSym0 SSucc) SZero))
sN)
sMaybePlus SNothing
= let
sP :: Sing @_ Let0123456789876543210PSym0
sP = SNothing
in sP
instance SingI (FooSym0 :: (~>) [Nat] [Nat]) where
sing = singFun1 @FooSym0 sFoo
instance SingI (TupSym0 :: (~>) (Nat, Nat) (Nat, Nat)) where
sing = singFun1 @TupSym0 sTup
instance SingI (Baz_Sym0 :: (~>) (Maybe Baz) (Maybe Baz)) where
sing = singFun1 @Baz_Sym0 sBaz_
instance SingI (BarSym0 :: (~>) (Maybe Nat) (Maybe Nat)) where
sing = singFun1 @BarSym0 sBar
instance SingI (MaybePlusSym0 :: (~>) (Maybe Nat) (Maybe Nat)) where
sing = singFun1 @MaybePlusSym0 sMaybePlus
data SBaz :: Baz -> Type
where
SBaz :: forall (n :: Nat) (n :: Nat) (n :: Nat).
(Sing n) -> (Sing n) -> (Sing n) -> SBaz (Baz n n n :: Baz)
type instance Sing @Baz = SBaz
instance SingKind Baz where
type Demote Baz = Baz
fromSing (SBaz b b b) = Baz (fromSing b) (fromSing b) (fromSing b)
toSing (Baz (b :: Demote Nat) (b :: Demote Nat) (b :: Demote Nat))
= case
(,,)
(toSing b :: SomeSing Nat) (toSing b :: SomeSing Nat)
(toSing b :: SomeSing Nat)
of
(,,) (SomeSing c) (SomeSing c) (SomeSing c)
-> SomeSing (SBaz c c c)
instance (SingI n, SingI n, SingI n) =>
SingI (Baz (n :: Nat) (n :: Nat) (n :: Nat)) where
sing = SBaz sing sing sing
instance (SingI n, SingI n) =>
SingI1 (Baz (n :: Nat) (n :: Nat)) where
liftSing = SBaz sing sing
instance SingI n => SingI2 (Baz (n :: Nat)) where
liftSing2 = SBaz sing
instance SingI (BazSym0 :: (~>) Nat ((~>) Nat ((~>) Nat Baz))) where
sing = singFun3 @BazSym0 SBaz
instance SingI d =>
SingI (BazSym1 (d :: Nat) :: (~>) Nat ((~>) Nat Baz)) where
sing = singFun2 @(BazSym1 (d :: Nat)) (SBaz (sing @d))
instance SingI1 (BazSym1 :: Nat -> (~>) Nat ((~>) Nat Baz)) where
liftSing (s :: Sing (d :: Nat))
= singFun2 @(BazSym1 (d :: Nat)) (SBaz s)
instance (SingI d, SingI d) =>
SingI (BazSym2 (d :: Nat) (d :: Nat) :: (~>) Nat Baz) where
sing
= singFun1
@(BazSym2 (d :: Nat) (d :: Nat)) (SBaz (sing @d) (sing @d))
instance SingI d =>
SingI1 (BazSym2 (d :: Nat) :: Nat -> (~>) Nat Baz) where
liftSing (s :: Sing (d :: Nat))
= singFun1 @(BazSym2 (d :: Nat) (d :: Nat)) (SBaz (sing @d) s)
instance SingI2 (BazSym2 :: Nat -> Nat -> (~>) Nat Baz) where
liftSing2 (s :: Sing (d :: Nat)) (s :: Sing (d :: Nat))
= singFun1 @(BazSym2 (d :: Nat) (d :: Nat)) (SBaz s s)