Ticket #3484: absurd.hs

File absurd.hs, 1.4 KB (added by ryani, 5 years ago)
Line 
1{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, FlexibleContexts, ScopedTypeVariables #-}
2{-# OPTIONS_GHC -Wall #-}
3module Absurd where
4
5data Z = Z
6newtype S n = S n
7class Nat n where
8   caseNat :: (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> n -> r
9instance Nat Z
10instance Nat n => Nat (S n)
11   
12-- empty type
13newtype Naught = Naught (forall a. a)
14-- types are equal!
15data TEq a b where
16   TEq :: (a ~ b) => TEq a b
17
18type family NatEqProves m n
19type instance NatEqProves (S m) (S n) = TEq m n
20
21noConf :: (Nat m, Nat n) => m -> TEq m n -> NatEqProves m n
22noConf = undefined
23predEq :: TEq (S a) (S b) -> TEq a b
24predEq = undefined
25
26data IsEq a b = Yes (TEq a b) | No (TEq a b -> Naught)
27
28natEqDec :: forall m n. (Nat m, Nat n) => m -> n -> IsEq m n
29natEqDec m n = caseNat undefined mIsS m where
30    mIsS :: forall pm. (m ~ S pm, Nat pm) => pm -> IsEq m n
31    mIsS pm = caseNat undefined nIsS n where
32        nIsS :: forall pn. (n ~ S pn, Nat pn) => pn -> IsEq m n
33        nIsS pn = case natEqDec pm pn of
34            Yes TEq -> Yes TEq
35            No contr -> No (contr . noConf m)
36--            No contr -> No (contr . predEq)
37
38-- strange things:
39-- (1) commenting out the "Yes" case or changing it to "undefined" makes compilation succeed
40-- (2) replacing the "No" line with with the commented out "No" line makes compilation succeed