singletons-2.7: tests/compile-and-dump/Singletons/T367.golden
Singletons/T367.hs:(0,0)-(0,0): Splicing declarations
singletonsOnly
[d| const' :: a -> b -> a
const' x _ = x |]
======>
type Const'Sym0 :: (~>) a ((~>) b a)
data Const'Sym0 a0123456789876543210
where
Const'Sym0KindInference :: SameKind (Apply Const'Sym0 arg) (Const'Sym1 arg) =>
Const'Sym0 a0123456789876543210
type instance Apply Const'Sym0 a0123456789876543210 = Const'Sym1 a0123456789876543210
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Const'Sym0 where
Data.Singletons.SuppressUnusedWarnings.suppressUnusedWarnings
= snd (((,) Const'Sym0KindInference) ())
type Const'Sym1 :: a -> (~>) b a
data Const'Sym1 a0123456789876543210 a0123456789876543210
where
Const'Sym1KindInference :: SameKind (Apply (Const'Sym1 a0123456789876543210) arg) (Const'Sym2 a0123456789876543210 arg) =>
Const'Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (Const'Sym1 a0123456789876543210) a0123456789876543210 = Const'Sym2 a0123456789876543210 a0123456789876543210
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Const'Sym1 a0123456789876543210) where
Data.Singletons.SuppressUnusedWarnings.suppressUnusedWarnings
= snd (((,) Const'Sym1KindInference) ())
type Const'Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) =
Const' a0123456789876543210 a0123456789876543210 :: a
type Const' :: a -> b -> a
type family Const' a a where
Const' x _ = x
sConst' ::
forall a b (t :: a) (t :: b).
Sing t -> Sing t -> Sing (Apply (Apply Const'Sym0 t) t :: a)
sConst' (sX :: Sing x) _ = sX
instance SingI (Const'Sym0 :: (~>) a ((~>) b a)) where
sing = (singFun2 @Const'Sym0) sConst'
instance SingI d => SingI (Const'Sym1 (d :: a) :: (~>) b a) where
sing = (singFun1 @(Const'Sym1 (d :: a))) (sConst' (sing @d))