blob: 8c10746f377af2c4d0f36ee84b0f6f4976c54315 (
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
|
{-# LANGUAGE DataKinds, TypeFamilies #-}
module OrdErr where
import GHC.TypeNats
import Data.Proxy
proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()
proxyInEq _ _ = ()
-- Throws an error
proxyInEq1 :: Proxy a -> Proxy (a+1) -> ()
proxyInEq1 = proxyInEq
-- Throws an error
proxyInEq2 :: Proxy 5 -> Proxy 3 -> ()
proxyInEq2 = proxyInEq
-- No error
proxyInEq3 :: Proxy 3 -> Proxy 4 -> ()
proxyInEq3 = proxyInEq
-- No error
proxyInEq4 :: (a <=? (a + 1)) ~ True => Proxy a -> Proxy (a + 1) -> ()
proxyInEq4 = proxyInEq
-- No error
proxyInEq5 :: (a <= (a + 1)) => Proxy a -> Proxy (a + 1) -> ()
proxyInEq5 = proxyInEq
-- No error
proxyInEq6 :: (CmpNat a (a + 1) ~ EQ) => Proxy a -> Proxy (a + 1) -> ()
proxyInEq6 = proxyInEq
-- No error
proxyInEq7 :: (CmpNat a (a + 1) ~ LT) => Proxy a -> Proxy (a + 1) -> ()
proxyInEq7 = proxyInEq
|
