Ticket #9725: 9725-RAE.hs

File 9725-RAE.hs, 2.0 KB (added by goldfire, 3 years ago)
Line 
1{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, FlexibleContexts, RankNTypes, ScopedTypeVariables,
2             ConstraintKinds #-}
3
4import Data.Proxy
5import Unsafe.Coerce
6
7data En = M Bool
8class Kn (l :: En)
9
10instance Kn (M b)
11
12data Fac :: En -> * where
13  Mo :: Kn (M b) => Proxy b -> Fac (M b)
14
15data Fm :: * -> * where
16  HiF :: Kn (ent b) => Fm (Fac (ent b)) -> Fm (O ent)
17  MoF :: Kn (M b) => Fm (Fac (M b))
18
19data O :: (k -> En) -> * where
20  Hi :: Fac (ent k) -> Proxy k -> O ent
21
22data Co :: (* -> *) -> * -> * where
23  Ab :: (t -> f t) -> Co f t
24
25-- Restricted kind signature:
26--test :: forall (ent :: Bool -> En) . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent)
27
28data Dict c where
29  Dict :: c => Dict c
30
31unsafeCoerceDict :: forall d_from d_to r. d_from => Proxy d_from -> Proxy d_to -> (d_to => r) -> r
32unsafeCoerceDict _ _ x = case unsafeCoerce (Dict :: Dict d_from) :: Dict d_to of Dict -> x
33
34test :: forall ent . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent)
35test de = Ab h
36    where h :: O ent -> Fm (O ent)
37          h (Hi m@(Mo (_ :: Proxy b)) (_ :: Proxy k1)) =
38                        unsafeCoerceDict (Proxy :: Proxy (Kn (M b)))
39                                         (Proxy :: Proxy (Kn (ent k1))) $
40                        HiF (d m)
41          d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i))
42          d _ = de
43
44{-
459725.hs:27:25:
46    Could not deduce (Kn (ent k1)) arising from a use of ‘HiF’
47    from the context (ent k1 ~ 'M b, Kn ('M b))
48      bound by a pattern with constructor
49                 Mo :: forall (b :: Bool). Kn ('M b) => Fac ('M b),
50               in an equation for ‘h’
51      at 9725.hs:27:19-20
52    In the expression: HiF (d m)
53    In an equation for ‘h’: h (Hi m@Mo) = HiF (d m)
54    In an equation for ‘test’:
55        test de
56          = Ab h
57          where
58              h :: O ent -> Fm (O ent)
59              h (Hi m@Mo) = HiF (d m)
60              d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i))
61              d _ = de
62Failed, modules loaded: none.
63-}