Add regression test for Trac #15629
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 13 Sep 2018 11:56:09 +0000 (12:56 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 13 Sep 2018 11:56:09 +0000 (12:56 +0100)
testsuite/tests/typecheck/should_fail/T15629.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T15629.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T

diff --git a/testsuite/tests/typecheck/should_fail/T15629.hs b/testsuite/tests/typecheck/should_fail/T15629.hs
new file mode 100644 (file)
index 0000000..fdbba60
--- /dev/null
@@ -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 (file)
index 0000000..d3f0978
--- /dev/null
@@ -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)
index 64bc8cf..274dcc6 100644 (file)
@@ -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, [''])