Fold integer-simple.git into ghc.git (re #8545)
[ghc.git] / testsuite / tests / polykinds / T6002.hs
1 -- This module should compile with -XIncoherentInstances, but didn't in 7.4
2
3
4 {- Here we define all the stuff that is needed for our singleton
5 types:
6 - phantom types (when GHC 7.4 arrives, the user-defined kinds)
7 - corresponding singleton types
8
9 These are basically the constructs from Omega,
10 reimplemented in Haskell for our purposes. -}
11
12 {-# LANGUAGE GADTs, KindSignatures, StandaloneDeriving,
13 RankNTypes, TypeFamilies, FlexibleInstances, IncoherentInstances #-}
14 module TypeMachinery where
15
16 -- The natural numbers:
17 -- o first the phantom types
18
19 data Z; data S n
20
21 -- o the using the above the singleton type Nat'
22
23 data Nat' :: * -> * where
24 Z :: Nat' Z
25 S :: Nat' n -> Nat' (S n)
26
27 deriving instance Show (Nat' a)
28
29 -- Type-level addition
30
31 type family Plus m n :: *
32 type instance Plus Z n = n
33 type instance Plus (S m) n = S (Plus m n)
34
35 -- Nat' addition
36
37 plus :: Nat' a -> Nat' b -> Nat' (Plus a b)
38 plus Z n = n
39 plus (S m) n = S (plus m n)
40
41 -- Equality on Nat'
42
43 sameNat' :: Nat' a -> Nat' b -> Bool
44 sameNat' Z Z = True
45 sameNat' (S m) (S n) = sameNat' m n
46 sameNat' _ _ = False
47
48 -- A data type for existentially hiding
49 -- (e.g.) Nat' values
50
51 data Hidden :: (* -> *) -> * where
52 Hide :: Show (a n) => a n -> Hidden a
53
54 deriving instance Show (Hidden t)
55
56 toNat' :: Integral i => i -> Hidden Nat'
57 toNat' 0 = Hide Z
58 toNat' n = case toNat' (n - 1) of
59 Hide n -> Hide (S n)
60
61 -- Now we are ready to make Hidden Nat' an Integral type
62
63 instance Eq (Hidden Nat') where
64 Hide a == Hide b = sameNat' a b
65
66 instance Ord (Hidden Nat') where
67 Hide Z `compare` Hide Z = EQ
68 Hide Z `compare` Hide _ = LT
69 Hide _ `compare` Hide Z = GT
70 Hide (S m) `compare` Hide (S n) = Hide m `compare` Hide n
71
72 instance Enum (Hidden Nat') where
73 toEnum = toEnum . fromIntegral
74 fromEnum = fromIntegral
75
76 instance Num (Hidden Nat') where
77 fromInteger = toNat'
78 signum (Hide Z) = 0
79 signum _ = 1
80 abs n = n
81 Hide a + Hide b = Hide $ plus a b
82 a * b = fromInteger $ toInteger a * toInteger b
83 negate a = error "negate(Hidden Nat')"
84
85 instance Real (Hidden Nat') where
86 toRational = toRational . toInteger
87
88 instance Integral (Hidden Nat') where
89 toInteger (Hide Z) = 0
90 toInteger (Hide (S n)) = 1 + toInteger (Hide n)
91 quotRem a b = let (a', b') = toInteger a `quotRem` toInteger b in (fromInteger a', fromInteger b')
92
93 -- McBride's Fin data type. By counting backwards from the
94 -- result index, it only admits a fixed number of inhabitants.
95
96 data Fin :: * -> * where
97 Stop :: Fin (S Z)
98 Retreat :: Fin s -> Fin (S s)
99
100 deriving instance Show (Fin a)
101