### Add regression test for #9725

`Kind equalities saves the day!`
parent cb767542
 {-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds, FlexibleContexts, RankNTypes, ScopedTypeVariables #-} module T9725 where data En = M Bool class Kn (l :: En) instance Kn (M b) data Fac :: En -> * where Mo :: Kn (M b) => Fac (M b) data Fm :: * -> * where HiF :: Kn (ent b) => Fm (Fac (ent b)) -> Fm (O ent) MoF :: Kn (M b) => Fm (Fac (M b)) data O :: (k -> En) -> * where Hi :: Fac (ent k) -> O ent data Co :: (* -> *) -> * -> * where Ab :: (t -> f t) -> Co f t -- Restricted kind signature: --test :: forall (ent :: Bool -> En) . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) test :: forall ent . (forall i . Kn (ent i) => Fm (Fac (ent i))) -> Co Fm (O ent) test de = Ab h where h :: O ent -> Fm (O ent) h (Hi m@Mo) = HiF (d m) d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i)) d _ = de {- 9725.hs:27:25: Could not deduce (Kn (ent k1)) arising from a use of ‘HiF’ from the context (ent k1 ~ 'M b, Kn ('M b)) bound by a pattern with constructor Mo :: forall (b :: Bool). Kn ('M b) => Fac ('M b), in an equation for ‘h’ at 9725.hs:27:19-20 In the expression: HiF (d m) In an equation for ‘h’: h (Hi m@Mo) = HiF (d m) In an equation for ‘test’: test de = Ab h where h :: O ent -> Fm (O ent) h (Hi m@Mo) = HiF (d m) d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i)) d _ = de Failed, modules loaded: none. -}
 ... ... @@ -103,6 +103,7 @@ test('T9263', normal, run_command, ['\$MAKE -s --no-print-directory T9263']) test('T9063', normal, compile, ['']) test('T9200', normal, compile, ['']) test('T9200b', normal, compile_fail, ['']) test('T9725', normal, compile, ['']) test('T9750', normal, compile, ['']) test('T9569', normal, compile, ['']) test('T9838', normal, multimod_compile, ['T9838.hs','-v0']) ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!