No deferred type errors under a forall

As Trac #14605 showed, we can't defer a type error under a
'forall' (when unifying two forall types).

The fix is simple.

5 files changed, 67 insertions, 10 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 6710434f29..e372c30971 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -378,16 +378,25 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
     implic' = implic { ic_skols = tvs'
                      , ic_given = map (tidyEvVar env1) given
                      , ic_info  = info' }
-    ctxt' = ctxt { cec_tidy     = env1
-                 , cec_encl     = implic' : cec_encl ctxt
-
-                 , cec_suppress = insoluble || cec_suppress ctxt
-                      -- Suppress inessential errors if there
-                      -- are insolubles anywhere in the
-                      -- tree rooted here, or we've come across
-                      -- a suppress-worthy constraint higher up (Trac #11541)
-
-                 , cec_binds    = evb }
+    ctxt1 | termEvidenceAllowed info = ctxt
+          | otherwise                = ctxt { cec_defer_type_errors = TypeError }
+          -- If we go inside an implication that has no term
+          -- evidence (i.e. unifying under a forall), we can't defer
+          -- type errors.  You could imagine using the /enclosing/
+          -- bindings (in cec_binds), but that may not have enough stuff
+          -- in scope for the bindings to be well typed.  So we just
+          -- switch off deferred type errors altogether.  See Trac #14605.
+
+    ctxt' = ctxt1 { cec_tidy     = env1
+                  , cec_encl     = implic' : cec_encl ctxt
+
+                  , cec_suppress = insoluble || cec_suppress ctxt
+                        -- Suppress inessential errors if there
+                        -- are insolubles anywhere in the
+                        -- tree rooted here, or we've come across
+                        -- a suppress-worthy constraint higher up (Trac #11541)
+
+                  , cec_binds    = evb }
 
     dead_givens = case status of
                     IC_Solved { ics_dead = dead } -> dead
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 03ea986de7..6704b87250 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -11231,6 +11231,29 @@ demonstrates:
     Prelude> fst x
     True
 
+Limitations of deferred type errors
+-----------------------------------
+The errors that can be deferred are:
+
+- Out of scope term variables
+- Equality constraints; e.g. `ord True` gives rise to an insoluble equality constraint `Char ~ Bool`, which can be deferred.
+- Type-class and implicit-parameter constraints
+
+All other type errors are reported immediately, and cannot be deferred; for
+example, an ill-kinded type signature, an instance declaration that is
+non-terminating or ill-formed, a type-family instance that does not
+obey the declared injectivity constraints, etc etc.
+
+In a few cases, even equality constraints cannot be deferred.  Specifically:
+
+- Kind-equalities cannot be deferred, e.g. ::
+
+    f :: Int Bool -> Char
+
+  This type signature contains a kind error which cannot be deferred.
+
+- Type equalities under a forall cannot be deferred (c.f. Trac #14605).
+
 .. _template-haskell:
 
 Template Haskell
diff --git a/testsuite/tests/typecheck/should_fail/T14605.hs b/testsuite/tests/typecheck/should_fail/T14605.hs
new file mode 100644
index 0000000000..4f75d59ebd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T14605.hs
@@ -0,0 +1,14 @@
+{-# Language TypeApplications #-}
+{-# Language ImpredicativeTypes #-}
+-- This isn't a test for impredicative types; it's
+-- just that visible type application on a for-all type
+-- is an easy way to provoke the error.
+--
+-- The ticket #14605 has a much longer example that
+-- also fails; it does not use ImpredicativeTypes
+
+module T14605 where
+
+import GHC.Prim (coerce)
+
+duplicate = coerce @(forall x. ()) @(forall x. x)
diff --git a/testsuite/tests/typecheck/should_fail/T14605.stderr b/testsuite/tests/typecheck/should_fail/T14605.stderr
new file mode 100644
index 0000000000..09181c6ee8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T14605.stderr
@@ -0,0 +1,10 @@
+
+T14605.hs:14:13: error:
+    • Couldn't match representation of type ‘x1’ with that of ‘()’
+        arising from a use of ‘coerce’
+      ‘x1’ is a rigid type variable bound by
+        the type ()
+        at T14605.hs:14:1-49
+    • In the expression: coerce @(forall x. ()) @(forall x. x)
+      In an equation for ‘duplicate’:
+          duplicate = coerce @(forall x. ()) @(forall x. x)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 2d8137f694..b8c3c4c1eb 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -464,3 +464,4 @@ test('T14390', normal, compile_fail, [''])
 test('MissingExportList03', normal, compile_fail, [''])
 test('T14618', normal, compile_fail, [''])
 test('T14607', normal, compile, [''])
+test('T14605', normal, compile_fail, [''])