blob: 7376271865ce15f1984f398133ced99aac0e9bf2 (
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
|
{-# LANGUAGE PolyKinds,
TypeFamilies,
GADTs,
DataKinds,
KindSignatures
#-}
module T5862 where
data Nat = Zero | Succ Nat
data SNat a where
SZero :: SNat 'Zero
SSucc :: SNat n -> SNat ('Succ n)
data SBool a where
SFalse :: SBool 'False
STrue :: SBool 'True
data SMaybe a where
SNothing :: SMaybe 'Nothing
SJust :: Sing a -> SMaybe ('Just a)
type family Sing (a :: k)
type instance Sing (a :: Nat) = SNat a
type instance Sing (a :: Bool) = SBool a
type instance Sing (a :: Maybe *) = SMaybe a -- want to say Maybe k
|
