[commit: ghc] master: Add regression test for #9725 (a02039c)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/a02039c7dcb4300b0aca80a994466a8f3039a3fc/ghc

>---------------------------------------------------------------

commit a02039c7dcb4300b0aca80a994466a8f3039a3fc
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date:   Tue Oct 3 10:10:39 2017 -0400

    Add regression test for #9725
    
    Kind equalities saves the day!


>---------------------------------------------------------------

a02039c7dcb4300b0aca80a994466a8f3039a3fc
 testsuite/tests/polykinds/T9725.hs | 51 ++++++++++++++++++++++++++++++++++++++
 testsuite/tests/polykinds/all.T    |  1 +
 2 files changed, 52 insertions(+)

diff --git a/testsuite/tests/polykinds/T9725.hs b/testsuite/tests/polykinds/T9725.hs
new file mode 100644
index 0000000..9a3d529
--- /dev/null
+++ b/testsuite/tests/polykinds/T9725.hs
@@ -0,0 +1,51 @@
+{-# 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 at 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 at Mo) = HiF (d m)
+    In an equation for ‘test’:
+        test de
+          = Ab h
+          where
+              h :: O ent -> Fm (O ent)
+              h (Hi m at Mo) = HiF (d m)
+              d :: Kn (ent i) => Fac (ent i) -> Fm (Fac (ent i))
+              d _ = de
+Failed, modules loaded: none.
+-}
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 0e5bcf1..fc7249e 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -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'])