singletons-base-3.3: tests/compile-and-dump/Singletons/Error.golden
Singletons/Error.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| head :: [a] -> a
head (a : _) = a
head [] = error "head: empty list" |]
======>
head :: [a] -> a
head (a : _) = a
head [] = error "head: empty list"
type HeadSym0 :: (~>) [a] a
data HeadSym0 :: (~>) [a] a
where
HeadSym0KindInference :: SameKind (Apply HeadSym0 arg) (HeadSym1 arg) =>
HeadSym0 a0123456789876543210
type instance Apply HeadSym0 a0123456789876543210 = Head a0123456789876543210
instance SuppressUnusedWarnings HeadSym0 where
suppressUnusedWarnings = snd ((,) HeadSym0KindInference ())
type HeadSym1 :: [a] -> a
type family HeadSym1 (a0123456789876543210 :: [a]) :: a where
HeadSym1 a0123456789876543210 = Head a0123456789876543210
type Head :: [a] -> a
type family Head (a :: [a]) :: a where
Head ('(:) a _) = a
Head '[] = Apply ErrorSym0 "head: empty list"
sHead ::
(forall (t :: [a]). Sing t -> Sing (Apply HeadSym0 t :: a) :: Type)
sHead (SCons (sA :: Sing a) _) = sA
sHead SNil = sError (sing :: Sing "head: empty list")
instance SingI (HeadSym0 :: (~>) [a] a) where
sing = singFun1 @HeadSym0 sHead