Commit 4c0ec20d authored by Simon Peyton Jones's avatar Simon Peyton Jones

Test Trac #6035, #6036

parent f2d5b3ef
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators
#-}
module T6035 where
data Nat = Zero | Succ Nat
type family Sing (a :: k) :: k -> *
data SNat n where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
data SList (a :: [k]) where
SNil :: SList '[]
SCons :: Sing h h -> SList t -> SList (h ': t)
type instance Sing (a :: Nat) = SNat
type instance Sing (a :: [k]) = SList
nil :: SList '[]
nil = SNil
zero :: SList '[ '[] ]
zero = SCons SNil SNil
term :: SList '[ '[Zero], '[]]
term = SCons (SCons SZero SNil) (SCons SNil SNil)
{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs #-}
module T6036 where
data family Sing (a :: k)
data instance Sing (a :: Maybe k) where
SNothing :: Sing 'Nothing
SJust :: Sing b -> Sing ('Just b)
data Nat = Zero | Succ Nat
data instance Sing (a :: Nat) where
SZero :: Sing Zero
SSucc :: Sing n -> Sing (Succ n)
term = SJust SZero
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment