Ticket #9725: 9725-GGR.hs

File 9725-GGR.hs, 1.6 KB (added by heisenbug, 2 years ago)

Now with a new (T i) type in kind En

Line 
1{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, FlexibleContexts, RankNTypes, ScopedTypeVariables,
2             ConstraintKinds, StandaloneDeriving #-}
3
4import Data.Proxy
5import GHC.TypeLits
6import Unsafe.Coerce
7
8data En = M Bool | T Nat
9
10class Kn (l :: En)
11instance Kn (M b)
12instance Kn (T i)
13
14data Fac :: En -> * where
15  Mo :: Kn (M b) => Proxy b -> Fac (M b)
16  Od :: Kn (T i) => Proxy i -> Fac (T i)
17
18deriving instance Show (Fac e)
19
20data Fm :: * -> * where
21  HiF :: Kn (ent b) => Fm (Fac (ent b)) -> Fm (O ent)
22  MoF :: Kn (M b) => Fm (Fac (M b))
23  OdF :: Kn (T i) => Fm (Fac (T i))
24
25deriving instance Show (Fm a)
26
27data O :: (k -> En) -> * where
28  Hi :: Fac (ent k) -> Proxy k -> O ent
29
30data Co :: (* -> *) -> * -> * where
31  Ab :: (t -> f t) -> Co f t
32
33
34data Dict c where
35  Dict :: c => Dict c
36
37unsafeCoerceDict :: forall d_from d_to r. d_from => Proxy d_from -> Proxy d_to -> (d_to => r) -> r
38unsafeCoerceDict _ _ x = case unsafeCoerce (Dict :: Dict d_from) :: Dict d_to of Dict -> x
39
40test :: forall ent . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent)
41test de = Ab h
42    where h :: O ent -> Fm (O ent)
43          h (Hi m@(Mo (_ :: Proxy b)) (_ :: Proxy k1)) =
44                        unsafeCoerceDict (Proxy :: Proxy (Kn (M b)))
45                                         (Proxy :: Proxy (Kn (ent k1))) $
46                        HiF (d m)
47          h (Hi o@(Od (_ :: Proxy i)) (_ :: Proxy k1)) =
48                        unsafeCoerceDict (Proxy :: Proxy (Kn (T i)))
49                                         (Proxy :: Proxy (Kn (ent k1))) $
50                        HiF (d o)
51          d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i))
52          d _ = de
53