Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T7230.hs
1 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2 {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeFamilies #-}
3 {-# LANGUAGE TypeOperators, UndecidableInstances #-}
4 module T7230 where
5
6 data Nat = Zero | Succ Nat deriving (Show, Eq, Ord)
7
8 data family Sing (x :: k)
9
10 data instance Sing (n :: Nat) where
11 SZero :: Sing Zero
12 SSucc :: Sing n -> Sing (Succ n)
13
14 type SNat (n :: Nat) = Sing n
15
16 data instance Sing (b :: Bool) where
17 STrue :: Sing True
18 SFalse :: Sing False
19
20 type SBool (b :: Bool) = Sing b
21
22 data instance Sing (xs :: [k]) where
23 SNil :: Sing ('[] :: [k])
24 SCons :: Sing x -> Sing xs -> Sing (x ': xs)
25
26 type SList (xs :: [k]) = Sing (xs :: [k])
27
28 type family (:<<=) (n :: Nat) (m :: Nat) :: Bool
29 type instance Zero :<<= n = True
30 type instance Succ n :<<= Zero = False
31 type instance Succ n :<<= Succ m = n :<<= m
32
33 (%:<<=) :: SNat n -> SNat m -> SBool (n :<<= m)
34 SZero %:<<= _ = STrue
35 SSucc _ %:<<= SZero = SFalse
36 SSucc n %:<<= SSucc m = n %:<<= m
37
38 type family (b :: Bool) :&& (b' :: Bool) :: Bool
39 type instance True :&& b = b
40 type instance False :&& b = False
41
42 type family Increasing (xs :: [Nat]) :: Bool
43 type instance Increasing '[] = True
44 type instance Increasing '[n] = True
45 type instance Increasing (n ': m ': ns) = n :<<= m :&& Increasing (m ': ns)
46
47 crash :: (Increasing xs) ~ True => SList xs -> SBool (Increasing xs)
48 crash (SCons x (SCons y xs)) = x %:<<= y
49 crash _ = STrue