Fix #14618 by applying a subst in deeplyInstantiate
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Tue, 26 Dec 2017 19:23:40 +0000 (14:23 -0500)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Tue, 26 Dec 2017 19:28:51 +0000 (14:28 -0500)
Previously, we were inexplicably not applying an instantiating
substitution to arguments in non-prenex types. It's amazing this
has been around for so long! I guess there aren't a lot of non-prenex
types around.

test case: typecheck/should_fail/T14618

compiler/typecheck/Inst.hs
testsuite/tests/typecheck/should_fail/T14618.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T14618.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T

index 6d656fe..9da96c4 100644 (file)
@@ -257,8 +257,9 @@ deeply_instantiate :: CtOrigin
 deeply_instantiate orig subst ty
   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
   = do { (subst', tvs') <- newMetaTyVarsX subst tvs
-       ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst' arg_tys)
-       ; let theta' = substTheta subst' theta
+       ; let arg_tys' = substTys   subst' arg_tys
+             theta'   = substTheta subst' theta
+       ; ids1  <- newSysLocalIds (fsLit "di") arg_tys'
        ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
        ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig
                                                 , text "type" <+> ppr ty
@@ -271,7 +272,7 @@ deeply_instantiate orig subst ty
                     <.> wrap2
                     <.> wrap1
                     <.> mkWpEvVarApps ids1,
-                 mkFunTys arg_tys rho2) }
+                 mkFunTys arg_tys' rho2) }
 
   | otherwise
   = do { let ty' = substTy subst ty
diff --git a/testsuite/tests/typecheck/should_fail/T14618.hs b/testsuite/tests/typecheck/should_fail/T14618.hs
new file mode 100644 (file)
index 0000000..da30d7a
--- /dev/null
@@ -0,0 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+
+module T14618 where
+
+safeCoerce :: a -> b
+safeCoerce = f'
+    where
+        f :: d -> forall c. d
+        f x = x
+
+        f' = f
diff --git a/testsuite/tests/typecheck/should_fail/T14618.stderr b/testsuite/tests/typecheck/should_fail/T14618.stderr
new file mode 100644 (file)
index 0000000..8faa64c
--- /dev/null
@@ -0,0 +1,23 @@
+
+T14618.hs:6:14: error:
+    • Couldn't match type ‘a’ with ‘b’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          safeCoerce :: forall a b. a -> b
+        at T14618.hs:5:1-20
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          safeCoerce :: forall a b. a -> b
+        at T14618.hs:5:1-20
+      Expected type: a -> b
+        Actual type: b -> b
+    • In the expression: f'
+      In an equation for ‘safeCoerce’:
+          safeCoerce
+            = f'
+            where
+                f :: d -> forall c. d
+                f x = x
+                f' = f
+    • Relevant bindings include
+        safeCoerce :: a -> b (bound at T14618.hs:6:1)
index 553e10a..b1a0e75 100644 (file)
@@ -462,3 +462,4 @@ test('T14325', normal, compile_fail, [''])
 test('T14350', normal, compile_fail, [''])
 test('T14390', normal, compile_fail, [''])
 test('MissingExportList03', normal, compile_fail, [''])
+test('T14618', normal, compile_fail, [''])