[commit: ghc] master: Add regression test for Trac #15629 (0d4f394)

[git at git.haskell.org]

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

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

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

commit 0d4f394810e13b4643f9361b6d2b3b29cb2d5003
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Thu Sep 13 12:56:09 2018 +0100

    Add regression test for Trac #15629


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

0d4f394810e13b4643f9361b6d2b3b29cb2d5003
 testsuite/tests/typecheck/should_fail/T15629.hs    | 27 +++++++++++++++
 .../tests/typecheck/should_fail/T15629.stderr      | 39 ++++++++++++++++++++++
 testsuite/tests/typecheck/should_fail/all.T        |  1 +
 3 files changed, 67 insertions(+)

diff --git a/testsuite/tests/typecheck/should_fail/T15629.hs b/testsuite/tests/typecheck/should_fail/T15629.hs
new file mode 100644
index 0000000..fdbba60
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15629.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug (f) where
+
+import Data.Kind
+import Data.Proxy
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family F x :: Type -> Type
+data F1Sym :: forall x a. x ~> F x a
+data F2Sym :: forall x a. F x a ~> x
+data Comp :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)
+
+sg :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
+      Proxy f -> Proxy g -> Proxy (Comp f g)
+sg _ _ = Proxy
+
+f :: forall (x :: Type). Proxy x -> ()
+f _ = ()
+  where
+    g :: forall ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+    g = sg Proxy Proxy
diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr
new file mode 100644
index 0000000..d3f0978
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15629.stderr
@@ -0,0 +1,39 @@
+
+T15629.hs:26:34: error:
+    • Expected kind ‘x1 ~> F x1 ab1’,
+        but ‘(F1Sym :: x ~> F x z)’ has kind ‘x1 ~> F x1 z’
+    • In the first argument of ‘Comp’, namely ‘(F1Sym :: x ~> F x z)’
+      In the first argument of ‘Proxy’, namely
+        ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’
+      In the type signature:
+        g :: forall ab.
+             Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+
+T15629.hs:27:9: error:
+    • Couldn't match kind ‘ab1’ with ‘z’
+      ‘ab1’ is a rigid type variable bound by
+        the type signature for:
+          g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym)
+        at T15629.hs:26:5-82
+      ‘z’ is a rigid type variable bound by
+        the type signature for:
+          g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym)
+        at T15629.hs:26:5-82
+      When matching types
+        f0 :: x ~> F x ab
+        F1Sym :: TyFun x1 (F x1 z) -> *
+      Expected type: Proxy (Comp F1Sym F2Sym)
+        Actual type: Proxy (Comp f0 F2Sym)
+    • In the expression: sg Proxy Proxy
+      In an equation for ‘g’: g = sg Proxy Proxy
+      In an equation for ‘f’:
+          f _
+            = ()
+            where
+                g ::
+                  forall ab.
+                  Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)
+                g = sg Proxy Proxy
+    • Relevant bindings include
+        g :: Proxy (Comp F1Sym F2Sym) (bound at T15629.hs:27:5)
+        f :: Proxy x1 -> () (bound at T15629.hs:24:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 64bc8cf..274dcc6 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -482,3 +482,4 @@ test('T15523', normal, compile_fail, ['-O'])
 test('T15527', normal, compile_fail, [''])
 test('T15552', normal, compile, [''])
 test('T15552a', normal, compile_fail, [''])
+test('T15629', normal, compile_fail, [''])