singletons-2.7: 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 a0123456789876543210
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 a0123456789876543210
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 a0123456789876543210 a0123456789876543210
where
BazSym2KindInference :: SameKind (Apply (BazSym2 a0123456789876543210 a0123456789876543210) arg) (BazSym3 a0123456789876543210 a0123456789876543210 arg) =>
BazSym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (BazSym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = BazSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (BazSym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) BazSym2KindInference) ())
type BazSym3 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
Baz a0123456789876543210 a0123456789876543210 a0123456789876543210 :: Baz
type 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 = Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210PSym0 where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210PSym0KindInference) ())
type 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 = Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210PSym2KindInference) ())
type 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 = Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210PSym1KindInference) ())
type 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 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 = Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210PSym2KindInference) ())
type 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 = Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210XSym0 where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210XSym0KindInference) ())
type Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 =
Let0123456789876543210X wild_01234567898765432100123456789876543210
type family Let0123456789876543210X wild_0123456789876543210 where
Let0123456789876543210X wild_0123456789876543210 = Apply JustSym0 wild_0123456789876543210
type Let0123456789876543210PSym0 = Let0123456789876543210P
type family Let0123456789876543210P where
Let0123456789876543210P = NothingSym0
type FooSym0 :: (~>) [Nat] [Nat]
data FooSym0 a0123456789876543210
where
FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
FooSym0 a0123456789876543210
type instance Apply FooSym0 a0123456789876543210 = FooSym1 a0123456789876543210
instance SuppressUnusedWarnings FooSym0 where
suppressUnusedWarnings = snd (((,) FooSym0KindInference) ())
type FooSym1 (a0123456789876543210 :: [Nat]) =
Foo a0123456789876543210 :: [Nat]
type TupSym0 :: (~>) (Nat, Nat) (Nat, Nat)
data TupSym0 a0123456789876543210
where
TupSym0KindInference :: SameKind (Apply TupSym0 arg) (TupSym1 arg) =>
TupSym0 a0123456789876543210
type instance Apply TupSym0 a0123456789876543210 = TupSym1 a0123456789876543210
instance SuppressUnusedWarnings TupSym0 where
suppressUnusedWarnings = snd (((,) TupSym0KindInference) ())
type TupSym1 (a0123456789876543210 :: (Nat, Nat)) =
Tup a0123456789876543210 :: (Nat, Nat)
type Baz_Sym0 :: (~>) (Maybe Baz) (Maybe Baz)
data Baz_Sym0 a0123456789876543210
where
Baz_Sym0KindInference :: SameKind (Apply Baz_Sym0 arg) (Baz_Sym1 arg) =>
Baz_Sym0 a0123456789876543210
type instance Apply Baz_Sym0 a0123456789876543210 = Baz_Sym1 a0123456789876543210
instance SuppressUnusedWarnings Baz_Sym0 where
suppressUnusedWarnings = snd (((,) Baz_Sym0KindInference) ())
type Baz_Sym1 (a0123456789876543210 :: Maybe Baz) =
Baz_ a0123456789876543210 :: Maybe Baz
type BarSym0 :: (~>) (Maybe Nat) (Maybe Nat)
data BarSym0 a0123456789876543210
where
BarSym0KindInference :: SameKind (Apply BarSym0 arg) (BarSym1 arg) =>
BarSym0 a0123456789876543210
type instance Apply BarSym0 a0123456789876543210 = BarSym1 a0123456789876543210
instance SuppressUnusedWarnings BarSym0 where
suppressUnusedWarnings = snd (((,) BarSym0KindInference) ())
type BarSym1 (a0123456789876543210 :: Maybe Nat) =
Bar a0123456789876543210 :: Maybe Nat
type MaybePlusSym0 :: (~>) (Maybe Nat) (Maybe Nat)
data MaybePlusSym0 a0123456789876543210
where
MaybePlusSym0KindInference :: SameKind (Apply MaybePlusSym0 arg) (MaybePlusSym1 arg) =>
MaybePlusSym0 a0123456789876543210
type instance Apply MaybePlusSym0 a0123456789876543210 = MaybePlusSym1 a0123456789876543210
instance SuppressUnusedWarnings MaybePlusSym0 where
suppressUnusedWarnings = snd (((,) MaybePlusSym0KindInference) ())
type MaybePlusSym1 (a0123456789876543210 :: Maybe Nat) =
MaybePlus a0123456789876543210 :: Maybe Nat
type Foo :: [Nat] -> [Nat]
type family Foo a 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 where
Tup '(wild_0123456789876543210,
wild_0123456789876543210) = Let0123456789876543210PSym2 wild_0123456789876543210 wild_0123456789876543210
type Baz_ :: Maybe Baz -> Maybe Baz
type family Baz_ a 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 where
Bar ('Just wild_0123456789876543210) = Let0123456789876543210XSym1 wild_0123456789876543210
Bar 'Nothing = NothingSym0
type MaybePlus :: Maybe Nat -> Maybe Nat
type family MaybePlus a 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])
sTup ::
forall (t :: (Nat, Nat)).
Sing t -> Sing (Apply TupSym0 t :: (Nat, Nat))
sBaz_ ::
forall (t :: Maybe Baz).
Sing t -> Sing (Apply Baz_Sym0 t :: Maybe Baz)
sBar ::
forall (t :: Maybe Nat).
Sing t -> Sing (Apply BarSym0 t :: Maybe Nat)
sMaybePlus ::
forall (t :: Maybe Nat).
Sing t -> Sing (Apply MaybePlusSym0 t :: Maybe Nat)
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 -> GHC.Types.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 (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 (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))