blob: 4425c85cd510c287bf38c3660daa8cedd46b7636 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
{-# 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
|