T6036.hs 369 Bytes
Newer Older
Simon Peyton Jones's avatar
Simon Peyton Jones committed
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