summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2020-12-31 17:01:46 +0000
committerMarge Bot <ben+marge-bot@smart-cactus.org>2021-01-22 15:00:07 -0500
commit34950fb84b85d964e30ae9eca995b84fbf4fd165 (patch)
tree06a51660ddfe8a9504d4483f167e1de451ad86f6
parenta255b4e38918065ac028789872e53239ac30ae1a (diff)
downloadhaskell-34950fb84b85d964e30ae9eca995b84fbf4fd165.tar.gz
Fix error recovery in solveEqualities
As #19142 showed, with -fdefer-type-errors we were allowing compilation to proceed despite a fatal kind error. This patch fixes it, as described in the new note in GHC.Tc.Solver, Note [Wrapping failing kind equalities] Also fixes #19158 Also when checking default( ty1, ty2, ... ) only consider a possible default (C ty2) if ty2 is kind-compatible with C. Previously we could form kind-incompatible constraints, with who knows what kind of chaos resulting. (Actually, no chaos results, but that's only by accident. It's plain wrong to form the constraint (Num Either) for example.) I just happened to notice this during fixing #19142.
-rw-r--r--compiler/GHC/Tc/Errors.hs43
-rw-r--r--compiler/GHC/Tc/Gen/Default.hs21
-rw-r--r--compiler/GHC/Tc/Solver.hs47
-rw-r--r--docs/users_guide/exts/defer_type_errors.rst15
-rw-r--r--testsuite/tests/ghci/scripts/T19158.script3
-rw-r--r--testsuite/tests/ghci/scripts/T19158.stderr6
-rwxr-xr-xtestsuite/tests/ghci/scripts/all.T2
-rw-r--r--testsuite/tests/typecheck/should_fail/T19142.hs20
-rw-r--r--testsuite/tests/typecheck/should_fail/T19142.stderr13
-rw-r--r--testsuite/tests/typecheck/should_fail/all.T1
10 files changed, 139 insertions, 32 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 4f7c9dfea2..f6bb5f7d42 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -167,7 +167,6 @@ reportUnsolved wanted
-- See Note [Deferring coercion errors to runtime]
-- Used by solveEqualities for kind equalities
-- (see Note [Fail fast on kind errors] in "GHC.Tc.Solver")
--- and for simplifyDefault.
reportAllUnsolved :: WantedConstraints -> TcM ()
reportAllUnsolved wanted
= do { ev_binds <- newNoTcEvBinds
@@ -378,15 +377,30 @@ deferringAnyBindings (CEC { cec_defer_type_errors = TypeError
, cec_out_of_scope_holes = HoleError }) = False
deferringAnyBindings _ = True
--- | Transforms a 'ReportErrCtxt' into one that does not defer any bindings
--- at all.
-noDeferredBindings :: ReportErrCtxt -> ReportErrCtxt
-noDeferredBindings ctxt = ctxt { cec_defer_type_errors = TypeError
- , cec_expr_holes = HoleError
- , cec_out_of_scope_holes = HoleError }
-
-{- Note [Suppressing error messages]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+maybeSwitchOffDefer :: EvBindsVar -> ReportErrCtxt -> ReportErrCtxt
+-- Switch off defer-type-errors inside CoEvBindsVar
+-- See Note [Failing equalities with no evidence bindings]
+maybeSwitchOffDefer evb ctxt
+ | CoEvBindsVar{} <- evb
+ = ctxt { cec_defer_type_errors = TypeError
+ , cec_expr_holes = HoleError
+ , cec_out_of_scope_holes = HoleError }
+ | otherwise
+ = ctxt
+
+{- Note [Failing equalities with no evidence bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we go inside an implication that has no term evidence
+(e.g. 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 #14605.
+
+This is done by maybeSwitchOffDefer. It's also useful in one other
+place: see Note [Wrapping failing kind equalities] in GHC.Tc.Solver.
+
+Note [Suppressing error messages]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The cec_suppress flag says "don't report any errors". Instead, just create
evidence bindings (as usual). It's used when more important errors have occurred.
@@ -445,15 +459,8 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs
implic' = implic { ic_skols = tvs'
, ic_given = map (tidyEvVar env1) given
, ic_info = info' }
- ctxt1 | CoEvBindsVar{} <- evb = noDeferredBindings ctxt
- | otherwise = ctxt
- -- If we go inside an implication that has no term
- -- evidence (e.g. 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 #14605.
+ ctxt1 = maybeSwitchOffDefer evb ctxt
ctxt' = ctxt1 { cec_tidy = env1
, cec_encl = implic' : cec_encl ctxt
diff --git a/compiler/GHC/Tc/Gen/Default.hs b/compiler/GHC/Tc/Gen/Default.hs
index d37f26df40..c8106858b9 100644
--- a/compiler/GHC/Tc/Gen/Default.hs
+++ b/compiler/GHC/Tc/Gen/Default.hs
@@ -12,6 +12,8 @@ import GHC.Prelude
import GHC.Hs
import GHC.Core.Class
+import GHC.Core.Type ( typeKind )
+import GHC.Types.Var( tyVarKind )
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Env
import GHC.Tc.Gen.HsType
@@ -82,13 +84,20 @@ tc_default_ty deflt_clss hs_ty
; return ty }
check_instance :: Type -> Class -> TcM Bool
- -- Check that ty is an instance of cls
- -- We only care about whether it worked or not; return a boolean
+-- Check that ty is an instance of cls
+-- We only care about whether it worked or not; return a boolean
+-- This checks that cls :: k -> Constraint
+-- with just one argument and no polymorphism; if we need to add
+-- polymorphism we can make it more complicated. For now we are
+-- concerned with classes like
+-- Num :: Type -> Constraint
+-- Foldable :: (Type->Type) -> Constraint
check_instance ty cls
- = do { (_, success) <- discardErrs $
- askNoErrs $
- simplifyDefault [mkClassPred cls [ty]]
- ; return success }
+ | [cls_tv] <- classTyVars cls
+ , tyVarKind cls_tv `tcEqType` typeKind ty
+ = simplifyDefault [mkClassPred cls [ty]]
+ | otherwise
+ = return False
defaultDeclCtxt :: SDoc
defaultDeclCtxt = text "When checking the types in a default declaration"
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 991708111d..2d97b84e9d 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -218,7 +218,13 @@ simplifyAndEmitFlatConstraints wanted
; traceTc "emitFlatConstraints {" (ppr wanted)
; case floatKindEqualities wanted of
Nothing -> do { traceTc "emitFlatConstraints } failing" (ppr wanted)
- ; emitConstraints wanted -- So they get reported!
+ -- Emit the bad constraints, wrapped in an implication
+ -- See Note [Wrapping failing kind equalities]
+ ; tclvl <- TcM.getTcLevel
+ ; implic <- buildTvImplication UnkSkol [] tclvl wanted
+ -- UnkSkol: doesn't matter, because
+ -- we bind no skolem varaibles here
+ ; emitImplication implic
; failM }
Just (simples, holes)
-> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples)
@@ -376,6 +382,40 @@ All this is done:
See also #18062, #11506
+Note [Wrapping failing kind equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In simplifyAndEmitFlatConstraints, if we fail to get down to simple
+flat constraints we will
+* re-emit the constraints so that they are reported
+* fail in the monad
+But there is a Terrible Danger that, if -fdefer-type-errors is on, and
+we just re-emit an insoluble constraint like (* ~ (*->*)), that we'll
+report only a warning and proceed with compilation. But if we ever fail
+in the monad it should be fatal; we should report an error and stop after
+the type checker. If not, chaos results: #19142.
+
+Our solution is this:
+* Even with -fdefer-type-errors, inside an implication with no place for
+ value bindings (ic_binds = CoEvBindsVar), report failing equalities as
+ errors. We have to do this anyway; see GHC.Tc.Errors
+ Note [Failing equalities with no evidence bindings].
+
+* Right here in simplifyAndEmitFlatConstraints, use buildTvImplication
+ to wrap the failing constraint in a degenerate implication (no
+ skolems, no theta, no bumped TcLevel), with ic_binds = CoEvBindsVar.
+ That way any failing equalities will lead to an error not a warning,
+ irrespective of -fdefer-type-errors.
+
+ This is a slight hack, because the implication doesn't have a bumped
+ TcLevel, but that doesn't matter.
+
+We re-emit the implication rather than reporting the errors right now,
+so that the error mesages are improved by other solving and defaulting.
+e.g. we prefer
+ Cannot match 'Type->Type' with 'Type'
+to Cannot match 'Type->Type' with 'TYPE r0'
+
+
Note [floatKindEqualities vs approximateWC]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
floatKindEqualities and approximateWC are strikingly similar to each
@@ -757,13 +797,12 @@ simplifyInteractive wanteds
------------------
simplifyDefault :: ThetaType -- Wanted; has no type variables in it
- -> TcM () -- Succeeds if the constraint is soluble
+ -> TcM Bool -- Return if the constraint is soluble
simplifyDefault theta
= do { traceTc "simplifyDefault" empty
; wanteds <- newWanteds DefaultOrigin theta
; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
- ; reportAllUnsolved unsolved
- ; return () }
+ ; return (isEmptyWC unsolved) }
------------------
tcCheckSatisfiability :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)
diff --git a/docs/users_guide/exts/defer_type_errors.rst b/docs/users_guide/exts/defer_type_errors.rst
index 146fc01760..1c644c5eda 100644
--- a/docs/users_guide/exts/defer_type_errors.rst
+++ b/docs/users_guide/exts/defer_type_errors.rst
@@ -99,7 +99,7 @@ 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.
+- 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
@@ -107,15 +107,22 @@ 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:
+In a few cases, equality constraints cannot be deferred. Specifically:
-- Kind-equalities cannot be deferred, e.g. ::
+- Kind errors in a type or kind signature, partial type signatures, or pattern signature.
+ 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. `#14605
+- Type equalities under a forall (c.f. `#14605
<https://gitlab.haskell.org/ghc/ghc/issues/14605>`_).
+- Kind errors in a visible type application. e.g. ::
+ reverse @Maybe xs
+
+- Kind errors in a ``default`` declaration. e.g. ::
+
+ default( Double, Int Int )
diff --git a/testsuite/tests/ghci/scripts/T19158.script b/testsuite/tests/ghci/scripts/T19158.script
new file mode 100644
index 0000000000..81d392cf43
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T19158.script
@@ -0,0 +1,3 @@
+:set -fdefer-type-errors
+:set -XTypeApplications
+:t id @Maybe
diff --git a/testsuite/tests/ghci/scripts/T19158.stderr b/testsuite/tests/ghci/scripts/T19158.stderr
new file mode 100644
index 0000000000..9b15a102e8
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T19158.stderr
@@ -0,0 +1,6 @@
+
+<interactive>:1:5: error:
+ • Expecting one more argument to ‘Maybe’
+ Expected a type, but ‘Maybe’ has kind ‘* -> *’
+ • In the type ‘Maybe’
+ In the expression: id @Maybe
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index f5c1a4ca39..08a6c4ee6a 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -327,3 +327,5 @@ test('T18644', normal, ghci_script, ['T18644.script'])
test('T18755', normal, ghci_script, ['T18755.script'])
test('T18828', normal, ghci_script, ['T18828.script'])
test('T19197', normal, ghci_script, ['T19197.script'])
+test('T19158', normal, ghci_script, ['T19158.script'])
+
diff --git a/testsuite/tests/typecheck/should_fail/T19142.hs b/testsuite/tests/typecheck/should_fail/T19142.hs
new file mode 100644
index 0000000000..6c49498efa
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19142.hs
@@ -0,0 +1,20 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+{-# LANGUAGE ExplicitForAll
+ , TypeApplications
+ , KindSignatures
+ , ScopedTypeVariables
+#-}
+
+module T19142 where
+
+-- Both these examples gave Lint errors
+-- NB: the -fdefer-type-errors at the top!!
+
+-- Example 1
+f (x :: Maybe Maybe) = x
+
+-- Example 2
+foo :: forall (f :: * -> *) . String
+foo = ""
+
+g x = foo @Int
diff --git a/testsuite/tests/typecheck/should_fail/T19142.stderr b/testsuite/tests/typecheck/should_fail/T19142.stderr
new file mode 100644
index 0000000000..fc94a4166f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19142.stderr
@@ -0,0 +1,13 @@
+
+T19142.hs:14:15: error:
+ • Expecting one more argument to ‘Maybe’
+ Expected a type, but ‘Maybe’ has kind ‘* -> *’
+ • In the first argument of ‘Maybe’, namely ‘Maybe’
+ In the type ‘Maybe Maybe’
+ In a pattern type signature: Maybe Maybe
+
+T19142.hs:20:12: error:
+ • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
+ • In the type ‘Int’
+ In the expression: foo @Int
+ In an equation for ‘g’: g x = foo @Int
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 76f99f81c6..e191a736aa 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -612,3 +612,4 @@ test('TyAppPat_ScopedTyVarConflict', normal, compile_fail, [''])
test('TyAppPat_TooMany', normal, compile_fail, [''])
test('T12178a', normal, compile_fail, [''])
test('T18869', normal, compile_fail, [''])
+test('T19142', normal, compile_fail, [''])