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