singletons-base-3.5: tests/compile-and-dump/Singletons/T183.golden
Singletons/T183.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| f1 (x :: Maybe Bool) = (x :: Maybe Bool)
f2 (x :: Maybe a) = (x :: Maybe a)
f3 (Just a :: Maybe Bool) = "hi"
g x = case Just x of (Just y :: Maybe Bool) -> (y :: Bool)
foo1 :: Maybe a -> a
foo1 (Just x :: Maybe a) = (x :: a)
foo2, foo3 :: forall a. Maybe a -> a
foo2 (Just x :: Maybe a) = (x :: a)
foo3 (Just x) = (x :: a)
foo4 :: (a, b) -> (b, a)
foo4 = \ (x :: a, y :: b) -> (y :: b, x :: a)
foo5, foo6 :: Maybe (Maybe a) -> Maybe (Maybe a)
foo5 (Just (Just (x :: a) :: Maybe a) :: Maybe (Maybe a))
= Just (Just (x :: a) :: Maybe a) :: Maybe (Maybe a)
foo6 (Just x :: Maybe (Maybe a))
= case x :: Maybe a of
(Just (y :: a) :: Maybe a) -> Just (Just (y :: a) :: Maybe a)
foo7 :: a -> b -> a
foo7 (x :: a) (_ :: b) = (x :: a)
foo8 :: forall a. Maybe a -> Maybe a
foo8 x@(Just (_ :: a) :: Maybe a) = x
foo8 x@(Nothing :: Maybe a) = x
foo9 :: a -> a
foo9 (x :: a)
= let
g :: a -> b -> a
g y _ = y
in g x () |]
======>
f1 (x :: Maybe Bool) = x :: Maybe Bool
f2 (x :: Maybe a) = x :: Maybe a
f3 (Just a :: Maybe Bool) = "hi"
g x = case Just x of (Just y :: Maybe Bool) -> y :: Bool
foo1 :: Maybe a -> a
foo1 (Just x :: Maybe a) = x :: a
foo2 :: forall a. Maybe a -> a
foo3 :: forall a. Maybe a -> a
foo2 (Just x :: Maybe a) = x :: a
foo3 (Just x) = x :: a
foo4 :: (a, b) -> (b, a)
foo4 = \ (x :: a, y :: b) -> (y :: b, x :: a)
foo5 :: Maybe (Maybe a) -> Maybe (Maybe a)
foo6 :: Maybe (Maybe a) -> Maybe (Maybe a)
foo5 (Just (Just (x :: a) :: Maybe a) :: Maybe (Maybe a))
= Just (Just (x :: a) :: Maybe a) :: Maybe (Maybe a)
foo6 (Just x :: Maybe (Maybe a))
= case x :: Maybe a of
(Just (y :: a) :: Maybe a) -> Just (Just (y :: a) :: Maybe a)
foo7 :: a -> b -> a
foo7 (x :: a) (_ :: b) = x :: a
foo8 :: forall a. Maybe a -> Maybe a
foo8 x@(Just (_ :: a) :: Maybe a) = x
foo8 x@(Nothing :: Maybe a) = x
foo9 :: a -> a
foo9 (x :: a)
= let
g :: a -> b -> a
g y _ = y
in g x ()
data Let0123456789876543210GSym0 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) :: (~>) a0123456789876543210 ((~>) b0123456789876543210 a0123456789876543210)
where
Let0123456789876543210GSym0KindInference :: SameKind (Apply (Let0123456789876543210GSym0 a0123456789876543210 x0123456789876543210) arg) (Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 arg) =>
Let0123456789876543210GSym0 a0123456789876543210 x0123456789876543210 a0123456789876543210
type instance Apply @a0123456789876543210 @((~>) b0123456789876543210 a0123456789876543210) (Let0123456789876543210GSym0 a0123456789876543210 x0123456789876543210) a0123456789876543210 = Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210GSym0 a0123456789876543210 x0123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210GSym0KindInference ())
data Let0123456789876543210GSym1 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: a0123456789876543210) :: (~>) b0123456789876543210 a0123456789876543210
where
Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210 a0123456789876543210 arg) =>
Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply @b0123456789876543210 @a0123456789876543210 (Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 a0123456789876543210) a0123456789876543210 = Let0123456789876543210G a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) Let0123456789876543210GSym1KindInference ())
type family Let0123456789876543210GSym2 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: a0123456789876543210 where
Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210G a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210
type family Let0123456789876543210G a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (a :: a0123456789876543210) (a :: b) :: a0123456789876543210 where
Let0123456789876543210G a x y _ = y
type family Let0123456789876543210XSym0 a0123456789876543210 (wild_01234567898765432100123456789876543210 :: a0123456789876543210) where
Let0123456789876543210XSym0 a0123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210X a0123456789876543210 wild_01234567898765432100123456789876543210
type family Let0123456789876543210X a0123456789876543210 (wild_01234567898765432100123456789876543210 :: a0123456789876543210) where
Let0123456789876543210X a wild_0123456789876543210 = Apply JustSym0 (wild_0123456789876543210 :: a) :: Maybe a
type family Let0123456789876543210XSym0 a0123456789876543210 where
Let0123456789876543210XSym0 a0123456789876543210 = Let0123456789876543210X a0123456789876543210
type family Let0123456789876543210X a0123456789876543210 where
Let0123456789876543210X a = NothingSym0 :: Maybe a
type family LamCases_0123456789876543210 a0123456789876543210 x0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 a x ('Just (y :: a) :: Maybe a) = Apply JustSym0 (Apply JustSym0 (y :: a) :: Maybe a)
data LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210) arg) (LamCases_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 (a_01234567898765432100123456789876543210 :: (a0123456789876543210,
b0123456789876543210)) a_0123456789876543210 where
LamCases_0123456789876543210 a_0123456789876543210 '(x :: a,
y :: b) = Apply (Apply Tuple2Sym0 (y :: b)) (x :: a)
data LamCases_0123456789876543210Sym0 (a_01234567898765432100123456789876543210 :: (a0123456789876543210,
b0123456789876543210)) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210) arg) (LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 (a_01234567898765432100123456789876543210 :: (a0123456789876543210,
b0123456789876543210)) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 x0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 x ('Just y :: Maybe Bool) = y :: Bool
data LamCases_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 x0123456789876543210) arg) (LamCases_0123456789876543210Sym1 x0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 x0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 x0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type Foo9Sym0 :: (~>) a a
data Foo9Sym0 :: (~>) a a
where
Foo9Sym0KindInference :: SameKind (Apply Foo9Sym0 arg) (Foo9Sym1 arg) =>
Foo9Sym0 a0123456789876543210
type instance Apply @a @a Foo9Sym0 a0123456789876543210 = Foo9 a0123456789876543210
instance SuppressUnusedWarnings Foo9Sym0 where
suppressUnusedWarnings = snd ((,) Foo9Sym0KindInference ())
type Foo9Sym1 :: a -> a
type family Foo9Sym1 @a (a0123456789876543210 :: a) :: a where
Foo9Sym1 a0123456789876543210 = Foo9 a0123456789876543210
type Foo8Sym0 :: forall a. (~>) (Maybe a) (Maybe a)
data Foo8Sym0 :: (~>) (Maybe a) (Maybe a)
where
Foo8Sym0KindInference :: SameKind (Apply Foo8Sym0 arg) (Foo8Sym1 arg) =>
Foo8Sym0 a0123456789876543210
type instance Apply @(Maybe a) @(Maybe a) Foo8Sym0 a0123456789876543210 = Foo8 a0123456789876543210
instance SuppressUnusedWarnings Foo8Sym0 where
suppressUnusedWarnings = snd ((,) Foo8Sym0KindInference ())
type Foo8Sym1 :: forall a. Maybe a -> Maybe a
type family Foo8Sym1 @a (a0123456789876543210 :: Maybe a) :: Maybe a where
Foo8Sym1 a0123456789876543210 = Foo8 a0123456789876543210
type Foo7Sym0 :: (~>) a ((~>) b a)
data Foo7Sym0 :: (~>) a ((~>) b a)
where
Foo7Sym0KindInference :: SameKind (Apply Foo7Sym0 arg) (Foo7Sym1 arg) =>
Foo7Sym0 a0123456789876543210
type instance Apply @a @((~>) b a) Foo7Sym0 a0123456789876543210 = Foo7Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo7Sym0 where
suppressUnusedWarnings = snd ((,) Foo7Sym0KindInference ())
type Foo7Sym1 :: a -> (~>) b a
data Foo7Sym1 (a0123456789876543210 :: a) :: (~>) b a
where
Foo7Sym1KindInference :: SameKind (Apply (Foo7Sym1 a0123456789876543210) arg) (Foo7Sym2 a0123456789876543210 arg) =>
Foo7Sym1 a0123456789876543210 a0123456789876543210
type instance Apply @b @a (Foo7Sym1 a0123456789876543210) a0123456789876543210 = Foo7 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Foo7Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd ((,) Foo7Sym1KindInference ())
type Foo7Sym2 :: a -> b -> a
type family Foo7Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where
Foo7Sym2 a0123456789876543210 a0123456789876543210 = Foo7 a0123456789876543210 a0123456789876543210
type Foo6Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a))
data Foo6Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a))
where
Foo6Sym0KindInference :: SameKind (Apply Foo6Sym0 arg) (Foo6Sym1 arg) =>
Foo6Sym0 a0123456789876543210
type instance Apply @(Maybe (Maybe a)) @(Maybe (Maybe a)) Foo6Sym0 a0123456789876543210 = Foo6 a0123456789876543210
instance SuppressUnusedWarnings Foo6Sym0 where
suppressUnusedWarnings = snd ((,) Foo6Sym0KindInference ())
type Foo6Sym1 :: Maybe (Maybe a) -> Maybe (Maybe a)
type family Foo6Sym1 @a (a0123456789876543210 :: Maybe (Maybe a)) :: Maybe (Maybe a) where
Foo6Sym1 a0123456789876543210 = Foo6 a0123456789876543210
type Foo5Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a))
data Foo5Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a))
where
Foo5Sym0KindInference :: SameKind (Apply Foo5Sym0 arg) (Foo5Sym1 arg) =>
Foo5Sym0 a0123456789876543210
type instance Apply @(Maybe (Maybe a)) @(Maybe (Maybe a)) Foo5Sym0 a0123456789876543210 = Foo5 a0123456789876543210
instance SuppressUnusedWarnings Foo5Sym0 where
suppressUnusedWarnings = snd ((,) Foo5Sym0KindInference ())
type Foo5Sym1 :: Maybe (Maybe a) -> Maybe (Maybe a)
type family Foo5Sym1 @a (a0123456789876543210 :: Maybe (Maybe a)) :: Maybe (Maybe a) where
Foo5Sym1 a0123456789876543210 = Foo5 a0123456789876543210
type Foo4Sym0 :: (~>) (a, b) (b, a)
data Foo4Sym0 :: (~>) (a, b) (b, a)
where
Foo4Sym0KindInference :: SameKind (Apply Foo4Sym0 arg) (Foo4Sym1 arg) =>
Foo4Sym0 a0123456789876543210
type instance Apply @(a, b) @(b,
a) Foo4Sym0 a0123456789876543210 = Foo4 a0123456789876543210
instance SuppressUnusedWarnings Foo4Sym0 where
suppressUnusedWarnings = snd ((,) Foo4Sym0KindInference ())
type Foo4Sym1 :: (a, b) -> (b, a)
type family Foo4Sym1 @a @b (a0123456789876543210 :: (a, b)) :: (b,
a) where
Foo4Sym1 a0123456789876543210 = Foo4 a0123456789876543210
type Foo3Sym0 :: forall a. (~>) (Maybe a) a
data Foo3Sym0 :: (~>) (Maybe a) a
where
Foo3Sym0KindInference :: SameKind (Apply Foo3Sym0 arg) (Foo3Sym1 arg) =>
Foo3Sym0 a0123456789876543210
type instance Apply @(Maybe a) @a Foo3Sym0 a0123456789876543210 = Foo3 a0123456789876543210
instance SuppressUnusedWarnings Foo3Sym0 where
suppressUnusedWarnings = snd ((,) Foo3Sym0KindInference ())
type Foo3Sym1 :: forall a. Maybe a -> a
type family Foo3Sym1 @a (a0123456789876543210 :: Maybe a) :: a where
Foo3Sym1 a0123456789876543210 = Foo3 a0123456789876543210
type Foo2Sym0 :: forall a. (~>) (Maybe a) a
data Foo2Sym0 :: (~>) (Maybe a) a
where
Foo2Sym0KindInference :: SameKind (Apply Foo2Sym0 arg) (Foo2Sym1 arg) =>
Foo2Sym0 a0123456789876543210
type instance Apply @(Maybe a) @a Foo2Sym0 a0123456789876543210 = Foo2 a0123456789876543210
instance SuppressUnusedWarnings Foo2Sym0 where
suppressUnusedWarnings = snd ((,) Foo2Sym0KindInference ())
type Foo2Sym1 :: forall a. Maybe a -> a
type family Foo2Sym1 @a (a0123456789876543210 :: Maybe a) :: a where
Foo2Sym1 a0123456789876543210 = Foo2 a0123456789876543210
type Foo1Sym0 :: (~>) (Maybe a) a
data Foo1Sym0 :: (~>) (Maybe a) a
where
Foo1Sym0KindInference :: SameKind (Apply Foo1Sym0 arg) (Foo1Sym1 arg) =>
Foo1Sym0 a0123456789876543210
type instance Apply @(Maybe a) @a Foo1Sym0 a0123456789876543210 = Foo1 a0123456789876543210
instance SuppressUnusedWarnings Foo1Sym0 where
suppressUnusedWarnings = snd ((,) Foo1Sym0KindInference ())
type Foo1Sym1 :: Maybe a -> a
type family Foo1Sym1 @a (a0123456789876543210 :: Maybe a) :: a where
Foo1Sym1 a0123456789876543210 = Foo1 a0123456789876543210
data GSym0 a0123456789876543210
where
GSym0KindInference :: SameKind (Apply GSym0 arg) (GSym1 arg) =>
GSym0 a0123456789876543210
type instance Apply @_ @_ GSym0 a0123456789876543210 = G a0123456789876543210
instance SuppressUnusedWarnings GSym0 where
suppressUnusedWarnings = snd ((,) GSym0KindInference ())
type family GSym1 a0123456789876543210 where
GSym1 a0123456789876543210 = G a0123456789876543210
data F3Sym0 a0123456789876543210
where
F3Sym0KindInference :: SameKind (Apply F3Sym0 arg) (F3Sym1 arg) =>
F3Sym0 a0123456789876543210
type instance Apply @_ @_ F3Sym0 a0123456789876543210 = F3 a0123456789876543210
instance SuppressUnusedWarnings F3Sym0 where
suppressUnusedWarnings = snd ((,) F3Sym0KindInference ())
type family F3Sym1 a0123456789876543210 where
F3Sym1 a0123456789876543210 = F3 a0123456789876543210
data F2Sym0 a0123456789876543210
where
F2Sym0KindInference :: SameKind (Apply F2Sym0 arg) (F2Sym1 arg) =>
F2Sym0 a0123456789876543210
type instance Apply @_ @_ F2Sym0 a0123456789876543210 = F2 a0123456789876543210
instance SuppressUnusedWarnings F2Sym0 where
suppressUnusedWarnings = snd ((,) F2Sym0KindInference ())
type family F2Sym1 a0123456789876543210 where
F2Sym1 a0123456789876543210 = F2 a0123456789876543210
data F1Sym0 a0123456789876543210
where
F1Sym0KindInference :: SameKind (Apply F1Sym0 arg) (F1Sym1 arg) =>
F1Sym0 a0123456789876543210
type instance Apply @_ @_ F1Sym0 a0123456789876543210 = F1 a0123456789876543210
instance SuppressUnusedWarnings F1Sym0 where
suppressUnusedWarnings = snd ((,) F1Sym0KindInference ())
type family F1Sym1 a0123456789876543210 where
F1Sym1 a0123456789876543210 = F1 a0123456789876543210
type Foo9 :: a -> a
type family Foo9 @a (a :: a) :: a where
Foo9 (x :: a) = Apply (Apply (Let0123456789876543210GSym0 a x) x) Tuple0Sym0
type Foo8 :: forall a. Maybe a -> Maybe a
type family Foo8 @a (a :: Maybe a) :: Maybe a where
Foo8 @a ('Just (wild_0123456789876543210 :: a) :: Maybe a :: Maybe a) = Let0123456789876543210XSym0 a wild_0123456789876543210
Foo8 @a ('Nothing :: Maybe a :: Maybe a) = Let0123456789876543210XSym0 a
type Foo7 :: a -> b -> a
type family Foo7 @a @b (a :: a) (a :: b) :: a where
Foo7 (x :: a) (wild_0123456789876543210 :: b) = x :: a
type Foo6 :: Maybe (Maybe a) -> Maybe (Maybe a)
type family Foo6 @a (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where
Foo6 ('Just x :: Maybe (Maybe a)) = Apply (LamCases_0123456789876543210Sym0 a x) (x :: Maybe a)
type Foo5 :: Maybe (Maybe a) -> Maybe (Maybe a)
type family Foo5 @a (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where
Foo5 ('Just ('Just (x :: a) :: Maybe a) :: Maybe (Maybe a)) = Apply JustSym0 (Apply JustSym0 (x :: a) :: Maybe a) :: Maybe (Maybe a)
type Foo4 :: (a, b) -> (b, a)
type family Foo4 @a @b (a :: (a, b)) :: (b, a) where
Foo4 a_0123456789876543210 = Apply (LamCases_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210
type Foo3 :: forall a. Maybe a -> a
type family Foo3 @a (a :: Maybe a) :: a where
Foo3 @a ('Just x :: Maybe a) = x :: a
type Foo2 :: forall a. Maybe a -> a
type family Foo2 @a (a :: Maybe a) :: a where
Foo2 @a ('Just x :: Maybe a :: Maybe a) = x :: a
type Foo1 :: Maybe a -> a
type family Foo1 @a (a :: Maybe a) :: a where
Foo1 ('Just x :: Maybe a) = x :: a
type family G a where
G x = Apply (LamCases_0123456789876543210Sym0 x) (Apply JustSym0 x)
type family F3 a where
F3 ('Just a :: Maybe Bool) = "hi"
type family F2 a where
F2 (x :: Maybe a) = x :: Maybe a
type family F1 a where
F1 (x :: Maybe Bool) = x :: Maybe Bool
sFoo9 :: (forall (t :: a). Sing t -> Sing (Foo9 t :: a) :: Type)
sFoo8 ::
forall a (t :: Maybe a). Sing t -> Sing (Foo8 t :: Maybe a)
sFoo7 ::
(forall (t :: a) (t :: b).
Sing t -> Sing t -> Sing (Foo7 t t :: a) :: Type)
sFoo6 ::
(forall (t :: Maybe (Maybe a)).
Sing t -> Sing (Foo6 t :: Maybe (Maybe a)) :: Type)
sFoo5 ::
(forall (t :: Maybe (Maybe a)).
Sing t -> Sing (Foo5 t :: Maybe (Maybe a)) :: Type)
sFoo4 ::
(forall (t :: (a, b)). Sing t -> Sing (Foo4 t :: (b, a)) :: Type)
sFoo3 :: forall a (t :: Maybe a). Sing t -> Sing (Foo3 t :: a)
sFoo2 :: forall a (t :: Maybe a). Sing t -> Sing (Foo2 t :: a)
sFoo1 ::
(forall (t :: Maybe a). Sing t -> Sing (Foo1 t :: a) :: Type)
sG :: forall arg. Sing arg -> Sing (G arg)
sF3 :: forall arg. Sing arg -> Sing (F3 arg)
sF2 :: forall arg. Sing arg -> Sing (F2 arg)
sF1 :: forall arg. Sing arg -> Sing (F1 arg)
sFoo9 (sX :: Sing x)
= (\cases
(_ :: Sing (x :: a))
-> let
sG ::
(forall (t :: a) (t :: b).
Sing t
-> Sing t -> Sing (Let0123456789876543210G a x t t :: a) :: Type)
sG (sY :: Sing y) _ = sY
in
applySing
(applySing (singFun2 @(Let0123456789876543210GSym0 a x) sG) sX)
STuple0)
(sX :: Sing x)
sFoo8
(SJust (sWild_0123456789876543210 :: Sing wild_0123456789876543210))
= (\cases
(_ :: Sing (wild_0123456789876543210 :: a))
(_ :: Sing ('Just (wild_0123456789876543210 :: a) :: Maybe a))
-> let
sX :: Sing @_ (Let0123456789876543210X a wild_0123456789876543210)
sX
= applySing
(singFun1 @JustSym0 SJust)
(sWild_0123456789876543210 ::
Sing (wild_0123456789876543210 :: a)) ::
Sing (Apply JustSym0 (wild_0123456789876543210 :: a) :: Maybe a)
in sX)
(sWild_0123456789876543210 :: Sing wild_0123456789876543210)
(SJust
(sWild_0123456789876543210 :: Sing wild_0123456789876543210))
sFoo8 SNothing
= (\cases
(_ :: Sing ('Nothing :: Maybe a))
-> let
sX :: Sing @_ (Let0123456789876543210X a)
sX = SNothing :: Sing (NothingSym0 :: Maybe a)
in sX)
SNothing
sFoo7
(sX :: Sing x)
(sWild_0123456789876543210 :: Sing wild_0123456789876543210)
= (\cases
(_ :: Sing (x :: a)) (_ :: Sing (wild_0123456789876543210 :: b))
-> sX :: Sing (x :: a))
(sX :: Sing x)
(sWild_0123456789876543210 :: Sing wild_0123456789876543210)
sFoo6 (SJust (sX :: Sing x))
= (\cases
(_ :: Sing ('Just x :: Maybe (Maybe a)))
-> applySing
(singFun1
@(LamCases_0123456789876543210Sym0 a x)
(\cases
(SJust (sY :: Sing y))
-> (\cases
(_ :: Sing (y :: a)) (_ :: Sing ('Just (y :: a) :: Maybe a))
-> applySing
(singFun1 @JustSym0 SJust)
(applySing
(singFun1 @JustSym0 SJust) (sY :: Sing (y :: a)) ::
Sing (Apply JustSym0 (y :: a) :: Maybe a)))
(sY :: Sing y) (SJust (sY :: Sing y))))
(sX :: Sing (x :: Maybe a)))
(SJust (sX :: Sing x))
sFoo5 (SJust (SJust (sX :: Sing x)))
= (\cases
(_ :: Sing (x :: a))
(_ :: Sing ('Just (x :: a) :: Maybe a))
(_ :: Sing ('Just ('Just (x :: a) :: Maybe a) :: Maybe (Maybe a)))
-> applySing
(singFun1 @JustSym0 SJust)
(applySing (singFun1 @JustSym0 SJust) (sX :: Sing (x :: a)) ::
Sing (Apply JustSym0 (x :: a) :: Maybe a)) ::
Sing (Apply JustSym0 (Apply JustSym0 (x :: a) :: Maybe a) :: Maybe (Maybe a)))
(sX :: Sing x) (SJust (sX :: Sing x))
(SJust (SJust (sX :: Sing x)))
sFoo4 (sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(singFun1
@(LamCases_0123456789876543210Sym0 a_0123456789876543210)
(\cases
(STuple2 (sX :: Sing x) (sY :: Sing y))
-> (\cases
(_ :: Sing (x :: a)) (_ :: Sing (y :: b))
-> applySing
(applySing (singFun2 @Tuple2Sym0 STuple2) (sY :: Sing (y :: b)))
(sX :: Sing (x :: a)))
(sX :: Sing x) (sY :: Sing y)))
sA_0123456789876543210
sFoo3 (SJust (sX :: Sing x)) = sX :: Sing (x :: a)
sFoo2 (SJust (sX :: Sing x))
= (\cases (_ :: Sing ('Just x :: Maybe a)) -> sX :: Sing (x :: a))
(SJust (sX :: Sing x))
sFoo1 (SJust (sX :: Sing x))
= (\cases (_ :: Sing ('Just x :: Maybe a)) -> sX :: Sing (x :: a))
(SJust (sX :: Sing x))
sG (sX :: Sing x)
= applySing
(singFun1
@(LamCases_0123456789876543210Sym0 x)
(\cases
(SJust (sY :: Sing y))
-> (\cases
(_ :: Sing ('Just y :: Maybe Bool)) -> sY :: Sing (y :: Bool))
(SJust (sY :: Sing y))))
(applySing (singFun1 @JustSym0 SJust) sX)
sF3 (SJust (sA :: Sing a))
= (\cases (_ :: Sing ('Just a :: Maybe Bool)) -> sing :: Sing "hi")
(SJust (sA :: Sing a))
sF2 (sX :: Sing x)
= (\cases (_ :: Sing (x :: Maybe a)) -> sX :: Sing (x :: Maybe a))
(sX :: Sing x)
sF1 (sX :: Sing x)
= (\cases
(_ :: Sing (x :: Maybe Bool)) -> sX :: Sing (x :: Maybe Bool))
(sX :: Sing x)
instance SingI (Foo9Sym0 :: (~>) a a) where
sing = singFun1 @Foo9Sym0 sFoo9
instance SingI (Foo8Sym0 :: (~>) (Maybe a) (Maybe a)) where
sing = singFun1 @Foo8Sym0 sFoo8
instance SingI (Foo7Sym0 :: (~>) a ((~>) b a)) where
sing = singFun2 @Foo7Sym0 sFoo7
instance SingI d => SingI (Foo7Sym1 (d :: a) :: (~>) b a) where
sing = singFun1 @(Foo7Sym1 (d :: a)) (sFoo7 (sing @d))
instance SingI1 (Foo7Sym1 :: a -> (~>) b a) where
liftSing (s :: Sing (d :: a))
= singFun1 @(Foo7Sym1 (d :: a)) (sFoo7 s)
instance SingI (Foo6Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a))) where
sing = singFun1 @Foo6Sym0 sFoo6
instance SingI (Foo5Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a))) where
sing = singFun1 @Foo5Sym0 sFoo5
instance SingI (Foo4Sym0 :: (~>) (a, b) (b, a)) where
sing = singFun1 @Foo4Sym0 sFoo4
instance SingI (Foo3Sym0 :: (~>) (Maybe a) a) where
sing = singFun1 @Foo3Sym0 sFoo3
instance SingI (Foo2Sym0 :: (~>) (Maybe a) a) where
sing = singFun1 @Foo2Sym0 sFoo2
instance SingI (Foo1Sym0 :: (~>) (Maybe a) a) where
sing = singFun1 @Foo1Sym0 sFoo1
instance SingI GSym0 where
sing = singFun1 @GSym0 sG
instance SingI F3Sym0 where
sing = singFun1 @F3Sym0 sF3
instance SingI F2Sym0 where
sing = singFun1 @F2Sym0 sF2
instance SingI F1Sym0 where
sing = singFun1 @F1Sym0 sF1