From 7881ee10b34d5947923bb8c19732709b7d9968ce Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Thu, 31 Dec 2020 17:01:46 +0000 Subject: 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. --- compiler/GHC/Tc/Errors.hs | 43 +++++++++++--------- compiler/GHC/Tc/Gen/Default.hs | 21 +++++++--- compiler/GHC/Tc/Solver.hs | 47 ++++++++++++++++++++-- docs/users_guide/exts/defer_type_errors.rst | 15 +++++-- testsuite/tests/ghci/scripts/T19158.script | 3 ++ testsuite/tests/ghci/scripts/T19158.stderr | 6 +++ testsuite/tests/ghci/scripts/all.T | 2 + testsuite/tests/typecheck/should_fail/T19142.hs | 20 +++++++++ .../tests/typecheck/should_fail/T19142.stderr | 13 ++++++ testsuite/tests/typecheck/should_fail/all.T | 1 + 10 files changed, 139 insertions(+), 32 deletions(-) create mode 100644 testsuite/tests/ghci/scripts/T19158.script create mode 100644 testsuite/tests/ghci/scripts/T19158.stderr create mode 100644 testsuite/tests/typecheck/should_fail/T19142.hs create mode 100644 testsuite/tests/typecheck/should_fail/T19142.stderr 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 `_). +- 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 @@ + +: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, ['']) -- cgit v1.2.1