Ticket #7908: pr7908.hs

File pr7908.hs, 1.3 KB (added by heisenbug, 22 months ago)

reproduction testcase

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