blob: c89de8e73d570a69eb1f04ddc63c84aad971ec76 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators
#-}
module T6035 where
import Data.Kind (Type)
data Nat = Zero | Succ Nat
type family Sing (a :: k) :: k -> Type
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)
|
