Ticket #9725: 9725.hs

File 9725.hs, 1.5 KB (added by heisenbug, 3 years ago)

Simplified reproduction testcase

Line 
1{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, FlexibleContexts, RankNTypes, ScopedTypeVariables #-}
2
3data En = M Bool
4class Kn (l :: En)
5
6instance Kn (M b)
7
8data Fac :: En -> * where
9  Mo :: Kn (M b) => Fac (M b)
10
11data Fm :: * -> * where
12  HiF :: Kn (ent b) => Fm (Fac (ent b)) -> Fm (O ent)
13  MoF :: Kn (M b) => Fm (Fac (M b))
14
15data O :: (k -> En) -> * where
16  Hi :: Fac (ent k) -> O ent
17
18data Co :: (* -> *) -> * -> * where
19  Ab :: (t -> f t) -> Co f t
20
21-- Restricted kind signature:
22--test :: forall (ent :: Bool -> En) . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent)
23
24test :: forall ent . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent)
25test de = Ab h
26    where h :: O ent -> Fm (O ent)
27          h (Hi m@Mo) = HiF (d m)
28          d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i))
29          d _ = de
30
31{-
329725.hs:27:25:
33    Could not deduce (Kn (ent k1)) arising from a use of ‘HiF’
34    from the context (ent k1 ~ 'M b, Kn ('M b))
35      bound by a pattern with constructor
36                 Mo :: forall (b :: Bool). Kn ('M b) => Fac ('M b),
37               in an equation for ‘h’
38      at 9725.hs:27:19-20
39    In the expression: HiF (d m)
40    In an equation for ‘h’: h (Hi m@Mo) = HiF (d m)
41    In an equation for ‘test’:
42        test de
43          = Ab h
44          where
45              h :: O ent -> Fm (O ent)
46              h (Hi m@Mo) = HiF (d m)
47              d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i))
48              d _ = de
49Failed, modules loaded: none.
50-}