Commit 298ec78c authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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.
parent bd438b2d
......@@ -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
......
......@@ -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
......
{-# 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)
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)
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment