singletons-2.5: tests/compile-and-dump/Singletons/T183.ghc86.template
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
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
foo9 :: a -> a
foo9 (x :: a)
= let
g :: a -> b -> a
g y _ = y
in (g x) ()
type Let0123456789876543210GSym3 x0123456789876543210 (a0123456789876543210 :: a) (a0123456789876543210 :: b0123456789876543210) =
Let0123456789876543210G x0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210GSym2KindInference) ())
data Let0123456789876543210GSym2 x0123456789876543210 (a0123456789876543210 :: a) :: forall b0123456789876543210.
(~>) b0123456789876543210 a
where
Let0123456789876543210GSym2KindInference :: forall x0123456789876543210
a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 arg) =>
Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210) a0123456789876543210 = Let0123456789876543210G a0123456789876543210 x0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210GSym1 x0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210GSym1KindInference) ())
data Let0123456789876543210GSym1 x0123456789876543210 :: forall b0123456789876543210
a.
(~>) a ((~>) b0123456789876543210 a)
where
Let0123456789876543210GSym1KindInference :: forall x0123456789876543210
a0123456789876543210
arg. SameKind (Apply (Let0123456789876543210GSym1 x0123456789876543210) arg) (Let0123456789876543210GSym2 x0123456789876543210 arg) =>
Let0123456789876543210GSym1 x0123456789876543210 a0123456789876543210
type instance Apply (Let0123456789876543210GSym1 x0123456789876543210) a0123456789876543210 = Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210GSym0 where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210GSym0KindInference) ())
data Let0123456789876543210GSym0 x0123456789876543210
where
Let0123456789876543210GSym0KindInference :: forall x0123456789876543210
arg. SameKind (Apply Let0123456789876543210GSym0 arg) (Let0123456789876543210GSym1 arg) =>
Let0123456789876543210GSym0 x0123456789876543210
type instance Apply Let0123456789876543210GSym0 x0123456789876543210 = Let0123456789876543210GSym1 x0123456789876543210
type family Let0123456789876543210G x (a :: a) (a :: b) :: a where
Let0123456789876543210G x y _ = y
type Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 =
Let0123456789876543210X wild_01234567898765432100123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210XSym0 where
suppressUnusedWarnings
= snd (((,) Let0123456789876543210XSym0KindInference) ())
data Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210
where
Let0123456789876543210XSym0KindInference :: forall wild_01234567898765432100123456789876543210
arg. SameKind (Apply Let0123456789876543210XSym0 arg) (Let0123456789876543210XSym1 arg) =>
Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210
type instance Apply Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210
type family Let0123456789876543210X wild_0123456789876543210 where
Let0123456789876543210X wild_0123456789876543210 = (Apply JustSym0 (wild_0123456789876543210 :: a) :: Maybe a)
type Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 =
Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
(((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: forall x0123456789876543210
arg. SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 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 t where
Lambda_0123456789876543210 a_0123456789876543210 arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 arg_0123456789876543210
type Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 t0123456789876543210 =
Lambda_0123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym1KindInference) ())
data Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 t0123456789876543210
where
Lambda_0123456789876543210Sym1KindInference :: forall a_01234567898765432100123456789876543210
t0123456789876543210
arg. SameKind (Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 arg) =>
Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 t0123456789876543210
type instance Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210) t0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings Lambda_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Lambda_0123456789876543210Sym0KindInference) ())
data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210
where
Lambda_0123456789876543210Sym0KindInference :: forall a_01234567898765432100123456789876543210
arg. SameKind (Apply Lambda_0123456789876543210Sym0 arg) (Lambda_0123456789876543210Sym1 arg) =>
Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210
type instance Apply Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 = Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210
type Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 =
Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
(((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: forall x0123456789876543210
arg. SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 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 Foo9Sym1 (a0123456789876543210 :: a0123456789876543210) =
Foo9 a0123456789876543210
instance SuppressUnusedWarnings Foo9Sym0 where
suppressUnusedWarnings = snd (((,) Foo9Sym0KindInference) ())
data Foo9Sym0 :: forall a0123456789876543210.
(~>) a0123456789876543210 a0123456789876543210
where
Foo9Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo9Sym0 arg) (Foo9Sym1 arg) =>
Foo9Sym0 a0123456789876543210
type instance Apply Foo9Sym0 a0123456789876543210 = Foo9 a0123456789876543210
type Foo8Sym1 (a0123456789876543210 :: Maybe a0123456789876543210) =
Foo8 a0123456789876543210
instance SuppressUnusedWarnings Foo8Sym0 where
suppressUnusedWarnings = snd (((,) Foo8Sym0KindInference) ())
data Foo8Sym0 :: forall a0123456789876543210.
(~>) (Maybe a0123456789876543210) (Maybe a0123456789876543210)
where
Foo8Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo8Sym0 arg) (Foo8Sym1 arg) =>
Foo8Sym0 a0123456789876543210
type instance Apply Foo8Sym0 a0123456789876543210 = Foo8 a0123456789876543210
type Foo7Sym2 (a0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) =
Foo7 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Foo7Sym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) Foo7Sym1KindInference) ())
data Foo7Sym1 (a0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210.
(~>) b0123456789876543210 a0123456789876543210
where
Foo7Sym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (Foo7Sym1 a0123456789876543210) arg) (Foo7Sym2 a0123456789876543210 arg) =>
Foo7Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (Foo7Sym1 a0123456789876543210) a0123456789876543210 = Foo7 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings Foo7Sym0 where
suppressUnusedWarnings = snd (((,) Foo7Sym0KindInference) ())
data Foo7Sym0 :: forall a0123456789876543210 b0123456789876543210.
(~>) a0123456789876543210 ((~>) b0123456789876543210 a0123456789876543210)
where
Foo7Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo7Sym0 arg) (Foo7Sym1 arg) =>
Foo7Sym0 a0123456789876543210
type instance Apply Foo7Sym0 a0123456789876543210 = Foo7Sym1 a0123456789876543210
type Foo6Sym1 (a0123456789876543210 :: Maybe (Maybe a0123456789876543210)) =
Foo6 a0123456789876543210
instance SuppressUnusedWarnings Foo6Sym0 where
suppressUnusedWarnings = snd (((,) Foo6Sym0KindInference) ())
data Foo6Sym0 :: forall a0123456789876543210.
(~>) (Maybe (Maybe a0123456789876543210)) (Maybe (Maybe a0123456789876543210))
where
Foo6Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo6Sym0 arg) (Foo6Sym1 arg) =>
Foo6Sym0 a0123456789876543210
type instance Apply Foo6Sym0 a0123456789876543210 = Foo6 a0123456789876543210
type Foo5Sym1 (a0123456789876543210 :: Maybe (Maybe a0123456789876543210)) =
Foo5 a0123456789876543210
instance SuppressUnusedWarnings Foo5Sym0 where
suppressUnusedWarnings = snd (((,) Foo5Sym0KindInference) ())
data Foo5Sym0 :: forall a0123456789876543210.
(~>) (Maybe (Maybe a0123456789876543210)) (Maybe (Maybe a0123456789876543210))
where
Foo5Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo5Sym0 arg) (Foo5Sym1 arg) =>
Foo5Sym0 a0123456789876543210
type instance Apply Foo5Sym0 a0123456789876543210 = Foo5 a0123456789876543210
type Foo4Sym1 (a0123456789876543210 :: (a0123456789876543210,
b0123456789876543210)) =
Foo4 a0123456789876543210
instance SuppressUnusedWarnings Foo4Sym0 where
suppressUnusedWarnings = snd (((,) Foo4Sym0KindInference) ())
data Foo4Sym0 :: forall a0123456789876543210 b0123456789876543210.
(~>) (a0123456789876543210,
b0123456789876543210) (b0123456789876543210, a0123456789876543210)
where
Foo4Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo4Sym0 arg) (Foo4Sym1 arg) =>
Foo4Sym0 a0123456789876543210
type instance Apply Foo4Sym0 a0123456789876543210 = Foo4 a0123456789876543210
type Foo3Sym1 (a0123456789876543210 :: Maybe a0123456789876543210) =
Foo3 a0123456789876543210
instance SuppressUnusedWarnings Foo3Sym0 where
suppressUnusedWarnings = snd (((,) Foo3Sym0KindInference) ())
data Foo3Sym0 :: forall a0123456789876543210.
(~>) (Maybe a0123456789876543210) a0123456789876543210
where
Foo3Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo3Sym0 arg) (Foo3Sym1 arg) =>
Foo3Sym0 a0123456789876543210
type instance Apply Foo3Sym0 a0123456789876543210 = Foo3 a0123456789876543210
type Foo2Sym1 (a0123456789876543210 :: Maybe a0123456789876543210) =
Foo2 a0123456789876543210
instance SuppressUnusedWarnings Foo2Sym0 where
suppressUnusedWarnings = snd (((,) Foo2Sym0KindInference) ())
data Foo2Sym0 :: forall a0123456789876543210.
(~>) (Maybe a0123456789876543210) a0123456789876543210
where
Foo2Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo2Sym0 arg) (Foo2Sym1 arg) =>
Foo2Sym0 a0123456789876543210
type instance Apply Foo2Sym0 a0123456789876543210 = Foo2 a0123456789876543210
type Foo1Sym1 (a0123456789876543210 :: Maybe a0123456789876543210) =
Foo1 a0123456789876543210
instance SuppressUnusedWarnings Foo1Sym0 where
suppressUnusedWarnings = snd (((,) Foo1Sym0KindInference) ())
data Foo1Sym0 :: forall a0123456789876543210.
(~>) (Maybe a0123456789876543210) a0123456789876543210
where
Foo1Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Foo1Sym0 arg) (Foo1Sym1 arg) =>
Foo1Sym0 a0123456789876543210
type instance Apply Foo1Sym0 a0123456789876543210 = Foo1 a0123456789876543210
type GSym1 a0123456789876543210 = G a0123456789876543210
instance SuppressUnusedWarnings GSym0 where
suppressUnusedWarnings = snd (((,) GSym0KindInference) ())
data GSym0 a0123456789876543210
where
GSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply GSym0 arg) (GSym1 arg) =>
GSym0 a0123456789876543210
type instance Apply GSym0 a0123456789876543210 = G a0123456789876543210
type F3Sym1 a0123456789876543210 = F3 a0123456789876543210
instance SuppressUnusedWarnings F3Sym0 where
suppressUnusedWarnings = snd (((,) F3Sym0KindInference) ())
data F3Sym0 a0123456789876543210
where
F3Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply F3Sym0 arg) (F3Sym1 arg) =>
F3Sym0 a0123456789876543210
type instance Apply F3Sym0 a0123456789876543210 = F3 a0123456789876543210
type F2Sym1 a0123456789876543210 = F2 a0123456789876543210
instance SuppressUnusedWarnings F2Sym0 where
suppressUnusedWarnings = snd (((,) F2Sym0KindInference) ())
data F2Sym0 a0123456789876543210
where
F2Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply F2Sym0 arg) (F2Sym1 arg) =>
F2Sym0 a0123456789876543210
type instance Apply F2Sym0 a0123456789876543210 = F2 a0123456789876543210
type F1Sym1 a0123456789876543210 = F1 a0123456789876543210
instance SuppressUnusedWarnings F1Sym0 where
suppressUnusedWarnings = snd (((,) F1Sym0KindInference) ())
data F1Sym0 a0123456789876543210
where
F1Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply F1Sym0 arg) (F1Sym1 arg) =>
F1Sym0 a0123456789876543210
type instance Apply F1Sym0 a0123456789876543210 = F1 a0123456789876543210
type family Foo9 (a :: a) :: a where
Foo9 (x :: a) = Apply (Apply (Let0123456789876543210GSym1 x) x) Tuple0Sym0
type family Foo8 (a :: Maybe a) :: Maybe a where
Foo8 ( 'Just (wild_0123456789876543210 :: a) :: Maybe a) = Let0123456789876543210XSym1 wild_0123456789876543210
type family Foo7 (a :: a) (a :: b) :: a where
Foo7 (x :: a) (wild_0123456789876543210 :: b) = (x :: a)
type family Foo6 (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where
Foo6 ( 'Just x :: Maybe (Maybe a)) = Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x)
type family Foo5 (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 family Foo4 (a :: (a, b)) :: (b, a) where
Foo4 a_0123456789876543210 = Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210
type family Foo3 (a :: Maybe a) :: a where
Foo3 ( 'Just x) = (x :: a)
type family Foo2 (a :: Maybe a) :: a where
Foo2 ( 'Just x :: Maybe a) = (x :: a)
type family Foo1 (a :: Maybe a) :: 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 }
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 (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)) } }) ::
Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) :: Maybe (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)
-> (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)) } }) ::
Sing (Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 arg_0123456789876543210) })))
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 (case sScrutinee_0123456789876543210 of {
SJust (sY :: Sing y)
-> case SJust (sY :: Sing y) of {
(_ :: Sing ( 'Just y :: Maybe Bool))
-> sY :: Sing (y :: Bool) } }) ::
Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x))
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