Simon Peyton Jones pushed to branch wip/T27731 at Glasgow Haskell Compiler / GHC

Commits:

7 changed files:

Changes:

  • changelog.d/T27731
    1 
    +section: compiler
    2 
    +synopsis: Fix a compiler crash after typechecking
    3 
    +issues: #27731
    4 
    +mrs: !16564
    5 
    +description: {
    6 
    +  The type checker was failing to report an error, even though it had found one,
    7 
    +  due to over-zealous error suppression. That led to subsequent chaos. This
    8 
    +  MR fixes it *and* simplifies the code.
    9 
    +
    10 
    +  Claude found a second, closely-related bug, now immortalised as test ``T18851d``.
    11 
    +}

  • compiler/GHC/Tc/Errors.hs
    ... ... @@ -263,11 +263,11 @@ report_unsolved type_errors expr_holes
    263 263 
                                 , cec_type_holes = type_holes
    264 264 
                                 , cec_out_of_scope_holes = out_of_scope_holes
    265 265 
                                 , cec_suppress = insolubleWC wanted
    266 
    -                                 -- See Note [Suppressing error messages]
    267 
    -                                 -- Suppress low-priority errors if there
    268 
    -                                 -- are insoluble errors anywhere;
    269 
    -                                 -- See #15539 and c.f. setting ic_status
    270 
    -                                 -- in GHC.Tc.Solver.setImplicationStatus
    266 
    +                              -- See (SLIE1) in
    267 
    +                              -- Note [cec_suppress: suppressing less-important error messages]
    268 
    +                              -- Suppress low-priority errors if there are insoluble errors
    269 
    +                              -- anywhere in the treee. See #15539 and c.f. setting ic_status
    270 
    +                              -- in GHC.Tc.Solver.setImplicationStatus
    271 271 
                                 , cec_warn_redundant = warn_redundant
    272 272 
                                 , cec_expand_syns = exp_syns
    273 273 
                                 , cec_binds    = binds_var }
    ... ... @@ -322,30 +322,123 @@ we just switch off deferred type errors altogether. See #14605.
    322 322 
     This is done by maybeSwitchOffDefer.  It's also useful in one other
    323 323 
     place: see Note [Wrapping failing kind equalities] in GHC.Tc.Solver.
    324 324
    325 
    -Note [Suppressing error messages]
    326 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    327 
    -The cec_suppress flag says "don't report any errors".  Instead, just create
    328 
    -evidence bindings (as usual).  It's used when more important errors have occurred.
    329 
    -
    330 
    -Specifically (see reportWanteds)
    331 
    -  * If there are insoluble Givens, then we are in unreachable code and all bets
    332 
    -    are off.  So don't report any further errors.
    333 
    -  * If there are any insolubles (eg Int~Bool), here or in a nested implication,
    334 
    -    then suppress errors from the simple constraints here.  Sometimes the
    335 
    -    simple-constraint errors are a knock-on effect of the insolubles.
    336 
    -
    337 
    -This suppression behaviour is controlled by the Bool flag in
    338 
    -ReportErrorSpec, as used in reportWanteds.
    339 
    -
    340 
    -But we need to take care: flags can turn errors into warnings, and we
    341 
    -don't want those warnings to suppress subsequent errors (including
    342 
    -suppressing the essential addTcEvBind for them: #15152). So in
    343 
    -tryReporter we use askNoErrs to see if any error messages were
    344 
    -/actually/ produced; if not, we don't switch on suppression.
    345 
    -
    346 
    -A consequence is that warnings never suppress warnings, so turning an
    347 
    -error into a warning may allow subsequent warnings to appear that were
    348 
    -previously suppressed.   (e.g. partial-sigs/should_fail/T14584)
    325 
    +Note [cec_suppress: suppressing less-important error messages]
    326 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    327 
    +The cec_suppress flag says "don't report any less-important errors".  Instead, just create
    328 
    +evidence bindings (as usual).  It's used when more important errors have occurred
    329 
    +(or will occur) eleswhere.
    330 
    +
    331 
    +(SLIE0)
    332 
    +  * Note that `cec_suppress` does not affect more-important errors, namely the `report1`
    333 
    +    group in `reportWanteds`
    334 
    +  * But `cec_suppress` /does/ affect the less-important errors, namely the `report2` group.
    335 
    +  To see this, look at the plumbing of cec suppress in `reportWanteds`
    336 
    +
    337 
    +(SLIE1) When we begin `reportAllUnsolved` we set `cec_suppress` if there are insoluble
    338 
    +  wanteds /anywhere/ in the tree, via `insolubleWC`.  That means we'll suppress all
    339 
    +  less-important errors in favour of the more important (insolbule) ones
    340 
    +
    341 
    +(SLIE2) But we need to take care: flags can turn errors into warnings, and we
    342 
    +  don't want those warnings to suppress subsequent errors (including
    343 
    +  suppressing the essential addTcEvBind for them: #15152). So in
    344 
    +  tryReporter we use askNoErrs to see if any error messages were
    345 
    +  /actually/ produced; if not, we don't switch on suppression.
    346 
    +
    347 
    +  A consequence is that warnings never suppress warnings, so turning an
    348 
    +  error into a warning may allow subsequent warnings to appear that were
    349 
    +  previously suppressed.   (e.g. partial-sigs/should_fail/T14584)
    350 
    +
    351 
    +(SLIE3) There is a tricky interaction between
    352 
    +   * `cec_suppress` (a global flag) and
    353 
    +   * `ei_suppress` (a local, per-error-item flag),
    354 
    +     see Note [ei_suppresss: suppressing confusing errors]
    355 
    +   Suppose cec_suppress is True because of an insoluble constraint arising from a
    356 
    +   superclass constraint -- this constraint will have ei_suppress=True.
    357 
    +
    358 
    +
    359 
    +
    360 
    +Note [ei_suppresss: suppressing confusing errors]
    361 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    362 
    +Certain errors we might encounter are potentially confusing to users.
    363 
    +If there are any other errors to report, at all, we want to suppress these.
    364 
    +We achieve this by setting the `ei_suppress` flag in the `ErrorItem`.
    365 
    +
    366 
    +Which errors should be suppressed?
    367 
    +
    368 
    +(SCE1) Non-empty rewriter sets.  See Note [Wanteds rewrite Wanteds: rewriter-sets]
    369 
    +   in  GHC.Tc.Types.Constraint
    370 
    +
    371 
    +(SCE2) Superclasses of Wanteds.  These are generated only in case they trigger functional
    372 
    +   dependencies.  If such a constraint is unsolved, then its "parent" constraint must
    373 
    +   also be unsolved, and is much more informative to the user.  Example (#26255):
    374 
    +        class (MinVersion <= F era) => Era era where { ... }
    375 
    +        f :: forall era. EraFamily era -> IO ()
    376 
    +        f = ..blah...   -- [W] Era era
    377 
    +   Here we have simply omitted "Era era =>" from f's type.  But we'll end up with
    378 
    +   /two/ Wanted constraints:
    379 
    +        [W] d1 :  Era era
    380 
    +        [W] d2 : MinVersion <= F era  -- Superclass of d1
    381 
    +   We definitely want to report d1 and not d2!  Happily it's easy to filter out those
    382 
    +   superclass-Wanteds, becuase their Origin betrays them.
    383 
    +
    384 
    +There are wrinkles
    385 
    +
    386 
    +(SCE3) In rare cases we may suppress /all/ errors. That is catastrophic: GHC proceeds
    387 
    +  to desugar and optimise the program, even though it is full of type errors (#22702,
    388 
    +  #22793), and/or we fail to bind evidence (#27731).
    389 
    +
    390 
    +  If this happens, unless we are sure that an error will be reported some other way
    391 
    +  (details in the defn of `tidy_items` in `reportWanteds), we just un-suppress the lot,
    392 
    +  which is brutal but safe.  It's a rare case.
    393 
    +
    394 
    +   How can it happen that there are /all/ errors are suppressed?
    395 
    +   * See test T18851 for an example of how it is (just, barely) possible for the
    396 
    +     /only/ errors to be superclass-of-Wanted constraints.
    397 
    +   * Similarly #27731, which also involves a superclass-of-Wanted:
    398 
    +          class (a ~ F b) => Ren a b
    399 
    +     If we have a [W] Ren a b, we'll emit the superclass [W] a ~ F b, which will
    400 
    +     rewrite the original class constraint to [W] Ren (F b) b.  Now we have two
    401 
    +     constraints: one has a non-empty rewriter set (SEC1) and one is a superclass of
    402 
    +     a Wanted (SEC2).
    403 
    +   * Also see Wrinkle (PER2) in Note [Prioritise Wanteds with empty
    404 
    +     CoHoleSet] in GHC.Tc.Types.Constraint.
    405 
    +
    406 
    +Historical note.  We used to suppress errors arising from the interaction of two
    407 
    +   fundep constraints.  But nowadays fundep constraints never "escape" into the main
    408 
    +   solver and so never show up in error messages.  See (SOLVE-FD) in Note [Overview
    409 
    +   of functional dependencies in type inference] in GHC.Tc.Solver.FunDeps.  So this
    410 
    +   wrinkle is now just a historical note.
    411 
    +
    412 
    +   Errors which arise from the interaction of two Wanted fun-dep constraints.
    413 
    +   Example:
    414 
    +
    415 
    +     class C a b | a -> b where
    416 
    +       op :: a -> b -> b
    417 
    +
    418 
    +     foo _ = op True Nothing
    419 
    +
    420 
    +     bar _ = op False []
    421 
    +
    422 
    +   Here, we could infer
    423 
    +     foo :: C Bool (Maybe a) => p -> Maybe a
    424 
    +     bar :: C Bool [a]       => p -> [a]
    425 
    +
    426 
    +   (The unused arguments suppress the monomorphism restriction.) The problem
    427 
    +   is that these types can't both be correct, as they violate the functional
    428 
    +   dependency. Yet reporting an error here is awkward: we must
    429 
    +   non-deterministically choose either foo or bar to reject. We thus want
    430 
    +   to report this problem only when there is nothing else to report.
    431 
    +   See typecheck/should_fail/T13506 for an example of when to suppress
    432 
    +   the error. The case above is actually accepted, because foo and bar
    433 
    +   are checked separately, and thus the two fundep constraints never
    434 
    +   encounter each other. It is test case typecheck/should_compile/FunDepOrigin1.
    435 
    +
    436 
    +   This case applies only when both fundeps are *Wanted* fundeps; when
    437 
    +   both are givens, the error represents unreachable code. For
    438 
    +   a Given/Wanted case, see #9612.
    439 
    +
    440 
    +   End of historical note
    441 
    +
    349 442 
     -}
    350 443
    351 444 
     reportImplic :: SolverReportErrCtxt -> Implication -> TcM ()
    ... ... @@ -452,16 +545,6 @@ reportBadTelescope ctxt env (ForAllSkol telescope) skols
    452 545 
     reportBadTelescope _ _ skol_info skols
    453 546 
       = pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols)
    454 547
    455 
    --- | Should we completely ignore this constraint in error reporting?
    456 
    --- It *must* be the case that any constraint for which this returns True
    457 
    --- somehow causes an error to be reported elsewhere.
    458 
    --- See Note [Constraints to ignore].
    459 
    -ignoreConstraint :: Ct -> Bool
    460 
    -ignoreConstraint ct
    461 
    -  = case ctOrigin ct of
    462 
    -      AssocFamPatOrigin         -> True  -- See (CIG1)
    463 
    -      _                         -> False
    464 
    -
    465 548 
     -- | Makes an error item from a constraint, calculating whether or not the item
    466 549 
     -- should be suppressed. See Note [Wanteds rewrite Wanteds: rewriter-sets]
    467 550 
     -- in GHC.Tc.Types.Constraint. Returns Nothing if we should just ignore
    ... ... @@ -473,56 +556,105 @@ mkErrorItem ct
    473 556 
            ; return Nothing }   -- See Note [Constraints to ignore]
    474 557
    475 558 
       | otherwise
    476 
    -  = do { let loc = ctLoc ct
    477 
    -             flav = ctFlavour ct
    559 
    +  = do { let ev = ctEvidence ct
    560 
    +
    561 
    +             m_evdest =  case ev of
    562 
    +                           CtGiven {}                               -> Nothing
    563 
    +                           CtWanted (WantedCt { ctev_dest = dest }) -> Just dest
    478 564
    479 
    -             -- For this `suppress` stuff see
    480 
    -             -- Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint
    481 
    -             (suppress, m_evdest) = case ctEvidence ct of
    482 
    -                     CtGiven {} -> (False, Nothing)
    483 
    -                     CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest })
    484 
    -                                -> (not (isEmptyCoHoleSet rws), Just dest)
    485 565
    486 
    -       ; let m_reason = case ct of
    566 
    +             m_reason = case ct of
    487 567 
                     CIrredCan (IrredCt { ir_reason = reason }) -> Just reason
    488 568 
                     _                                          -> Nothing
    489 569
    490 
    -             insoluble_ct = insolubleCt ct
    491 
    -
    492 570 
            ; return $ Just $ EI { ei_pred      = ctPred ct
    493 571 
                                 , ei_evdest    = m_evdest
    494 
    -                            , ei_flavour   = flav
    495 
    -                            , ei_loc       = loc
    572 
    +                            , ei_flavour   = ctFlavour ct
    573 
    +                            , ei_loc       = ctLoc ct
    496 574 
                                 , ei_m_reason  = m_reason
    497 
    -                            , ei_insoluble = insoluble_ct
    498 
    -                            , ei_suppress  = suppress }}
    575 
    +                            , ei_insoluble = insolubleCt ct
    576 
    +                            , ei_suppress  = suppressCtError ev }}
    499 577
    500 578 
     -- | Actually report this 'ErrorItem'.
    501 579 
     unsuppressErrorItem :: ErrorItem -> ErrorItem
    502 580 
     unsuppressErrorItem ei = ei { ei_suppress = False }
    503 581
    582 
    +-- | Should we completely ignore this constraint in error reporting?
    583 
    +-- It *must* be the case that any constraint for which this returns True
    584 
    +-- somehow causes an error to be reported elsewhere.
    585 
    +-- See Note [Constraints to ignore].
    586 
    +ignoreConstraint :: Ct -> Bool
    587 
    +ignoreConstraint ct
    588 
    +  = case ctOrigin ct of
    589 
    +      AssocFamPatOrigin         -> True  -- See (CIG1)
    590 
    +      _                         -> False
    591 
    +
    592 
    +suppressCtError :: CtEvidence -> Bool
    593 
    +-- See Note [ei_suppress: suppressing confusing errors]
    594 
    +suppressCtError (CtGiven {})
    595 
    +  = False
    596 
    +suppressCtError (CtWanted (WantedCt { ctev_rewriters = rws, ctev_loc = loc }))
    597 
    +  | not (isEmptyCoHoleSet rws)
    598 
    +  = True  -- See (SCE1)
    599 
    +
    600 
    +  | isWantedSuperclassOrigin (ctLocOrigin loc)
    601 
    +  = True  -- See (SCE2)
    602 
    +
    603 
    +  | otherwise
    604 
    +  = False
    605 
    +
    606 
    +{- Note [Constraints to ignore]
    607 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    608 
    +Some constraints are meant only to aid the solver by unification; a failure
    609 
    +to solve them is not necessarily an error to report to the user. It is critical
    610 
    +that compilation is aborted elsewhere if there are any ignored constraints here;
    611 
    +they will remain unfilled, and might have been used to rewrite another constraint.
    612 
    +
    613 
    +Currently, the constraints to ignore are:
    614 
    +
    615 
    +(CIG1) Constraints generated in order to unify associated type instance parameters
    616 
    +   with class parameters. Here are two illustrative examples:
    617 
    +
    618 
    +     class C (a :: k) where
    619 
    +       type F (b :: k)
    620 
    +
    621 
    +     instance C True where
    622 
    +       type F a = Int
    623 
    +
    624 
    +     instance C Left where
    625 
    +       type F (Left :: a -> Either a b) = Bool
    626 
    +
    627 
    +   In the first instance, we want to infer that `a` has type Bool. So we emit
    628 
    +   a constraint unifying kappa (the guessed type of `a`) with Bool. All is well.
    629 
    +
    630 
    +   In the second instance, we process the associated type instance only
    631 
    +   after fixing the quantified type variables of the class instance. We thus
    632 
    +   have skolems a1 and b1 such that the class instance is for (Left :: a1 -> Either a1 b1).
    633 
    +   Unifying a1 and b1 with a and b in the type instance will fail, but harmlessly so.
    634 
    +   checkConsistentFamInst checks for this, and will fail if anything has gone
    635 
    +   awry. Really the equality constraints emitted are just meant as an aid, not
    636 
    +   a requirement. This is test case T13972.
    637 
    +
    638 
    +   We detect this case by looking for an origin of AssocFamPatOrigin; constraints
    639 
    +   with this origin are dropped entirely during error message reporting.
    640 
    +
    641 
    +   If there is any trouble, checkValidFamInst bleats, aborting compilation.
    642 
    +
    643 
    +(Note: Aug 25: this seems a rather tricky corner;
    644 
    +               c.f. Note [ei_suppress: suppressing confusing errors])
    645 
    +-}
    646 
    +
    504 647 
     ----------------------------------------------------------------
    505 648 
     reportWanteds :: SolverReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
    506 649 
     reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
    507 650 
                                      , wc_errors = errs })
    508 
    -  | isEmptyWC wc = traceTc "reportWanteds empty WC" empty
    651 
    +  | isEmptyWC wc
    652 
    +  = traceTc "reportWanteds empty WC" empty
    509 653 
       | otherwise
    510 654 
       = do { tidy_items1 <- mapMaybeM mkErrorItem tidy_cts
    511 
    -       ; traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples
    512 
    -                                         , text "Suppress =" <+> ppr (cec_suppress ctxt)
    513 
    -                                         , text "tidy_cts   =" <+> ppr tidy_cts
    514 
    -                                         , text "tidy_items1 =" <+> ppr tidy_items1
    515 
    -                                         , text "tidy_errs =" <+> ppr tidy_errs ])
    516 655
    517 656 
              -- Catch an awkward (and probably rare) case in which /all/ errors are
    518 
    -         -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty
    519 
    -         -- CoHoleSet] in GHC.Tc.Types.Constraint.
    520 
    -         --
    521 
    -         -- Unless we are sure that an error will be reported some other way
    522 
    -         -- (details in the defn of tidy_items) un-suppress the lot. This makes
    523 
    -         -- sure we don't forget to report an error at all, which is
    524 
    -         -- catastrophic: GHC proceeds to desguar and optimise the program, even
    525 
    -         -- though it is full of type errors (#22702, #22793)
    657 
    +         -- suppressed: see (SCE3) in Note [ie_suppress: suppressing confusing errors]
    526 658 
            ; errs_already <- ifErrsM (return True) (return False)
    527 659 
            ; let tidy_items
    528 660 
                    | not errs_already                     -- Have not already reported an error (perhaps
    ... ... @@ -530,43 +662,54 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
    530 662 
                    , not (any ignoreConstraint simples)   -- No error is ignorable (is reported elsewhere)
    531 663 
                    , all ei_suppress tidy_items1          -- All errors are suppressed
    532 664 
                    = map unsuppressErrorItem tidy_items1
    665 
    +
    533 666 
                    | otherwise
    534 667 
                    = tidy_items1
    535 668
    669 
    +       ; traceTc "reportWanteds 1" (vcat [ text "Simples =" <+> ppr simples
    670 
    +                                         , text "Suppress =" <+> ppr (cec_suppress ctxt)
    671 
    +                                         , text "tidy_cts   =" <+> ppr tidy_cts
    672 
    +                                         , text "tidy_items1 =" <+> ppr tidy_items1
    673 
    +                                         , text "tidy_errs =" <+> ppr tidy_errs ])
    674 
    +
    536 675 
              -- First, deal with any out-of-scope errors:
    537 676 
            ; let (out_of_scope, other_holes, not_conc_errs, mult_co_errs) = partition_errors tidy_errs
    538 
    -               -- don't suppress out-of-scope errors
    677 
    +               -- Don't suppress out-of-scope errors
    678 
    +               -- See (SLIE0) in Note [cec_suppress: suppressing less-important error messages]
    539 679 
                  ctxt_for_scope_errs = ctxt { cec_suppress = False }
    540 680 
            ; (_, no_out_of_scope) <- askNoErrs $
    541 681 
                                      reportHoles tidy_items ctxt_for_scope_errs out_of_scope
    542 682
    543 683 
              -- Next, deal with things that are utterly wrong
    544 
    -         -- Like Int ~ Bool (incl nullary TyCons)
    545 
    -         -- or  Int ~ t a   (AppTy on one side)
    546 
    -         -- These /ones/ are not suppressed by the incoming context
    547 
    -         -- (but will be by out-of-scope errors)
    684 
    +         -- These should not be suppressed by the incoming context
    685 
    +         -- (but should be suppressed by out-of-scope errors)
    686 
    +         -- See (SLIE0) in Note [cec_suppress: suppressing less-important error messages]
    548 687 
            ; let ctxt_for_insols = ctxt { cec_suppress = not no_out_of_scope }
    549 
    -       ; reportHoles tidy_items ctxt_for_insols other_holes
    550 
    -          -- holes never suppress
    551 688
    689 
    +       -- Don't suppress holes or concreteness errors unless we have scope errors
    690 
    +       ; reportHoles tidy_items ctxt_for_insols other_holes
    552 691 
            ; reportNotConcreteErrs ctxt_for_insols not_conc_errs
    553 692
    554 693 
            -- We only want to report multiplicity coercion errors for multiplicity
    555 694 
            -- constraints which are /solved/ with a non-reflexivity coercion. We
    556 695 
            -- over approximate here: we only report multiplicity coercion errors
    557 
    -       -- when /all/ constraints are solved.
    696 
    +       -- when /all/ other constraints are solved.
    558 697 
            -- See wrinkle (DME1) in Note [Coercion errors in tcSubMult] in GHC.Tc.Utils.Unify.
    559 
    -       ; when (null simples) $ reportMultiplicityCoercionErrs ctxt_for_insols mult_co_errs
    698 
    +       ; when (null simples) $
    699 
    +         reportMultiplicityCoercionErrs ctxt_for_insols mult_co_errs
    560 700
    561 
    -          -- See Note [Suppressing confusing errors]
    562 
    -       ; let (suppressed_items, reportable_items) = partition suppressItem tidy_items
    563 
    -       ; traceTc "reportWanteds suppressed:" (ppr suppressed_items)
    564 
    -       ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 reportable_items
    701 
    +       -- Now the main batch of utterly-wrong things
    702 
    +       -- Like Int ~ Bool (incl nullary TyCons)
    703 
    +       -- or   Int ~ t a  (AppTy on one side)
    704 
    +       ; (ctxt1, items1) <- tryReporters ctxt_for_insols report1 tidy_items
    565 705
    566 706 
              -- Now all the other constraints.  We suppress errors here if
    567 
    -         -- any of the first batch failed, or if the enclosing context
    568 
    -         -- says to suppress
    569 
    -       ; let ctxt2 = ctxt1 { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 }
    707 
    +         -- any of the first batch failed (ctxt1), or if the enclosing context
    708 
    +         -- says to suppress AND there are no local insolubles
    709 
    +         -- Why the AND part?  In case all those local insolubles are suppressed.
    710 
    +         -- See (SLIE3) in Note [cec_suppress: suppressing less-important error messages]
    711 
    +       ; let ctxt2 = ctxt1 { cec_suppress = cec_suppress ctxt1
    712 
    +                                || (cec_suppress ctxt && not (any ei_insoluble tidy_items)) }
    570 713 
            ; (_, leftovers) <- tryReporters ctxt2 report2 items1
    571 714 
            ; massertPpr (null leftovers)
    572 715 
                (text "The following unsolved Wanted constraints \
    ... ... @@ -577,21 +720,10 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
    577 720 
                 -- NB ctxt2: don't suppress inner insolubles if there's only a
    578 721 
                 -- wanted insoluble here; but do suppress inner insolubles
    579 722 
                 -- if there's a *given* insoluble here (= inaccessible code)
    580 
    -
    581 
    -         -- If there are no other errors to report, report suppressed errors.
    582 
    -         -- See (SCE3) in Note [Suppressing confusing errors].
    583 
    -         -- NB: with -fdefer-type-errors we might have reported warnings only from
    584 
    -         -- reportable_items`, but we still want to suppress the `suppressed_items`.
    585 
    -       ; when (null reportable_items) $
    586 
    -         do { (_, more_leftovers) <- tryReporters ctxt_for_insols (report1++report2)
    587 
    -                                                  suppressed_items
    588 
    -                 -- ctxt_for_insols: the suppressed errors can be Int~Bool, which
    589 
    -                 -- will have made the incoming `ctxt` be True; don't make that
    590 
    -                 -- suppress the Int~Bool error!
    591 
    -            ; massertPpr (null more_leftovers) (ppr more_leftovers) } }
    723 
    +       }
    592 724 
      where
    593 725 
         env       = cec_tidy ctxt
    594 
    -    tidy_cts  = bagToList (mapBag (tidyCt env)   simples)
    726 
    +    tidy_cts  = bagToList (mapBag (tidyCt env)           simples)
    595 727 
         tidy_errs = bagToList (mapBag (tidyDelayedError env) errs)
    596 728
    597 729 
         partition_errors :: [DelayedError] -> ([Hole], [Hole], [NotConcreteError], [(TcCoercion, CtLoc)])
    ... ... @@ -610,8 +742,8 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
    610 742 
               DE_Multiplicity mult_co loc
    611 743 
                 -> (es1, es2, es3, (mult_co, loc):es4)
    612 744
    613 
    -    -- report1: ones that should *not* be suppressed by
    614 
    -    --          an insoluble somewhere else in the tree
    745 
    +    -- report1: ones that should *not* be suppressed by cec_suppress,
    746 
    +    --          (i.e. by an insoluble somewhere else in the tree)
    615 747 
         -- It's crucial that anything that is considered insoluble
    616 748 
         -- (see GHC.Tc.Utils.insolublWantedCt) is caught here, otherwise
    617 749 
         -- we might suppress its error message, and proceed on past
    ... ... @@ -752,15 +884,6 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
    752 884 
           = has_gadt_match implics
    753 885
    754 886 
     ---------------
    755 
    -suppressItem :: ErrorItem -> Bool
    756 
    - -- See Note [Suppressing confusing errors]
    757 
    -suppressItem item
    758 
    -  | Wanted <- ei_flavour item
    759 
    -  , let orig = errorItemOrigin item
    760 
    -  = isWantedSuperclassOrigin orig       -- See (SCE1)
    761 
    -  | otherwise
    762 
    -  = False
    763 
    -
    764 887 
     isSkolemTy :: TcLevel -> Type -> Bool
    765 888 
     -- The type is a skolem tyvar
    766 889 
     isSkolemTy tc_lvl ty
    ... ... @@ -778,113 +901,8 @@ isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
    778 901 
                           Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
    779 902 
                           _ -> Nothing
    780 903
    781 
    -{- Note [Suppressing confusing errors]
    782 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    783 
    -Certain errors we might encounter are potentially confusing to users.
    784 
    -If there are any other errors to report, at all, we want to suppress these.
    785 
    -
    786 
    -Which errors should be suppressed?
    787 
    -
    788 
    -(SCE1) Superclasses of Wanteds.  These are generated only in case they trigger functional
    789 
    -   dependencies.  If such a constraint is unsolved, then its "parent" constraint must
    790 
    -   also be unsolved, and is much more informative to the user.  Example (#26255):
    791 
    -        class (MinVersion <= F era) => Era era where { ... }
    792 
    -        f :: forall era. EraFamily era -> IO ()
    793 
    -        f = ..blah...   -- [W] Era era
    794 
    -   Here we have simply omitted "Era era =>" from f's type.  But we'll end up with
    795 
    -   /two/ Wanted constraints:
    796 
    -        [W] d1 :  Era era
    797 
    -        [W] d2 : MinVersion <= F era  -- Superclass of d1
    798 
    -   We definitely want to report d1 and not d2!  Happily it's easy to filter out those
    799 
    -   superclass-Wanteds, becuase their Origin betrays them.
    800 
    -
    801 
    -Historical (SCE2).  Fundep constraints never "escape" into the
    802 
    -   main solver and so never show up in error messages.
    803 
    -   See (SOLVE-FD) in Note [Overview of functional dependencies in type inference]
    804 
    -   in GHC.Tc.Solver.FunDeps.  So this wrinkle is now just a historical note.
    805 
    -
    806 
    -   Errors which arise from the interaction of two Wanted fun-dep constraints.
    807 
    -   Example:
    808 
    -
    809 
    -     class C a b | a -> b where
    810 
    -       op :: a -> b -> b
    811 
    -
    812 
    -     foo _ = op True Nothing
    813 
    -
    814 
    -     bar _ = op False []
    815 
    -
    816 
    -   Here, we could infer
    817 
    -     foo :: C Bool (Maybe a) => p -> Maybe a
    818 
    -     bar :: C Bool [a]       => p -> [a]
    819 
    -
    820 
    -   (The unused arguments suppress the monomorphism restriction.) The problem
    821 
    -   is that these types can't both be correct, as they violate the functional
    822 
    -   dependency. Yet reporting an error here is awkward: we must
    823 
    -   non-deterministically choose either foo or bar to reject. We thus want
    824 
    -   to report this problem only when there is nothing else to report.
    825 
    -   See typecheck/should_fail/T13506 for an example of when to suppress
    826 
    -   the error. The case above is actually accepted, because foo and bar
    827 
    -   are checked separately, and thus the two fundep constraints never
    828 
    -   encounter each other. It is test case typecheck/should_compile/FunDepOrigin1.
    829 
    -
    830 
    -   This case applies only when both fundeps are *Wanted* fundeps; when
    831 
    -   both are givens, the error represents unreachable code. For
    832 
    -   a Given/Wanted case, see #9612.
    833 
    -
    834 
    -   End of historical (SCE2)
    835 
    -
    836 
    -(SCE3) How can it happen that there are /only/ suppressed errors?  See test T18851
    837 
    -   for an example of how it is (just, barely) possible for the /only/ errors to
    838 
    -   be superclass-of-Wanted constraints.
    839 
    -
    840 
    -Mechanism:
    841 
    -
    842 
    -We use the `suppress` function within reportWanteds to filter out these
    843 
    -"suppress" cases, then report all other errors. After doing so, we return to these
    844 
    -suppressed ones and report them only if there have been no errors so far.
    845 
    -
    846 
    -Note [Constraints to ignore]
    847 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    848 
    -Some constraints are meant only to aid the solver by unification; a failure
    849 
    -to solve them is not necessarily an error to report to the user. It is critical
    850 
    -that compilation is aborted elsewhere if there are any ignored constraints here;
    851 
    -they will remain unfilled, and might have been used to rewrite another constraint.
    852 
    -
    853 
    -Currently, the constraints to ignore are:
    854 
    -
    855 
    -(CIG1) Constraints generated in order to unify associated type instance parameters
    856 
    -   with class parameters. Here are two illustrative examples:
    857 
    -
    858 
    -     class C (a :: k) where
    859 
    -       type F (b :: k)
    860 
    -
    861 
    -     instance C True where
    862 
    -       type F a = Int
    863 
    -
    864 
    -     instance C Left where
    865 
    -       type F (Left :: a -> Either a b) = Bool
    866 
    -
    867 
    -   In the first instance, we want to infer that `a` has type Bool. So we emit
    868 
    -   a constraint unifying kappa (the guessed type of `a`) with Bool. All is well.
    869 
    -
    870 
    -   In the second instance, we process the associated type instance only
    871 
    -   after fixing the quantified type variables of the class instance. We thus
    872 
    -   have skolems a1 and b1 such that the class instance is for (Left :: a1 -> Either a1 b1).
    873 
    -   Unifying a1 and b1 with a and b in the type instance will fail, but harmlessly so.
    874 
    -   checkConsistentFamInst checks for this, and will fail if anything has gone
    875 
    -   awry. Really the equality constraints emitted are just meant as an aid, not
    876 
    -   a requirement. This is test case T13972.
    877 
    -
    878 
    -   We detect this case by looking for an origin of AssocFamPatOrigin; constraints
    879 
    -   with this origin are dropped entirely during error message reporting.
    880 
    -
    881 
    -   If there is any trouble, checkValidFamInst bleats, aborting compilation.
    882 
    -
    883 
    -(Note: Aug 25: this seems a rather tricky corner;
    884 
    -               c.f. Note [Suppressing confusing errors])
    885 
    -
    886 
    -Note [Implementation of Unsatisfiable constraints]
    887 
    -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    904 
    +{- Note [Implementation of Unsatisfiable constraints]
    905 
    +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    888 906 
     The Unsatisfiable constraint was introduced in GHC proposal #433 (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst).
    889 907 
     See Note [The Unsatisfiable constraint] in GHC.TypeError.
    890 908
    ... ... @@ -1317,9 +1335,15 @@ maybeReportError :: SolverReportErrCtxt
    1317 1335 
     maybeReportError ctxt items@(item1:|_) (SolverReport { sr_important_msg = important
    1318 1336 
                                                          , sr_supplementary = supp
    1319 1337 
                                                          , sr_hints         = hints })
    1320 
    -  | suppress_group = return ()
    1321 
    -  | otherwise      = do { msg <- mkErrorReport loc_env diag (Just ctxt) supp hints
    1322 
    -                        ; reportDiagnostic msg }
    1338 
    +  | suppress_group
    1339 
    +  = -- Suppress the report entirely
    1340 
    +    -- But NB we still create the evidence binding; see `reportGroup`.
    1341 
    +    return ()
    1342 
    +
    1343 
    +  | otherwise
    1344 
    +  = -- Spit out an error or warning
    1345 
    +    do { msg <- mkErrorReport loc_env diag (Just ctxt) supp hints
    1346 
    +       ; reportDiagnostic msg }
    1323 1347 
       where
    1324 1348 
         reason | any (nonDeferrableOrigin . errorItemOrigin) items = ErrorWithoutFlag
    1325 1349 
                | otherwise                                         = cec_defer_type_errors ctxt
    ... ... @@ -1328,11 +1352,6 @@ maybeReportError ctxt items@(item1:|_) (SolverReport { sr_important_msg = import
    1328 1352 
         loc_env = ctLocEnv (errorItemCtLoc item1)
    1329 1353
    1330 1354 
         suppress_group
    1331 
    -     | all ei_suppress items
    1332 
    -     = True  -- If they are all suppressed (notably, have been rewritten by another unsolved wanted)
    1333 
    -             -- report nothing.  (If at least one is not suppressed, do report: the function that
    1334 
    -             -- generates the error message should look for an unsuppressed error item.)
    1335 
    -
    1336 1355 
     -- It is tempting to say that we always want to see all insoluble errors
    1337 1356 
     -- But then we get a bit more than we want.  Examples:
    1338 1357 
     --    a ~ t a               occurs check errors (T2534, mc25)
    ... ... @@ -1344,6 +1363,12 @@ maybeReportError ctxt items@(item1:|_) (SolverReport { sr_important_msg = import
    1344 1363 
          | cec_suppress ctxt
    1345 1364 
          = True   -- Some earlier error has occurred, so suppress this diagnostic
    1346 1365
    1366 
    +     | all ei_suppress items
    1367 
    +     = True  -- If they are all suppressed (notably, have been rewritten by another unsolved
    1368 
    +             -- wanted) report nothing.  (If at least one is not suppressed, do report:
    1369 
    +             -- the function that generates the error message should look for an
    1370 
    +             -- unsuppressed error item.)
    1371 
    +
    1347 1372 
          | otherwise
    1348 1373 
          = False
    1349 1374
    ... ... @@ -1402,11 +1427,11 @@ mkErrorTerm ct_loc ty ctxt msg supp hints
    1402 1427
    1403 1428 
            ; return $ evDelayedError ty err_str }
    1404 1429
    1405 
    -tryReporters :: SolverReportErrCtxt -> [ReporterSpec] -> [ErrorItem] -> TcM (SolverReportErrCtxt, [ErrorItem])
    1430 
    +tryReporters :: SolverReportErrCtxt -> [ReporterSpec] -> [ErrorItem]
    1431 
    +             -> TcM (SolverReportErrCtxt, [ErrorItem])
    1406 1432 
     -- Use the first reporter in the list whose predicate says True
    1407 1433 
     tryReporters ctxt reporters items
    1408 
    -  = do { let (vis_items, invis_items)
    1409 
    -               = partition (isVisibleOrigin . errorItemOrigin) items
    1434 
    +  = do { let (vis_items, invis_items) = partition (isVisibleOrigin . errorItemOrigin) items
    1410 1435 
            ; traceTc "tryReporters {" (ppr vis_items $$ ppr invis_items)
    1411 1436 
            ; (ctxt', items') <- go ctxt reporters vis_items invis_items
    1412 1437 
            ; traceTc "tryReporters }" (ppr items')
    ... ... @@ -1416,9 +1441,9 @@ tryReporters ctxt reporters items
    1416 1441 
           = return (ctxt, vis_items ++ invis_items)
    1417 1442
    1418 1443 
         go ctxt (r : rs) vis_items invis_items
    1419 
    -       -- always look at *visible* Origins before invisible ones
    1444 
    +       -- Always look at *visible* Origins before invisible ones
    1420 1445 
            -- this is the whole point of isVisibleOrigin
    1421 
    -      = do { (ctxt', vis_items') <- tryReporter ctxt r vis_items
    1446 
    +      = do { (ctxt',  vis_items')   <- tryReporter ctxt  r vis_items
    1422 1447 
                ; (ctxt'', invis_items') <- tryReporter ctxt' r invis_items
    1423 1448 
                ; go ctxt'' rs vis_items' invis_items' }
    1424 1449 
                     -- Carry on with the rest, because we must make
    ... ... @@ -1432,7 +1457,7 @@ tryReporter ctxt (str, keep_me, suppress_after, reporter) items = case nonEmpty
    1432 1457 
            { traceTc "tryReporter{ " (text str <+> ppr yeses)
    1433 1458 
            ; (_, no_errs) <- askNoErrs (reporter ctxt yeses)
    1434 1459 
            ; let suppress_now   = not no_errs && suppress_after
    1435 
    -                            -- See Note [Suppressing error messages]
    1460 
    +             -- See (SLIE2) in Note [cec_suppress: suppressing less-important error messages]
    1436 1461 
                  ctxt' = ctxt { cec_suppress = suppress_now || cec_suppress ctxt }
    1437 1462 
            ; traceTc "tryReporter end }" (text str <+> ppr (cec_suppress ctxt) <+> ppr suppress_after)
    1438 1463 
            ; return (ctxt', nos) }

  • compiler/GHC/Tc/Types/Constraint.hs
    ... ... @@ -1214,15 +1214,16 @@ insolubleWantedCt :: Ct -> Bool
    1214 1214 
     --
    1215 1215 
     -- See Note [Insoluble Wanteds]
    1216 1216 
     insolubleWantedCt ct
    1217 
    -  | CtWanted (WantedCt { ctev_loc = loc, ctev_rewriters = rewriters })
    1218 
    -      <- ctEvidence ct
    1217 
    +  | CtWanted (WantedCt {}) <- ctEvidence ct
    1219 1218 
           -- It's a Wanted
    1220 1219 
       , insolubleCt ct
    1221 1220 
           -- It's insoluble
    1222 
    -  , isEmptyCoHoleSet rewriters
    1221 
    +--  , isEmptyCoHoleSet rewriters
    1223 1222 
           -- It has no rewriters – see (IW1) in Note [Insoluble Wanteds]
    1224 
    -  , not (isGivenLoc loc)
    1225 
    -      -- isGivenLoc: see (IW2) in Note [Insoluble Wanteds]
    1223 
    +
    1224 
    +-- I don't understand IW2 so I'm going to get rid of it
    1225 
    +--  , not (isGivenLoc loc)
    1226 
    +--      -- isGivenLoc: see (IW2) in Note [Insoluble Wanteds]
    1226 1227 
         -- See also historical (IW3) in Note [Insoluble Wanteds]
    1227 1228 
       = True
    1228 1229

  • testsuite/tests/typecheck/should_fail/T18851d.hs
    1 
    +{-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
    2 
    +             ScopedTypeVariables, TypeFamilies, TypeApplications,
    3 
    +             FlexibleContexts, AllowAmbiguousTypes, ExtendedDefaultRules #-}
    4 
    +
    5 
    +module T18851d where
    6 
    +
    7 
    +default (Int)
    8 
    +
    9 
    +type family C_FD a
    10 
    +class C_FD a ~ b => C a b
    11 
    +
    12 
    +type instance C_FD Int = Bool -- just for Show (C_FD Int)
    13 
    +instance C Int b => C Int b
    14 
    +
    15 
    +class IsInt int
    16 
    +instance int ~ Int => IsInt int
    17 
    +
    18 
    +data A
    19 
    +instance Show A where
    20 
    +  show _ = "A"
    21 
    +data B
    22 
    +instance Show B where
    23 
    +  show _ = "B"
    24 
    +
    25 
    +data D
    26 
    +
    27 
    +f :: forall a b c int
    28 
    +  .  ( Show c, Num int
    29 
    +     , C int a, C int b, C int c
    30 
    +     -- , c ~ C_FD int -- add this to get rid of ambiguity error
    31 
    +     )
    32 
    +  => String
    33 
    +f = show (undefined :: c)
    34 
    +
    35 
    +g :: String
    36 
    +g = f @A @B  ++ show (undefined :: D)
    37 
    +  -- This variant, suggested by Claude in a review of !16564,
    38 
    +  -- has an unsolved (Show D) constraint.  It must not be suppressed
    39 
    +  -- by the insoluble-but-suppressed constraints arising from (C Int a)

  • testsuite/tests/typecheck/should_fail/T27731.hs
    1 
    +{-# LANGUAGE ImplicitParams, TypeFamilies #-}
    2 
    +
    3 
    +module Bug where
    4 
    +
    5 
    +type family St (a :: k) :: *
    6 
    +type family Ev (a :: k) :: * -> *
    7 
    +
    8 
    +data T1 a = C1 a
    9 
    +data T2 h g = C2 (h ())
    10 
    +
    11 
    +class (h ~ Ev g, s ~ St g) => Ren s h g
    12 
    +
    13 
    +f1 ::
    14 
    +  (s ~ St h, Ren s h g, ?settings :: settings)
    15 
    +  => (g v -> g ()) -> g v -> g ()
    16 
    +f1 form = (\_ a -> a) (C1 (f2 {-@g-})) form
    17 
    +
    18 
    +f2 :: forall g h s. ( s ~ St h, Ren s h g) => T2 h g
    19 
    +f2 = error "urk"
    20 
    +
    21 
    +{- Call of f2
    22 
    +
    23 
    +[W] s ~ St h  -->  St g ~ St h -->  St g ~ St (Ev g)
    24 
    +[W] Ren s h g
    25 
    +[W] s ~ St g   -- Superclass of wanted
    26 
    +[W] h ~ Ev g   -- Superclass of wanted
    27 
    +-}
    28 
    +
    29 
    +{-
    30 
    +f3 ::
    31 
    +  T1 ()
    32 
    +  -> (g v -> g ())
    33 
    +  -> g v -> g ()
    34 
    +f3 wd form = ((\_ a -> a) wd form)
    35 
    +
    36 
    +-}

  • testsuite/tests/typecheck/should_fail/T27731.stderr
    1 
    +T27731.hs:16:28: [GHC-05617]
    2 
    +    • Could not deduce ‘St (Ev g0) ~ St g0’
    3 
    +        arising from a superclass required to satisfy ‘Ren
    4 
    +                                                         (St (Ev g0)) (Ev g0) g0’,
    5 
    +        arising from a use of ‘f2’
    6 
    +      from the context: (s ~ St h, Ren s h g, ?settings::settings)
    7 
    +        bound by the type signature for:
    8 
    +                   f1 :: forall s (h :: * -> *) (g :: * -> *) settings v.
    9 
    +                         (s ~ St h, Ren s h g, ?settings::settings) =>
    10 
    +                         (g v -> g ()) -> g v -> g ()
    11 
    +        at T27731.hs:(13,1)-(15,33)
    12 
    +      Note: ‘St’ is a non-injective type family.
    13 
    +      The type variable ‘g0’ is ambiguous
    14 
    +    • In the first argument of ‘C1’, namely ‘(f2)’
    15 
    +      In the first argument of ‘\ _ a -> a’, namely ‘(C1 (f2))’
    16 
    +      In the expression: (\ _ a -> a) (C1 (f2)) form

  • testsuite/tests/typecheck/should_fail/all.T
    ... ... @@ -565,6 +565,7 @@ test('T17563', normal, compile_fail, [''])
    565 565 
     test('T18851', normal, compile_fail, [''])
    566 566 
     test('T18851b', normal, compile, [''])
    567 567 
     test('T18851c', normal, compile, [''])
    568 
    +test('T18851d', normal, compile, [''])
    568 569 
     test('T16946', normal, compile_fail, [''])
    569 570 
     test('T16502', expect_broken(12854), compile, [''])
    570 571 
     test('T17566b', normal, compile_fail, [''])
    ... ... @@ -763,3 +764,4 @@ test('T26861', normal, compile_fail, [''])
    763 764 
     test('T26862', normal, compile_fail, [''])
    764 765 
     test('T27210', normal, compile_fail, [''])
    765 766 
     test('T26532', normal, compile_fail, [''])
    767 
    +test('T27731', normal, compile_fail, [''])

    • —
    View it on GitLab.
    You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications · Help Notification message regarding https://gitlab.haskell.org/ghc/ghc/-/commit/2aaebe8bbdf7d6bf280584448b885dd73406512a at 1788426115