Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / indexed-types / should_compile / Numerals.hs
1 {-# LANGUAGE TypeFamilies #-}
2 {-# LANGUAGE EmptyDataDecls #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE TypeOperators #-}
5
6 module Numerals where
7
8 import Data.Kind
9
10 data Z -- empty data type
11 data S a -- empty data type
12
13 data SNat n where -- natural numbers as singleton type
14 Zero :: SNat Z
15 Succ :: SNat n -> SNat (S n)
16
17 zero = Zero
18 one = Succ zero
19 two = Succ one
20 three = Succ two
21 -- etc...we really would like some nicer syntax here
22
23 type family (:+:) n m :: Type
24 type instance Z :+: m = m
25 type instance (S n) :+: m = S (n :+: m)
26
27 add :: SNat n -> SNat m -> SNat (n :+: m)
28 add Zero m = m
29 add (Succ n) m = Succ (add n m)
30