singletons-2.7: 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 x0123456789876543210
where
Let0123456789876543210GSym0KindInference :: SameKind (Apply Let0123456789876543210GSym0 arg) (Let0123456789876543210GSym1 arg) =>
Let0123456789876543210GSym0 x0123456789876543210
type instance Apply Let0123456789876543210GSym0 x0123456789876543210 = Let0123456789876543210GSym1 x0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210GSym0 where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210GSym0KindInference) ())
data Let0123456789876543210GSym1 x0123456789876543210 :: (~>) a ((~>) b0123456789876543210 a)
where
Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 x0123456789876543210) arg) (Let0123456789876543210GSym2 x0123456789876543210 arg) =>
Let0123456789876543210GSym1 x0123456789876543210 a0123456789876543210
type instance Apply (Let0123456789876543210GSym1 x0123456789876543210) a0123456789876543210 = Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210GSym1 x0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210GSym1KindInference) ())
data Let0123456789876543210GSym2 x0123456789876543210 (a0123456789876543210 :: a) :: (~>) b0123456789876543210 a
where
Let0123456789876543210GSym2KindInference :: SameKind (Apply (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 arg) =>
Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) a0123456789876543210 = Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210GSym2KindInference) ())
type Let0123456789876543210GSym3 x0123456789876543210 (a0123456789876543210 :: a) (a0123456789876543210 :: b0123456789876543210) =
Let0123456789876543210G x0123456789876543210 a0123456789876543210 a0123456789876543210 :: a
type family Let0123456789876543210G x (a :: a) (a :: b) :: a where
Let0123456789876543210G x y _ = y
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 :: a) :: Maybe a
type Let0123456789876543210XSym0 = Let0123456789876543210X
type family Let0123456789876543210X where
Let0123456789876543210X = NothingSym0 :: Maybe a
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
(((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
())
type Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 =
Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210 x where
Let0123456789876543210Scrutinee_0123456789876543210 x = x :: Maybe a
type family Case_0123456789876543210 x t where
Case_0123456789876543210 x ('Just (y :: a) :: Maybe a) = Apply JustSym0 (Apply JustSym0 (y :: a) :: Maybe a)
type family Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 t where
Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 '(x :: a,
y :: b) = Apply (Apply Tuple2Sym0 (y :: b)) (x :: a)
type family Lambda_0123456789876543210 a_0123456789876543210 arg_0123456789876543210 where
Lambda_0123456789876543210 a_0123456789876543210 arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 arg_0123456789876543210
data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
type Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 =
Lambda_0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
(((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
())
type Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 =
Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210 x where
Let0123456789876543210Scrutinee_0123456789876543210 x = Apply JustSym0 x
type family Case_0123456789876543210 x t where
Case_0123456789876543210 x ('Just y :: Maybe Bool) = y :: Bool
type Foo9Sym0 :: (~>) a a
data Foo9Sym0 a0123456789876543210
where
Foo9Sym0KindInference :: SameKind (Apply Foo9Sym0 arg) (Foo9Sym1 arg) =>
Foo9Sym0 a0123456789876543210
type instance Apply Foo9Sym0 a0123456789876543210 = Foo9Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo9Sym0 where
suppressUnusedWarnings = snd (((,) Foo9Sym0KindInference) ())
type Foo9Sym1 (a0123456789876543210 :: a) =
Foo9 a0123456789876543210 :: a
type Foo8Sym0 :: forall a. (~>) (Maybe a) (Maybe a)
data Foo8Sym0 a0123456789876543210
where
Foo8Sym0KindInference :: SameKind (Apply Foo8Sym0 arg) (Foo8Sym1 arg) =>
Foo8Sym0 a0123456789876543210
type instance Apply Foo8Sym0 a0123456789876543210 = Foo8Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo8Sym0 where
suppressUnusedWarnings = snd (((,) Foo8Sym0KindInference) ())
type Foo8Sym1 (a0123456789876543210 :: Maybe a) =
Foo8 a0123456789876543210 :: Maybe a
type Foo7Sym0 :: (~>) a ((~>) b a)
data Foo7Sym0 a0123456789876543210
where
Foo7Sym0KindInference :: SameKind (Apply Foo7Sym0 arg) (Foo7Sym1 arg) =>
Foo7Sym0 a0123456789876543210
type instance Apply Foo7Sym0 a0123456789876543210 = Foo7Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo7Sym0 where
suppressUnusedWarnings = snd (((,) Foo7Sym0KindInference) ())
type Foo7Sym1 :: a -> (~>) b a
data Foo7Sym1 a0123456789876543210 a0123456789876543210
where
Foo7Sym1KindInference :: SameKind (Apply (Foo7Sym1 a0123456789876543210) arg) (Foo7Sym2 a0123456789876543210 arg) =>
Foo7Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (Foo7Sym1 a0123456789876543210) a0123456789876543210 = Foo7Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Foo7Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) Foo7Sym1KindInference) ())
type Foo7Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) =
Foo7 a0123456789876543210 a0123456789876543210 :: a
type Foo6Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a))
data Foo6Sym0 a0123456789876543210
where
Foo6Sym0KindInference :: SameKind (Apply Foo6Sym0 arg) (Foo6Sym1 arg) =>
Foo6Sym0 a0123456789876543210
type instance Apply Foo6Sym0 a0123456789876543210 = Foo6Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo6Sym0 where
suppressUnusedWarnings = snd (((,) Foo6Sym0KindInference) ())
type Foo6Sym1 (a0123456789876543210 :: Maybe (Maybe a)) =
Foo6 a0123456789876543210 :: Maybe (Maybe a)
type Foo5Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a))
data Foo5Sym0 a0123456789876543210
where
Foo5Sym0KindInference :: SameKind (Apply Foo5Sym0 arg) (Foo5Sym1 arg) =>
Foo5Sym0 a0123456789876543210
type instance Apply Foo5Sym0 a0123456789876543210 = Foo5Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo5Sym0 where
suppressUnusedWarnings = snd (((,) Foo5Sym0KindInference) ())
type Foo5Sym1 (a0123456789876543210 :: Maybe (Maybe a)) =
Foo5 a0123456789876543210 :: Maybe (Maybe a)
type Foo4Sym0 :: (~>) (a, b) (b, a)
data Foo4Sym0 a0123456789876543210
where
Foo4Sym0KindInference :: SameKind (Apply Foo4Sym0 arg) (Foo4Sym1 arg) =>
Foo4Sym0 a0123456789876543210
type instance Apply Foo4Sym0 a0123456789876543210 = Foo4Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo4Sym0 where
suppressUnusedWarnings = snd (((,) Foo4Sym0KindInference) ())
type Foo4Sym1 (a0123456789876543210 :: (a, b)) =
Foo4 a0123456789876543210 :: (b, a)
type Foo3Sym0 :: forall a. (~>) (Maybe a) a
data Foo3Sym0 a0123456789876543210
where
Foo3Sym0KindInference :: SameKind (Apply Foo3Sym0 arg) (Foo3Sym1 arg) =>
Foo3Sym0 a0123456789876543210
type instance Apply Foo3Sym0 a0123456789876543210 = Foo3Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo3Sym0 where
suppressUnusedWarnings = snd (((,) Foo3Sym0KindInference) ())
type Foo3Sym1 (a0123456789876543210 :: Maybe a) =
Foo3 a0123456789876543210 :: a
type Foo2Sym0 :: forall a. (~>) (Maybe a) a
data Foo2Sym0 a0123456789876543210
where
Foo2Sym0KindInference :: SameKind (Apply Foo2Sym0 arg) (Foo2Sym1 arg) =>
Foo2Sym0 a0123456789876543210
type instance Apply Foo2Sym0 a0123456789876543210 = Foo2Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo2Sym0 where
suppressUnusedWarnings = snd (((,) Foo2Sym0KindInference) ())
type Foo2Sym1 (a0123456789876543210 :: Maybe a) =
Foo2 a0123456789876543210 :: a
type Foo1Sym0 :: (~>) (Maybe a) a
data Foo1Sym0 a0123456789876543210
where
Foo1Sym0KindInference :: SameKind (Apply Foo1Sym0 arg) (Foo1Sym1 arg) =>
Foo1Sym0 a0123456789876543210
type instance Apply Foo1Sym0 a0123456789876543210 = Foo1Sym1 a0123456789876543210
instance SuppressUnusedWarnings Foo1Sym0 where
suppressUnusedWarnings = snd (((,) Foo1Sym0KindInference) ())
type Foo1Sym1 (a0123456789876543210 :: Maybe a) =
Foo1 a0123456789876543210 :: a
data GSym0 a0123456789876543210
where
GSym0KindInference :: SameKind (Apply GSym0 arg) (GSym1 arg) =>
GSym0 a0123456789876543210
type instance Apply GSym0 a0123456789876543210 = GSym1 a0123456789876543210
instance SuppressUnusedWarnings GSym0 where
suppressUnusedWarnings = snd (((,) GSym0KindInference) ())
type GSym1 a0123456789876543210 = G a0123456789876543210
data F3Sym0 a0123456789876543210
where
F3Sym0KindInference :: SameKind (Apply F3Sym0 arg) (F3Sym1 arg) =>
F3Sym0 a0123456789876543210
type instance Apply F3Sym0 a0123456789876543210 = F3Sym1 a0123456789876543210
instance SuppressUnusedWarnings F3Sym0 where
suppressUnusedWarnings = snd (((,) F3Sym0KindInference) ())
type F3Sym1 a0123456789876543210 = F3 a0123456789876543210
data F2Sym0 a0123456789876543210
where
F2Sym0KindInference :: SameKind (Apply F2Sym0 arg) (F2Sym1 arg) =>
F2Sym0 a0123456789876543210
type instance Apply F2Sym0 a0123456789876543210 = F2Sym1 a0123456789876543210
instance SuppressUnusedWarnings F2Sym0 where
suppressUnusedWarnings = snd (((,) F2Sym0KindInference) ())
type F2Sym1 a0123456789876543210 = F2 a0123456789876543210
data F1Sym0 a0123456789876543210
where
F1Sym0KindInference :: SameKind (Apply F1Sym0 arg) (F1Sym1 arg) =>
F1Sym0 a0123456789876543210
type instance Apply F1Sym0 a0123456789876543210 = F1Sym1 a0123456789876543210
instance SuppressUnusedWarnings F1Sym0 where
suppressUnusedWarnings = snd (((,) F1Sym0KindInference) ())
type F1Sym1 a0123456789876543210 = F1 a0123456789876543210
type Foo9 :: a -> a
type family Foo9 a where
Foo9 (x :: a) = Apply (Apply (Let0123456789876543210GSym1 x) x) Tuple0Sym0
type Foo8 :: forall a. Maybe a -> Maybe a
type family Foo8 a where
Foo8 ('Just (wild_0123456789876543210 :: a) :: Maybe a) = Let0123456789876543210XSym1 wild_0123456789876543210
Foo8 ('Nothing :: Maybe a) = Let0123456789876543210XSym0
type Foo7 :: a -> b -> a
type family Foo7 a a where
Foo7 (x :: a) (wild_0123456789876543210 :: b) = x :: a
type Foo6 :: Maybe (Maybe a) -> Maybe (Maybe a)
type family Foo6 a where
Foo6 ('Just x :: Maybe (Maybe a)) = Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x)
type Foo5 :: Maybe (Maybe a) -> Maybe (Maybe a)
type family Foo5 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 where
Foo4 a_0123456789876543210 = Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210
type Foo3 :: forall a. Maybe a -> a
type family Foo3 a where
Foo3 ('Just x) = x :: a
type Foo2 :: forall a. Maybe a -> a
type family Foo2 a where
Foo2 ('Just x :: Maybe a) = x :: a
type Foo1 :: Maybe a -> a
type family Foo1 a where
Foo1 ('Just x :: Maybe a) = x :: a
type family G a where
G x = Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 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 a (t :: a). Sing t -> Sing (Apply Foo9Sym0 t :: a)
sFoo8 ::
forall a (t :: Maybe a).
Sing t -> Sing (Apply Foo8Sym0 t :: Maybe a)
sFoo7 ::
forall a b (t :: a) (t :: b).
Sing t -> Sing t -> Sing (Apply (Apply Foo7Sym0 t) t :: a)
sFoo6 ::
forall a (t :: Maybe (Maybe a)).
Sing t -> Sing (Apply Foo6Sym0 t :: Maybe (Maybe a))
sFoo5 ::
forall a (t :: Maybe (Maybe a)).
Sing t -> Sing (Apply Foo5Sym0 t :: Maybe (Maybe a))
sFoo4 ::
forall a b (t :: (a, b)).
Sing t -> Sing (Apply Foo4Sym0 t :: (b, a))
sFoo3 ::
forall a (t :: Maybe a). Sing t -> Sing (Apply Foo3Sym0 t :: a)
sFoo2 ::
forall a (t :: Maybe a). Sing t -> Sing (Apply Foo2Sym0 t :: a)
sFoo1 ::
forall a (t :: Maybe a). Sing t -> Sing (Apply Foo1Sym0 t :: a)
sG :: forall arg. Sing arg -> Sing (Apply GSym0 arg)
sF3 :: forall arg. Sing arg -> Sing (Apply F3Sym0 arg)
sF2 :: forall arg. Sing arg -> Sing (Apply F2Sym0 arg)
sF1 :: forall arg. Sing arg -> Sing (Apply F1Sym0 arg)
sFoo9 (sX :: Sing x)
= case sX :: Sing x of {
(_ :: Sing (x :: a))
-> let
sG ::
forall b (t :: a) (t :: b).
Sing t
-> Sing t
-> Sing (Apply (Apply (Let0123456789876543210GSym1 x) t) t :: a)
sG (sY :: Sing y) _ = sY
in
(applySing
((applySing ((singFun2 @(Let0123456789876543210GSym1 x)) sG)) sX))
STuple0 }
sFoo8
(SJust (sWild_0123456789876543210 :: Sing wild_0123456789876543210))
= case
((,) (sWild_0123456789876543210 :: Sing wild_0123456789876543210))
(SJust
(sWild_0123456789876543210 :: Sing wild_0123456789876543210))
of {
(,) (_ :: Sing (wild_0123456789876543210 :: a))
(_ :: Sing ('Just (wild_0123456789876543210 :: a) :: Maybe a))
-> let
sX ::
Sing @_ (Let0123456789876543210XSym1 wild_0123456789876543210)
sX
= (applySing ((singFun1 @JustSym0) SJust))
(sWild_0123456789876543210 ::
Sing (wild_0123456789876543210 :: a)) ::
Sing (Apply JustSym0 (wild_0123456789876543210 :: a) :: Maybe a)
in sX }
sFoo8 SNothing
= case SNothing of {
(_ :: Sing ('Nothing :: Maybe a))
-> let
sX :: Sing @_ Let0123456789876543210XSym0
sX = SNothing :: Sing (NothingSym0 :: Maybe a)
in sX }
sFoo7
(sX :: Sing x)
(sWild_0123456789876543210 :: Sing wild_0123456789876543210)
= case
((,) (sX :: Sing x))
(sWild_0123456789876543210 :: Sing wild_0123456789876543210)
of {
(,) (_ :: Sing (x :: a))
(_ :: Sing (wild_0123456789876543210 :: b))
-> sX :: Sing (x :: a) }
sFoo6 (SJust (sX :: Sing x))
= case SJust (sX :: Sing x) of {
(_ :: Sing ('Just x :: Maybe (Maybe a)))
-> let
sScrutinee_0123456789876543210 ::
Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x)
sScrutinee_0123456789876543210 = sX :: Sing (x :: Maybe a)
in
(id
@(Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) :: Maybe (Maybe a))))
(case sScrutinee_0123456789876543210 of {
SJust (sY :: Sing y)
-> case ((,) (sY :: Sing y)) (SJust (sY :: Sing y)) of {
(,) (_ :: 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)) } }) }
sFoo5 (SJust (SJust (sX :: Sing x)))
= case
(((,,) (sX :: Sing x)) (SJust (sX :: Sing x)))
(SJust (SJust (sX :: Sing x)))
of {
(,,) (_ :: 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)) }
sFoo4 (sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
((singFun1
@(Apply Lambda_0123456789876543210Sym0 a_0123456789876543210))
(\ sArg_0123456789876543210
-> case sArg_0123456789876543210 of {
(_ :: Sing arg_0123456789876543210)
-> (id
@(Sing (Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 arg_0123456789876543210)))
(case sArg_0123456789876543210 of {
STuple2 (sX :: Sing x) (sY :: Sing y)
-> case ((,) (sX :: Sing x)) (sY :: Sing y) of {
(,) (_ :: Sing (x :: a)) (_ :: Sing (y :: b))
-> (applySing
((applySing ((singFun2 @Tuple2Sym0) STuple2))
(sY :: Sing (y :: b))))
(sX :: Sing (x :: a)) } }) })))
sA_0123456789876543210
sFoo3 (SJust (sX :: Sing x)) = sX :: Sing (x :: a)
sFoo2 (SJust (sX :: Sing x))
= case SJust (sX :: Sing x) of {
(_ :: Sing ('Just x :: Maybe a)) -> sX :: Sing (x :: a) }
sFoo1 (SJust (sX :: Sing x))
= case SJust (sX :: Sing x) of {
(_ :: Sing ('Just x :: Maybe a)) -> sX :: Sing (x :: a) }
sG (sX :: Sing x)
= let
sScrutinee_0123456789876543210 ::
Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x)
sScrutinee_0123456789876543210
= (applySing ((singFun1 @JustSym0) SJust)) sX
in
(id
@(Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x))))
(case sScrutinee_0123456789876543210 of {
SJust (sY :: Sing y)
-> case SJust (sY :: Sing y) of {
(_ :: Sing ('Just y :: Maybe Bool)) -> sY :: Sing (y :: Bool) } })
sF3 (SJust (sA :: Sing a))
= case SJust (sA :: Sing a) of {
(_ :: Sing ('Just a :: Maybe Bool)) -> sing :: Sing "hi" }
sF2 (sX :: Sing x)
= case sX :: Sing x of {
(_ :: Sing (x :: Maybe a)) -> sX :: Sing (x :: Maybe a) }
sF1 (sX :: Sing x)
= case sX :: Sing x of {
(_ :: Sing (x :: Maybe Bool)) -> sX :: Sing (x :: Maybe Bool) }
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 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