GitLab

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

Commits:

c3a4a7df
by Simon Peyton Jones at 2025-09-02T15:32:22+01:00
```
Wibbles
```

14 changed files:

compiler/GHC/Tc/Errors/Ppr.hs
compiler/GHC/Tc/Gen/Sig.hs
compiler/GHC/Tc/Solver/Monad.hs
compiler/GHC/Tc/Solver/Solve.hs
compiler/GHC/Tc/Types/Origin.hs
testsuite/tests/deriving/should_fail/T12768.stderr
testsuite/tests/deriving/should_fail/T1496.stderr
testsuite/tests/deriving/should_fail/T5498.stderr
testsuite/tests/deriving/should_fail/T7148.stderr
testsuite/tests/deriving/should_fail/T7148a.stderr
testsuite/tests/quantified-constraints/T19690.stderr
testsuite/tests/quantified-constraints/T21006.stderr
testsuite/tests/typecheck/should_fail/T15801.stderr
testsuite/tests/typecheck/should_fail/T22912.stderr

Changes:

@@ -4197,17 +4197,6 @@ pprTcSolverReportMsg ctxt@(CEC {cec_encl = implics})
 (text "Typeable" <+>
                parens (ppr ty <+> dcolon <+> ppr (typeKind ty)))
 -      -- When we were originally trying to solve a quantified constraint like
 -      --    (forall a. Eq a => Eq (c a))
 -      -- add a note to say so, so the overall error looks like
 -      --    Cannot deduce Eq (c a)
 -      --       from (Eq a)
 -      --    when trying to solve (forall a. Eq a => Eq (c a))
 -      -- Without this, the error is very inscrutable
 -      | ScOrigin (IsQC pred orig) _ <- orig
 -      = hang (text "When trying to solve the quantified constraint")
 -           2 (vcat [ ppr pred, pprCtOrigin orig ])
+-
        | otherwise
        = empty
@@ -4264,7 +4253,7 @@ pprTcSolverReportMsg (CEC {cec_encl = implics}) (OverlappingInstances item match
         -- simply report back the whole given
         -- context. Accelerate Smart.hs showed this problem.
           sep [ text "There exists a (perhaps superclass) match:"
 -             , nest 2 (vcat (pp_givens useful_givens))]
 +             , nest 2 (vcat (pp_from_givens useful_givens))]
      ,  ppWhen (null $ NE.tail matches) $
         parens (vcat [ ppUnless (null tyCoVars) $
@@ -4395,6 +4384,7 @@ pprMismatchMsg ctxt
                   , mismatch_whenMatching = mb_match_txt
                   , mismatch_mb_same_occ  = same_occ_info })
    =  vcat [ addArising (errorItemCtLoc item) msg
 +          , pprQCOriginExtra item
            , ea_extra
            , maybe empty (pprWhenMatching ctxt) mb_match_txt
            , maybe empty pprSameOccInfo same_occ_info ]
@@ -4447,9 +4437,10 @@ pprMismatchMsg ctxt
                    , teq_mismatch_actual   = act   --   the mis-match
                    , teq_mismatch_what     = mb_thing
                    , teq_mb_same_occ       = mb_same_occ })
 -  = addArising ct_loc $
 -    pprWithInvisibleBitsWhen ppr_invis_bits msg
 -    $$ maybe empty pprSameOccInfo mb_same_occ
 +  = vcat [ addArising ct_loc $
 +           pprWithInvisibleBitsWhen ppr_invis_bits msg
 +           $$ maybe empty pprSameOccInfo mb_same_occ
 +         , pprQCOriginExtra item ]
    where
      msg | Just (torc, rep) <- sORTKind_maybe exp
@@ -4565,45 +4556,55 @@ pprMismatchMsg ctxt
      starts_with_vowel []    = False
  pprMismatchMsg ctxt (CouldNotDeduce useful_givens (item :| others) mb_extra)
 -  = main_msg $$
 -     case supplementary of
 -      Left infos
 -        -> vcat (map (pprExpectedActualInfo ctxt) infos)
 -      Right other_msg
 -        -> other_msg
 +  = vcat [ main_msg
 +         , pprQCOriginExtra item
 +         , ea_supplementary ]
    where
      main_msg
 -      | null useful_givens
 -      = addArising ct_loc (no_instance_msg <+> missing)
 -      | otherwise
 -      = vcat (addArising ct_loc (no_deduce_msg <+> missing)
 -              : pp_givens useful_givens)
+-
 -    supplementary = case mb_extra of
 -      Nothing
 -        -> Left []
 -      Just (CND_Extra level ty1 ty2)
 -        -> mk_supplementary_ea_msg ctxt level ty1 ty2 orig
 +      | null useful_givens = addArising ct_loc no_instance_msg
 +      | otherwise          = vcat ( addArising ct_loc no_deduce_msg
 +                                  : pp_from_givens useful_givens)
++
 +    ea_supplementary = case mb_extra of
 +      Nothing                        -> empty
 +      Just (CND_Extra level ty1 ty2) -> mk_supplementary_ea_msg ctxt level ty1 ty2 orig
++
      ct_loc = errorItemCtLoc item
      orig   = ctLocOrigin ct_loc
      wanteds = map errorItemPred (item:others)
      no_instance_msg =
        case wanteds of
 -        [wanted] | Just (tc, _) <- splitTyConApp_maybe wanted
 -                 -- Don't say "no instance" for a constraint such as "c" for a type variable c.
 -                 , isClassTyCon tc -> text "No instance for"
 -        _ -> text "Could not solve:"
 +        [wanted] | -- Guard: don't say "no instance" for a constraint
 +                   -- such as "c" for a type variable c.
 +                   Just (tc, _) <- splitTyConApp_maybe wanted
 +                 , isClassTyCon tc
 +                 -> text "No instance for" <+> quotes (ppr wanted)
 +        _        -> text "Could not solve:" <+> pprTheta wanteds
      no_deduce_msg =
        case wanteds of
 -        [_wanted] -> text "Could not deduce"
 -        _         -> text "Could not deduce:"
+-
 -    missing =
 -      case wanteds of
 -        [wanted] -> quotes (ppr wanted)
 -        _        -> pprTheta wanteds
 +        [wanted] -> text "Could not deduce" <+> quotes (ppr wanted)
 +        _        -> text "Could not deduce:" <+> pprTheta wanteds
++
 +pprQCOriginExtra :: ErrorItem -> SDoc
 +-- When we were originally trying to solve a quantified constraint like
 +--    (forall a. Eq a => Eq (c a))
 +-- add a note to say so, so the overall error looks like
 +--    Cannot deduce Eq (c a)
 +--       from (Eq a)
 +--    when trying to solve (forall a. Eq a => Eq (c a))
 +-- Without this, the error is very inscrutable
 +-- See (WFA3) in Note [Solving a Wanted forall-constraint],
 +--            in GHC.Tc.Solver.Solve
 +pprQCOriginExtra item
 +  | ScOrigin (IsQC pred orig) _ <- orig
 +  = hang (text "When trying to solve the quantified constraint")
 +       2 (vcat [ ppr pred, pprCtOrigin orig ])
 +  | otherwise
 +  = empty
 +  where
 +    orig = ctLocOrigin (errorItemCtLoc item)
  pprKindMismatchMsg :: TypedThing -> Type -> Type -> SDoc
  pprKindMismatchMsg thing exp act
@@ -4908,10 +4909,7 @@ pprWhenMatching ctxt (WhenMatching cty1 cty2 sub_o mb_sub_t_or_k) =
    where
      sub_t_or_k = mb_sub_t_or_k `orElse` TypeLevel
      sub_whats  = text (levelString sub_t_or_k) <> char 's'
 -    supplementary =
 -      case mk_supplementary_ea_msg ctxt sub_t_or_k cty1 cty2 sub_o of
 -        Left infos -> vcat $ map (pprExpectedActualInfo ctxt) infos
 -        Right msg  -> msg
 +    supplementary = mk_supplementary_ea_msg ctxt sub_t_or_k cty1 cty2 sub_o
  pprTyVarInfo :: SolverReportErrCtxt -> TyVarInfo -> SDoc
  pprTyVarInfo ctxt (TyVarInfo { thisTyVar = tv1, otherTy = mb_tv2, thisTyVarIsUntouchable = mb_implic })
@@ -5294,8 +5292,8 @@ usefulContext implics pred
      implausible_info _                             = False
      -- Do not suggest adding constraints to an *inferred* type signature
 -pp_givens :: [Implication] -> [SDoc]
 -pp_givens givens
 +pp_from_givens :: [Implication] -> [SDoc]
 +pp_from_givens givens
     = case givens of
           []     -> []
           (g:gs) ->      ppr_given (text "from the context:") g
@@ -5465,13 +5463,15 @@ skolsSpan skol_tvs = foldr1WithDefault noSrcSpan combineSrcSpans (map getSrcSpan
  **********************************************************************-}
  mk_supplementary_ea_msg :: SolverReportErrCtxt -> TypeOrKind
 -                        -> Type -> Type -> CtOrigin -> Either [ExpectedActualInfo] SDoc
 +                        -> Type -> Type -> CtOrigin -> SDoc
  mk_supplementary_ea_msg ctxt level ty1 ty2 orig
    | TypeEqOrigin { uo_expected = exp, uo_actual = act } <- orig
    , not (ea_looks_same ty1 ty2 exp act)
 -  = mk_ea_msg ctxt Nothing level orig
 +  = case mk_ea_msg ctxt Nothing level orig of
 +      Left infos -> vcat $ map (pprExpectedActualInfo ctxt) infos
 +      Right msg  -> msg
    | otherwise
 -  = Left []
 +  = empty
  ea_looks_same :: Type -> Type -> Type -> Type -> Bool
  -- True if the faulting types (ty1, ty2) look the same as

compiler/GHC/Tc/Gen/Sig.hs

@@ -976,6 +976,8 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
                 tcInferRho spec_e
           -- (2) Solve the resulting wanteds
 +         -- When doing so, switch on `tcsmFullySolveQCIs`; see (WFA4) in
 +         -- Note [Solving a Wanted forall-constraint] in GHC.Tc.Solver.Solve
         ; ev_binds_var <- newTcEvBinds
         ; spec_e_wanted <- setTcLevel rhs_tclvl            $
                            runTcSWithEvBinds ev_binds_var  $

compiler/GHC/Tc/Solver/Monad.hs

@@ -908,7 +908,7 @@ data TcSMode
              , tcsmSkipOverlappable :: Bool
                     -- ^ Do not select an OVERLAPPABLE instance
              , tcsmFullySolveQCIs   :: Bool
 -                   -- ^ Fully solve all constraints, without using local Givens
 +                   -- ^ Fully solve quantified constraints
+             }
  vanillaTcSMode :: TcSMode
@@ -1281,7 +1281,8 @@ tryShortCutTcS :: TcS Bool -> TcS Bool
  -- Use only by the short-cut solver;
  --   see Note [Shortcut solving] in GHC.Tc.Solver.Dict
  tryShortCutTcS (TcS thing_inside)
 -  = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var
 +  = TcS $ \ env@(TcSEnv { tcs_mode = mode
 +                        , tcs_inerts = inerts_var
                          , tcs_ev_binds = old_ev_binds_var }) ->
      do { -- Initialise a fresh inert set, with no Givens and no Wanteds
           --    (i.e. empty `inert_cans`)
@@ -1297,7 +1298,7 @@ tryShortCutTcS (TcS thing_inside)
         ; new_wl_var       <- TcM.newTcRef emptyWorkList
         ; new_ev_binds_var <- TcM.cloneEvBindsVar old_ev_binds_var
 -       ; let nest_env = env { tcs_mode     = vanillaTcSMode { tcsmSkipOverlappable = True }
 +       ; let nest_env = env { tcs_mode     = mode { tcsmSkipOverlappable = True }
                              , tcs_ev_binds = new_ev_binds_var
                              , tcs_inerts   = new_inert_var
                              , tcs_worklist = new_wl_var }

compiler/GHC/Tc/Solver/Solve.hs

@@ -124,12 +124,10 @@ simplify_loop n limit definitely_redo_implications
                  -- Any insoluble constraints are in 'simples' and so get rewritten
                  -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet
 -       ; mode <- getTcSMode
 -       ; extras :: Bag (Either Ct Implication) <- mapMaybeBagM (solveWantedQCI mode) simples1
 -       ; let simples' :: Cts                      -- simples1 are all Wanteds
 -             implics_from_qcis :: Bag Implication
 -             (simples', implics_from_qcis) = partitionBagWith id extras
 +       -- Now try to solve any Wanted QCInsts in `simples1`
 +       ; (simples', implics_from_qcis) <- solveWantedQCIs simples1
 +       -- Next, solve implications from wc_impl
         ; implics' <- if not definitely_redo_implications  -- See Note [Superclass iteration]
                          && unifs1 == 0                    -- for this conditional
                      then return implics
@@ -1319,53 +1317,22 @@ and discharge df thus:
      df = /\ab. \g1 g2. let <binds> in d
  where <binds> is filled in by solving the implication constraint.
 -What we actually do is:
 -* In `solveForAll` we see if we have an identical quantified constraint
 -  to solve it (tryInertQCs), and then just add it to `inert_qcis :: [QCInst]`
 -* In the main solver loop, `GHC.Tc.Solver.Solve.simplify_loop`,
 -     - We attempt to solve the `wc_simple` constraints with `solveSimpleWanteds`
 -     - we grab grab any unsolved Wanted quantified constraints
 -       from that attempt; they are all `QCInst` constraints.
 -     - we turn those Wanted `QCInst` constraints into `Implication`s,
 -       using `wantedQciToImplic`.
 -     - we add them to `wc_implic` and do `solveImplications`
+-
 -We do not /actually/ emit an implication to solve later.  Rather we
 -try to solve it completely immediately using `trySolveImplication`
 -    - If successful, we can build evidence
 -    - If unsuccessful, we abandon the attempt and add the unsolved
 -      forall-constraint to the inert set.
+-
 -There are several reasons for this "solve immediately" approach
 +What we actually do is this:
 -* It saves quite a bit of plumbing, tracking the emitted implications for
 -  later solving; and the evidence would have to contain as-yet-incomplte
 -  bindings which complicates tracking of unused Givens.
+-
 -* We get better error messages, about failing to solve, say
 -         (forall a. a->a) ~ (forall b. b->Int)
+-
 -* Consider
 -    f :: forall f a. (Ix a, forall x. Eq x => Eq (f x)) => a -> f a
 -    {-# SPECIALISE f :: forall f. (forall x. Eq x => Eq (f x)) => Int -> f Int #-}
 -  This SPECIALISE is treated like an expression with a type signature, so
 -  we instantiate the constraints, simplify them and re-generalise.  From the
 -  instantiation we get  [W] d :: (forall x. Eq a => Eq (f x))
 -  and we want to generalise over that.  We do not want to attempt to solve it
 -  and then get stuck, and emit an error message.  If we can't solve it, better
 -  to leave it alone.
 +* In `solveForAll` we see if we have an identical quantified constraint
 +  to solve it (using tryInertQCs), and then just add it to `inert_qcis :: [QCInst]`
 +  See Note [Solving Wanted QCs from Given QCs]
 -  We still need to simplify quantified constraints that can be
 -  /fully solved/ from instances, otherwise we would never be able to
 -  specialise them away. Example: {-# SPECIALISE f @[] @a #-}.
 +* In the main solver loop, `GHC.Tc.Solver.Solve.simplify_loop`:
 -  This last point is a big one: it was the immediate driver for moving to
 -  the "solve immediately" approach.
 +     - We attempt to solve the `wc_simple` constraints with `solveSimpleWanteds`
 +       Unsolved quantified constraints just accumulate in the `inert_qcis` field
 +       of the `InertSet`.
 -You might worry about the wasted work from failed attempts to fully-solve, but
 -it is seldom repeated (because the constraint solver seldom iterates much).
 +     - Then we use `solveWantedQCIs` to solve any quantified constraints. It usually
 +       turns the `QCInst` into an `Implication`; but not invariably (WFA4)
 -There are some tricky corners though:
 +Wrinkles:
  (WFA1) We can take a more straightforward path when there is a matching Given, e.g.
            [W] dg :: forall c d. (Eq c, Ord d) => C x c d
@@ -1386,16 +1353,38 @@ There are some tricky corners though:
    * Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size))
    * Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc)
 -  Both of these things are done in solveForAll.  Now the mechanism described
 +  Both of these things are done in `solveWantedQCI`.  Now the mechanism described
    in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over.
 -(WFA3) When inferring an appropriate context for a `deriving` instance, we
 -  really /do/ want to generate an implication, and perhaps leave it half-solved,
 -  from where we might then gather unsolved class constraints (via
 -  `approximateWC` called in GHC.Tc.Deriv.Infer.simplifyDeriv).  Rather than
 -  have a complicated special solver mode, we simply generate an /implication/
 -  in the first place, in GHC.Tc.Deriv.Utils.emitPredSpecConstraints.
 -  See Note [Inferred contexts from method constraints] in GHC.Tc.Deriv.Infer
 +(WFA3) Error messages. Suppose we are trying to solve the quantified constraint
 +            forall a. Eq a => Eq (c a)
 +  We don't just want to say "No instance for Eq (c a)".  It /really/ helps to
 +  say what quantified constraint we were trying to solve.
++
 +  So the `IsQC` origin carries that info, and `GHC.Tc.Errors.Ppr.pprQCOriginExtra`
 +  prints the extra info.
++
 +(WFA4) Consider
 +    f :: forall f a. (Ix a, forall x. Eq x => Eq (f x)) => a -> f a
 +    {-# SPECIALISE f :: forall f. (forall x. Eq x => Eq (f x)) => Int -> f Int #-}
 +  This SPECIALISE is treated like an expression with a type signature, so
 +  we instantiate the constraints, simplify them and re-generalise.  From the
 +  instantiation we get  [W] d :: (forall x. Eq a => Eq (f x))
 +  and we want to generalise over that.  We do not want to attempt to solve it
 +  and then get stuck, and emit an error message.  If we can't solve it, it is
 +  much, much better to leave it alone.
++
 +  We still need to simplify quantified constraints that can be /fully solved/
 +  from instances, otherwise we would never be able to specialise them
 +  away. Example: {-# SPECIALISE f @[] @a #-}.  So:
++
 +  * The constraint solver has a mode flag `tcsmFullySolveQCIs` that says
 +    "fully solve quantified constraint, or leave them alone
 +  * When simplifying constraints in a SPECIALISE pragma, we switch on this
 +    flag (see `GHC.Tc.Gen.Sig.tcSpecPrag`, the `SpecSigE` case).
++
 +  You might worry about the wasted work from failed attempts to fully-solve, but
 +  it is seldom repeated (because the constraint solver seldom iterates much).
  Note [Solving Wanted QCs from Given QCs]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1505,13 +1494,23 @@ try_inert_qcs (QCI { qci_ev = ev_w }) inerts =
        | otherwise
        = Nothing
 +solveWantedQCIs :: Cts -> TcS (Cts, Bag Implication)
 +solveWantedQCIs wanteds
 +  = do { mode <- getTcSMode
 +       ; bag_of_eithers <- mapBagM (solveWantedQCI mode) wanteds
 +         -- bag_of_eithers :: Bag (Either Ct Implication)
 +       ; return (partitionBagWith id bag_of_eithers) }
++
  solveWantedQCI :: TcSMode
                 -> Ct   -- Definitely a Wanted
 -               -> TcS (Maybe (Either Ct Implication))
 --- Try to solve a quantified constraint.
 ---   In TcSChortCut mode, insist on solving it fully or not at all
 +               -> TcS (Either Ct Implication)
 +-- Try to solve a quantified constraint, `ct`
  -- Returns
 --- No-op on all Cts other than CQuantCan
 +--    (Left ct) if `ct` is not a quantified constraint
 +--    (Right implic) if we can solve a quantified constraint `ct` by creating
 +--                   an implication and fully or partly solving it
 +--    (Left ct) for a quantified constraint that can't be /fully solved/,
 +--              but mode is tcsmFullySolveQCIs
  -- See Note [Solving a Wanted forall-constraint]
  solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev =  ev, qci_tvs = tvs
                                         , qci_theta = theta, qci_body = body_pred }))
@@ -1543,7 +1542,8 @@ solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev =  ev, qci_tvs = tvs
                     ; newWantedNC loc' rewriters inst_pred }
         ; ev_binds_var <- TcS.newTcEvBinds
 -       ; let imp = (implicationPrototype (ctLocEnv loc))
 +       ; let imp :: Implication
 +             imp = (implicationPrototype (ctLocEnv loc))
                       { ic_tclvl  = lvl
                       , ic_skols  = skol_tvs
                       , ic_given  = given_ev_vars
@@ -1558,7 +1558,7 @@ solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev =  ev, qci_tvs = tvs
             , not (isSolvedStatus (ic_status imp'))
             -> -- Not fully solved, but mode says that we must fully
                -- solve quantified constraints; so abandon the attempt
 -              return (Just (Left ct))
 +              return (Left ct)
             | otherwise
             -> -- Record evidence and return residual implication
@@ -1570,14 +1570,14 @@ solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev =  ev, qci_tvs = tvs
                          , et_binds = TcEvBinds ev_binds_var
                          , et_body = wantedCtEvEvId wanted_ev }
 -                ; return (Just (Right imp')) }
 +                ; return (Right imp') }
+     }
    | otherwise  -- A Given QCInst
    = pprPanic "wantedQciToImplic: found a Given QCI" (ppr ct)
  -- No-op on all Ct's other than CQuantCan
 -solveWantedQCI _ ct = return (Just (Left ct))
 +solveWantedQCI _ ct = return (Left ct)
  {-

compiler/GHC/Tc/Types/Origin.hs

@@ -910,8 +910,9 @@ ppr_ct_origin herald (ScOrigin IsClsInst nkd)
  ppr_ct_origin _herald (ScOrigin (IsQC pred orig) nkd)
    = vcat [ whenPprDebug (text "IsQC" <> braces (text "sc-origin:" <> ppr nkd) <+> ppr pred)
 -         , ppr_ct_origin (text "arising (via a quantified constraint) from") orig ]
 -           -- Just print `orig`, with a new herald
 +         , hang (text "arising (via a quantified constraint) from") 2 (pprCtO orig) ]
 +           -- Print `orig` briefly with pprCtO.  We'll print it more voluminously later.
 +           -- See GHC.Tc.Errors.Ppr.pprQCOriginExtra
  ppr_ct_origin herald (NonLinearPatternOrigin reason pat)
    = hang (herald <+> text "a non-linear pattern" <+> quotes (ppr pat))

testsuite/tests/deriving/should_fail/T12768.stderr

  T12768.hs:9:33: error: [GHC-39999]
      • Could not deduce ‘D [a]’
 -        arising from the coercion of the method ‘op’
 -          from type ‘D [a] => [a] -> [a]’ to type ‘D (N a) => N a -> N a’
 +        arising (via a quantified constraint) from a derived method
        from the context: C a
          bound by the deriving clause for ‘C (N a)’ at T12768.hs:9:33
 -      or from: D (N a)
 -        bound by the method declaration for op at T12768.hs:9:33
 -      Possible fix:
 -        use a standalone 'deriving instance' declaration,
 -          so you can specify the instance context yourself
 +      or from: D (N a) bound by a quantified constraint at T12768.hs:9:33
 +      When trying to solve the quantified constraint
 +        D (N a) => (Coercible ([a] -> [a]) (N a -> N a), D [a])
 +        arising from the coercion of the method ‘op’
 +          from type ‘D [a] => [a] -> [a]’ to type ‘D (N a) => N a -> N a’
      • When deriving the instance for (C (N a))

testsuite/tests/deriving/should_fail/T1496.stderr

  T1496.hs:10:32: error: [GHC-18872]
      • Couldn't match representation of type: c Int
                                 with that of: c Moo
 +        arising (via a quantified constraint) from a derived method
 +      When trying to solve the quantified constraint
 +        forall (c :: * -> *). Coercible (c Int -> c Int) (c Int -> c Moo)
          arising from the coercion of the method ‘isInt’
            from type ‘forall (c :: * -> *). c Int -> c Int’
              to type ‘forall (c :: * -> *). c Int -> c Moo’

testsuite/tests/deriving/should_fail/T5498.stderr

  T5498.hs:30:39: error: [GHC-18872]
      • Couldn't match representation of type: c a
                                 with that of: c (Down a)
 +        arising (via a quantified constraint) from a derived method
 +      When trying to solve the quantified constraint
 +        forall (c :: * -> *).
 +        Coercible (c a -> c Int) (c (Down a) -> c Int)
          arising from the coercion of the method ‘intIso’
            from type ‘forall (c :: * -> *). c a -> c Int’
              to type ‘forall (c :: * -> *). c (Down a) -> c Int’

testsuite/tests/deriving/should_fail/T7148.stderr

  T7148.hs:27:40: error: [GHC-25897]
      • Couldn't match type ‘b’ with ‘Tagged a b’
 -        arising from the coercion of the method ‘iso1’
 -          from type ‘forall b1. SameType () b1 -> SameType b b1’
 -            to type ‘forall b1. SameType () b1 -> SameType (Tagged a b) b1’
 +        arising (via a quantified constraint) from a derived method
 +      When trying to solve the quantified constraint
 +        forall b1.
 +        Coercible
 +          (SameType b1 () -> SameType b1 b)
 +          (SameType b1 () -> SameType b1 (Tagged a b))
 +        arising from the coercion of the method ‘iso2’
 +          from type ‘forall b1. SameType b1 () -> SameType b1 b’
 +            to type ‘forall b1. SameType b1 () -> SameType b1 (Tagged a b)’
        ‘b’ is a rigid type variable bound by
          the deriving clause for ‘IsoUnit (Tagged a b)’
          at T7148.hs:27:40-46
@@ -10,9 +16,15 @@ T7148.hs:27:40: error: [GHC-25897]
  T7148.hs:27:40: error: [GHC-25897]
      • Couldn't match type ‘b’ with ‘Tagged a b’
 -        arising from the coercion of the method ‘iso2’
 -          from type ‘forall b1. SameType b1 () -> SameType b1 b’
 -            to type ‘forall b1. SameType b1 () -> SameType b1 (Tagged a b)’
 +        arising (via a quantified constraint) from a derived method
 +      When trying to solve the quantified constraint
 +        forall b1.
 +        Coercible
 +          (SameType () b1 -> SameType b b1)
 +          (SameType () b1 -> SameType (Tagged a b) b1)
 +        arising from the coercion of the method ‘iso1’
 +          from type ‘forall b1. SameType () b1 -> SameType b b1’
 +            to type ‘forall b1. SameType () b1 -> SameType (Tagged a b) b1’
        ‘b’ is a rigid type variable bound by
          the deriving clause for ‘IsoUnit (Tagged a b)’
          at T7148.hs:27:40-46

testsuite/tests/deriving/should_fail/T7148a.stderr

  T7148a.hs:19:50: error: [GHC-10283]
      • Couldn't match representation of type ‘b’
                                 with that of ‘Result a b’
 +        arising (via a quantified constraint) from a derived method
 +      When trying to solve the quantified constraint
 +        forall b.
 +        Coercible
 +          (Proxy b -> a -> Result a b) (Proxy b -> IS_NO_LONGER a -> b)
          arising from the coercion of the method ‘coerce’
            from type ‘forall b. Proxy b -> a -> Result a b’
              to type ‘forall b.
                       Proxy b -> IS_NO_LONGER a -> Result (IS_NO_LONGER a) b’
        ‘b’ is a rigid type variable bound by
 -        the method declaration for coerce
 +        a quantified constraint
          at T7148a.hs:19:50-56
      • When deriving the instance for (Convert (IS_NO_LONGER a))

testsuite/tests/quantified-constraints/T19690.stderr

  T19690.hs:12:16: error: [GHC-05617]
 -    • Could not solve: ‘Hold c => c’ arising from a use of ‘go’
 +    • Could not deduce ‘c’
 +        arising (via a quantified constraint) from a use of ‘go’
 +      from the context: Hold c
 +        bound by a quantified constraint at T19690.hs:12:16-17
 +      When trying to solve the quantified constraint
 +        Hold c => c
 +        arising from a use of ‘go’
      • In the expression: go
        In an equation for ‘anythingDict’:
            anythingDict
@@ -7,4 +13,6 @@ T19690.hs:12:16: error: [GHC-05617]
              where
                  go :: (Hold c => c) => Dict c
                  go = Dict
 +    • Relevant bindings include
 +        anythingDict :: Dict c (bound at T19690.hs:12:1)

testsuite/tests/quantified-constraints/T21006.stderr

  T21006.hs:14:10: error: [GHC-05617]
 -    • Could not solve: ‘forall b (c :: Constraint).
 -                        (Determines b, Determines c) =>
 -                        c’
 +    • Could not deduce ‘c’
 +        arising (via a quantified constraint) from
 +          the superclasses of an instance declaration
 +      from the context: (Determines b, Determines c)
 +        bound by a quantified constraint at T21006.hs:14:10-15
 +      When trying to solve the quantified constraint
 +        forall b (c :: Constraint). (Determines b, Determines c) => c
          arising from the superclasses of an instance declaration
      • In the instance declaration for ‘OpCode’

testsuite/tests/typecheck/should_fail/T15801.stderr

 -T15801.hs:52:10: error: [GHC-05617]
 -    • Could not solve: ‘forall (op_a :: Op (*)) (b :: Op (*)).
 -                        op_a -#- b’
 +T15801.hs:52:10: error: [GHC-18872]
 +    • Couldn't match representation of type: UnOp op_a -> UnOp b
 +                               with that of: op_a --> b
 +        arising (via a quantified constraint) from the superclasses of an instance declaration
 +      When trying to solve the quantified constraint
 +        forall (op_a :: Op (*)) (b :: Op (*)). op_a -#- b
          arising from the superclasses of an instance declaration
      • In the instance declaration for ‘OpRíki (Op (*))’

testsuite/tests/typecheck/should_fail/T22912.stderr

 -T22912.hs:17:16: error: [GHC-05617]
 -    • Could not solve: ‘Exactly (Implies c) => Implies c’
 +T22912.hs:17:16: error: [GHC-39999]
 +    • Could not deduce ‘Implies c’
 +        arising (via a quantified constraint) from a use of ‘go’
 +      from the context: Exactly (Implies c)
 +        bound by a quantified constraint at T22912.hs:17:16-17
 +      When trying to solve the quantified constraint
 +        Exactly (Implies c) => Implies c
          arising from a use of ‘go’
 +      Possible fix:
 +        add (Implies c) to the context of
 +          the type signature for:
 +            anythingDict :: forall (c :: Constraint). Dict c
      • In the expression: go
        In an equation for ‘anythingDict’:
            anythingDict