Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T7908.hs
1 {-# LANGUAGE GADTs, InstanceSigs, DataKinds, PolyKinds, RankNTypes, LambdaCase #-}
2
3 module T7908 where
4
5 class Monad' (m :: (k -> *) -> *) where
6 return' :: c a -> m c
7 (>>>=) :: m c -> (forall a . c a -> m d) -> m d
8 (>>-) :: m c -> (forall a . c a -> d) -> d
9
10
11 data Nat = Z' | S' Nat
12
13 data Nat' (n :: Nat) where
14 Z :: Nat' Z'
15 S :: Nat' n -> Nat' (S' n)
16
17 data Hidden :: (k -> *) -> * where
18 Hide :: m a -> Hidden m
19
20 instance Monad' Hidden where
21 return' :: forall (c :: k -> *) (a :: k) . c a -> Hidden c
22 return' = Hide
23 (>>>=) :: forall (c :: k -> *) (d :: k -> *) . Hidden c -> (forall (a :: k) . c a -> Hidden d) -> Hidden d
24 Hide a >>>= f = f a
25 (>>-) :: forall (c :: k -> *) d . Hidden c -> (forall (a :: k) . c a -> d) -> d
26 Hide a >>- f = f a
27
28
29 int2nat' 0 = return' Z
30 int2nat' i = (int2nat' $ i - 1) >>>= (\n -> return' $ S n)
31
32
33 data Fin (m :: Nat) (n :: Nat) where
34 Fz :: Fin (S' m) Z'
35 Fs :: Fin m n -> Fin (S' m) (S' n)
36
37 -- N.B. not total!
38 nat2fin :: Nat' f -> Hidden Nat' -> Hidden (Fin f)
39 nat2fin (S _) (Hide Z) = return' Fz
40 nat2fin (S f) n = n >>>= (\case S n -> (nat2fin f (return' n) >>>= (\fn -> return' $ Fs fn)))
41
42 fin2int :: Hidden (Fin f) -> Int
43 fin2int f = f >>- go
44 where go :: Fin f n -> Int
45 go Fz = 0
46 go (Fs f) = 1 + go f
47
48
49 test = fin2int (nat2fin (S $ S Z) $ return' (S Z))