Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations singletons [d| foo1 :: a -> Maybe a -> a foo1 d x = (\case { Just y -> y Nothing -> d }) x foo2 :: a -> Maybe a -> a foo2 d _ = (\case { Just y -> y Nothing -> d }) (Just d) foo3 :: a -> b -> a foo3 a b = (\case { (p, _) -> p }) (a, b) |] ======> foo1 :: forall a. a -> Maybe a -> a foo1 d x = \case { Just y -> y Nothing -> d } x foo2 :: forall a. a -> Maybe a -> a foo2 d _ = \case { Just y -> y Nothing -> d } (Just d) foo3 :: forall a b. a -> b -> a foo3 a b = \case { (p, _) -> p } (a, b) type family Case_0123456789 a b x_0123456789 t where Case_0123456789 a b x_0123456789 '(p, _z_0123456789) = p type family Lambda_0123456789 a b t where Lambda_0123456789 a b x_0123456789 = Case_0123456789 a b x_0123456789 x_0123456789 type Lambda_0123456789Sym3 t t t = Lambda_0123456789 t t t instance SuppressUnusedWarnings Lambda_0123456789Sym2 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.()) data Lambda_0123456789Sym2 l l l = forall arg. KindOf (Apply (Lambda_0123456789Sym2 l l) arg) ~ KindOf (Lambda_0123456789Sym3 l l arg) => Lambda_0123456789Sym2KindInference type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l instance SuppressUnusedWarnings Lambda_0123456789Sym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.()) data Lambda_0123456789Sym1 l l = forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) => Lambda_0123456789Sym1KindInference type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l instance SuppressUnusedWarnings Lambda_0123456789Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.()) data Lambda_0123456789Sym0 l = forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) => Lambda_0123456789Sym0KindInference type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l type family Case_0123456789 d x_0123456789 _z_0123456789 t where Case_0123456789 d x_0123456789 _z_0123456789 (Just y) = y Case_0123456789 d x_0123456789 _z_0123456789 Nothing = d type family Lambda_0123456789 d _z_0123456789 t where Lambda_0123456789 d _z_0123456789 x_0123456789 = Case_0123456789 d x_0123456789 _z_0123456789 x_0123456789 type Lambda_0123456789Sym3 t t t = Lambda_0123456789 t t t instance SuppressUnusedWarnings Lambda_0123456789Sym2 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.()) data Lambda_0123456789Sym2 l l l = forall arg. KindOf (Apply (Lambda_0123456789Sym2 l l) arg) ~ KindOf (Lambda_0123456789Sym3 l l arg) => Lambda_0123456789Sym2KindInference type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l instance SuppressUnusedWarnings Lambda_0123456789Sym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.()) data Lambda_0123456789Sym1 l l = forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) => Lambda_0123456789Sym1KindInference type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l instance SuppressUnusedWarnings Lambda_0123456789Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.()) data Lambda_0123456789Sym0 l = forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) => Lambda_0123456789Sym0KindInference type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l type family Case_0123456789 d x x_0123456789 t where Case_0123456789 d x x_0123456789 (Just y) = y Case_0123456789 d x x_0123456789 Nothing = d type family Lambda_0123456789 d x t where Lambda_0123456789 d x x_0123456789 = Case_0123456789 d x x_0123456789 x_0123456789 type Lambda_0123456789Sym3 t t t = Lambda_0123456789 t t t instance SuppressUnusedWarnings Lambda_0123456789Sym2 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.()) data Lambda_0123456789Sym2 l l l = forall arg. KindOf (Apply (Lambda_0123456789Sym2 l l) arg) ~ KindOf (Lambda_0123456789Sym3 l l arg) => Lambda_0123456789Sym2KindInference type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l instance SuppressUnusedWarnings Lambda_0123456789Sym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.()) data Lambda_0123456789Sym1 l l = forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) => Lambda_0123456789Sym1KindInference type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l instance SuppressUnusedWarnings Lambda_0123456789Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.()) data Lambda_0123456789Sym0 l = forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) => Lambda_0123456789Sym0KindInference type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l type Foo3Sym2 (t :: a) (t :: b) = Foo3 t t instance SuppressUnusedWarnings Foo3Sym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Foo3Sym1KindInference GHC.Tuple.()) data Foo3Sym1 (l :: a) (l :: TyFun b a) = forall arg. KindOf (Apply (Foo3Sym1 l) arg) ~ KindOf (Foo3Sym2 l arg) => Foo3Sym1KindInference type instance Apply (Foo3Sym1 l) l = Foo3Sym2 l l instance SuppressUnusedWarnings Foo3Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Foo3Sym0KindInference GHC.Tuple.()) data Foo3Sym0 (l :: TyFun a (TyFun b a -> *)) = forall arg. KindOf (Apply Foo3Sym0 arg) ~ KindOf (Foo3Sym1 arg) => Foo3Sym0KindInference type instance Apply Foo3Sym0 l = Foo3Sym1 l type Foo2Sym2 (t :: a) (t :: Maybe a) = Foo2 t t instance SuppressUnusedWarnings Foo2Sym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Foo2Sym1KindInference GHC.Tuple.()) data Foo2Sym1 (l :: a) (l :: TyFun (Maybe a) a) = forall arg. KindOf (Apply (Foo2Sym1 l) arg) ~ KindOf (Foo2Sym2 l arg) => Foo2Sym1KindInference type instance Apply (Foo2Sym1 l) l = Foo2Sym2 l l instance SuppressUnusedWarnings Foo2Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Foo2Sym0KindInference GHC.Tuple.()) data Foo2Sym0 (l :: TyFun a (TyFun (Maybe a) a -> *)) = forall arg. KindOf (Apply Foo2Sym0 arg) ~ KindOf (Foo2Sym1 arg) => Foo2Sym0KindInference type instance Apply Foo2Sym0 l = Foo2Sym1 l type Foo1Sym2 (t :: a) (t :: Maybe a) = Foo1 t t instance SuppressUnusedWarnings Foo1Sym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Foo1Sym1KindInference GHC.Tuple.()) data Foo1Sym1 (l :: a) (l :: TyFun (Maybe a) a) = forall arg. KindOf (Apply (Foo1Sym1 l) arg) ~ KindOf (Foo1Sym2 l arg) => Foo1Sym1KindInference type instance Apply (Foo1Sym1 l) l = Foo1Sym2 l l instance SuppressUnusedWarnings Foo1Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Foo1Sym0KindInference GHC.Tuple.()) data Foo1Sym0 (l :: TyFun a (TyFun (Maybe a) a -> *)) = forall arg. KindOf (Apply Foo1Sym0 arg) ~ KindOf (Foo1Sym1 arg) => Foo1Sym0KindInference type instance Apply Foo1Sym0 l = Foo1Sym1 l type family Foo3 (a :: a) (a :: b) :: a where Foo3 a b = Apply (Apply (Apply Lambda_0123456789Sym0 a) b) (Apply (Apply Tuple2Sym0 a) b) type family Foo2 (a :: a) (a :: Maybe a) :: a where Foo2 d _z_0123456789 = Apply (Apply (Apply Lambda_0123456789Sym0 d) _z_0123456789) (Apply JustSym0 d) type family Foo1 (a :: a) (a :: Maybe a) :: a where Foo1 d x = Apply (Apply (Apply Lambda_0123456789Sym0 d) x) x sFoo3 :: forall (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply Foo3Sym0 t) t :: a) sFoo2 :: forall (t :: a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply Foo2Sym0 t) t :: a) sFoo1 :: forall (t :: a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply Foo1Sym0 t) t :: a) sFoo3 sA sB = let lambda :: forall a b. (t ~ a, t ~ b) => Sing a -> Sing b -> Sing (Apply (Apply Foo3Sym0 a) b :: a) lambda a b = applySing (singFun1 (Proxy :: Proxy (Apply (Apply Lambda_0123456789Sym0 a) b)) (\ sX_0123456789 -> let lambda :: forall x_0123456789. Sing x_0123456789 -> Sing (Apply (Apply (Apply Lambda_0123456789Sym0 a) b) x_0123456789) lambda x_0123456789 = case x_0123456789 of { STuple2 sP _s_z_0123456789 -> let lambda :: forall p _z_0123456789. Apply (Apply Tuple2Sym0 p) _z_0123456789 ~ x_0123456789 => Sing p -> Sing _z_0123456789 -> Sing (Case_0123456789 a b x_0123456789 (Apply (Apply Tuple2Sym0 p) _z_0123456789)) lambda p _z_0123456789 = p in lambda sP _s_z_0123456789 } :: Sing (Case_0123456789 a b x_0123456789 x_0123456789) in lambda sX_0123456789)) (applySing (applySing (singFun2 (Proxy :: Proxy Tuple2Sym0) STuple2) a) b) in lambda sA sB sFoo2 sD _s_z_0123456789 = let lambda :: forall d _z_0123456789. (t ~ d, t ~ _z_0123456789) => Sing d -> Sing _z_0123456789 -> Sing (Apply (Apply Foo2Sym0 d) _z_0123456789 :: a) lambda d _z_0123456789 = applySing (singFun1 (Proxy :: Proxy (Apply (Apply Lambda_0123456789Sym0 d) _z_0123456789)) (\ sX_0123456789 -> let lambda :: forall x_0123456789. Sing x_0123456789 -> Sing (Apply (Apply (Apply Lambda_0123456789Sym0 d) _z_0123456789) x_0123456789) lambda x_0123456789 = case x_0123456789 of { SJust sY -> let lambda :: forall y. Apply JustSym0 y ~ x_0123456789 => Sing y -> Sing (Case_0123456789 d x_0123456789 _z_0123456789 (Apply JustSym0 y)) lambda y = y in lambda sY SNothing -> let lambda :: NothingSym0 ~ x_0123456789 => Sing (Case_0123456789 d x_0123456789 _z_0123456789 NothingSym0) lambda = d in lambda } :: Sing (Case_0123456789 d x_0123456789 _z_0123456789 x_0123456789) in lambda sX_0123456789)) (applySing (singFun1 (Proxy :: Proxy JustSym0) SJust) d) in lambda sD _s_z_0123456789 sFoo1 sD sX = let lambda :: forall d x. (t ~ d, t ~ x) => Sing d -> Sing x -> Sing (Apply (Apply Foo1Sym0 d) x :: a) lambda d x = applySing (singFun1 (Proxy :: Proxy (Apply (Apply Lambda_0123456789Sym0 d) x)) (\ sX_0123456789 -> let lambda :: forall x_0123456789. Sing x_0123456789 -> Sing (Apply (Apply (Apply Lambda_0123456789Sym0 d) x) x_0123456789) lambda x_0123456789 = case x_0123456789 of { SJust sY -> let lambda :: forall y. Apply JustSym0 y ~ x_0123456789 => Sing y -> Sing (Case_0123456789 d x x_0123456789 (Apply JustSym0 y)) lambda y = y in lambda sY SNothing -> let lambda :: NothingSym0 ~ x_0123456789 => Sing (Case_0123456789 d x x_0123456789 NothingSym0) lambda = d in lambda } :: Sing (Case_0123456789 d x x_0123456789 x_0123456789) in lambda sX_0123456789)) x in lambda sD sX