Simon Peyton Jones pushed to branch wip/T25440 at Glasgow Haskell Compiler / GHC Commits: be011dac by Simon Peyton Jones at 2025-04-18T13:12:23+01:00 Wibbles - - - - - 12 changed files: - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Zonk/TcType.hs - compiler/GHC/Tc/Zonk/Type.hs - testsuite/tests/indexed-types/should_fail/T3330c.stderr - testsuite/tests/indexed-types/should_fail/T4174.stderr - testsuite/tests/indexed-types/should_fail/T8227.stderr - testsuite/tests/typecheck/should_fail/T18851.stderr Changes: ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -466,13 +466,12 @@ mkErrorItem ct = do { let loc = ctLoc ct flav = ctFlavour ct - ; (suppress, m_evdest) <- case ctEvidence ct of - -- For this `suppress` stuff - -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint - CtGiven {} -> return (False, Nothing) - CtWanted (WantedCt { ctev_rewriters = rewriters, ctev_dest = dest }) - -> do { rewriters' <- zonkRewriterSet rewriters - ; return (not (isEmptyRewriterSet rewriters'), Just dest) } + (suppress, m_evdest) = case ctEvidence ct of + -- For this `suppress` stuff + -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint + CtGiven {} -> (False, Nothing) + CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest }) + -> (not (isEmptyRewriterSet rws), Just dest) ; let m_reason = case ct of CIrredCan (IrredCt { ir_reason = reason }) -> Just reason @@ -503,7 +502,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics , text "tidy_errs =" <+> ppr tidy_errs ]) -- Catch an awkward (and probably rare) case in which /all/ errors are - -- suppressed: see Wrinkle (WRW2) in Note [Prioritise Wanteds with empty + -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty -- RewriterSet] in GHC.Tc.Types.Constraint. -- -- Unless we are sure that an error will be reported some other way ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -1081,9 +1081,9 @@ disambigProposalSequences orig_wanteds wanteds proposalSequences allConsistent ; successes <- fmap catMaybes $ nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) $ mapM firstSuccess proposalSequences - ; traceTcS "disambigProposalSequences" (vcat [ ppr wanteds - , ppr proposalSequences - , ppr successes ]) + ; traceTcS "disambigProposalSequences {" (vcat [ ppr wanteds + , ppr proposalSequences + , ppr successes ]) -- Step (4) in Note [How type-class constraints are defaulted] ; case successes of success@(tvs, subst) : rest ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -2077,11 +2077,15 @@ Wrinkles: that `kw`. (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets - solved. This is done in kickOutAfterFillingCoercionHole, which kicks out + solved. This is done in `kickOutAfterFillingCoercionHole`, which kicks out all equalities whose RHS mentions the filled-in coercion hole. Note that it looks for type family equalities, too, because of the use of unifyTest in canEqTyVarFunEq. + To do this, we slightly-hackily use the `ctev_rewriters` field of the inert, + which records that `w` has been rewritten by `kw`. + See (WRW3) in Note [Wanteds reewrite Wanteds] in GHC.Tc.Types.Constraint. + (EIK2b) What if the RHS mentions /other/ coercion holes? How can that happen? The main way is like this. Assume F :: forall k. k -> Type [W] kw : k ~ Type @@ -2615,6 +2619,7 @@ But it's not so simple: error message that we can solve (F a ~ a Int) arising from F a ~ F a Better to hang on to `g1`, in preference to `g2`. + See (WRW1) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. -} tryInertEqs :: EqCt -> SolverStage () ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -150,7 +150,6 @@ import qualified GHC.Tc.Utils.Env as TcM , topIdLvl ) import GHC.Tc.Zonk.Monad ( ZonkM ) import qualified GHC.Tc.Zonk.TcType as TcM -import qualified GHC.Tc.Zonk.Type as TcM import GHC.Driver.DynFlags @@ -489,7 +488,7 @@ kickOutAfterFillingCoercionHole hole kick_out ics@(IC { inert_irreds = irreds }) = -- We only care about irreds here, because any constraint blocked -- by a coercion hole is an irred. See wrinkle (EIK2a) in - -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical + -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality (irreds_to_kick, ics { inert_irreds = irreds_to_keep }) where (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds @@ -1457,8 +1456,8 @@ emitWork cts -- c1 is rewritten by another, c2. When c2 gets solved, -- c1 has no rewriters, and can be prioritised; see -- Note [Prioritise Wanteds with empty RewriterSet] - -- in GHC.Tc.Types.Constraint wrinkle (WRW1) - ; cts <- wrapTcS $ mapBagM TcM.zonkCtRewriterSet cts + -- in GHC.Tc.Types.Constraint wrinkle (PER1) + ; cts <- liftZonkTcS $ mapBagM TcM.zonkCtRewriterSet cts ; updWorkListTcS (extendWorkListCts cts) } emitImplication :: Implication -> TcS () @@ -2252,7 +2251,7 @@ wrapUnifierX ev role do_unifications ; wrapTcS $ do { defer_ref <- TcM.newTcRef emptyBag ; unified_ref <- TcM.newTcRef [] - ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev) + ; rewriters <- TcM.liftZonkM (TcM.zonkRewriterSet (ctEvRewriters ev)) ; let env = UE { u_role = role , u_rewriters = rewriters , u_loc = ctEvLoc ev ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -240,7 +240,7 @@ instance Outputable DictCt where {- Note [Canonical equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ An EqCt is a canonical equality constraint, one that can live in the inert set, -and that can be used to rewrite other constrtaints. It satisfies these invariants: +and that can be used to rewrite other constraints. It satisfies these invariants: * (TyEq:OC) lhs does not occur in rhs (occurs check) Note [EqCt occurs check] * (TyEq:F) rhs has no foralls @@ -2444,19 +2444,29 @@ We thus want Wanteds to rewrite Wanteds in order to accept more programs, but we don't want Wanteds to rewrite Wanteds because doing so can create inscrutable error messages. To solve this dilemma: -* We allow Wanteds to rewrite Wanteds, but... +* We allow Wanteds to rewrite Wanteds, but each Wanted tracks the set of Wanteds + it has been rewritten by, in its RewriterSet, stored in the ctev_rewriters + field of the CtWanted constructor of CtEvidence. (Only Wanteds have + RewriterSets.) -* Each Wanted tracks the set of Wanteds it has been rewritten by, in its - RewriterSet, stored in the ctev_rewriters field of the CtWanted - constructor of CtEvidence. (Only Wanteds have RewriterSets.) +* A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient + because only equalities (evidenced by coercion holes) are used for rewriting; + other (dictionary) constraints cannot ever rewrite. + +* The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet, + consisting of the evidence (a CoercionHole) for any Wanted equalities used in + rewriting. + +* Then GHC.Tc.Solver.Solve.rewriteEvidence and GHC.Tc.Solver.Equality.rewriteEqEvidence + add this RewriterSet to the rewritten constraint's rewriter set. * In error reporting, we simply suppress any errors that have been rewritten by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, - which uses GHC.Tc.Zonk.Type.zonkRewriterSet to look through any filled + which uses `GHC.Tc.Zonk.Type.zonkRewriterSet` to look through any filled coercion holes. The idea is that we wish to report the "root cause" -- the error that rewrote all the others. -* We prioritise Wanteds that have an empty RewriterSet: +* In error reporting, we prioritise Wanteds that have an empty RewriterSet: see Note [Prioritise Wanteds with empty RewriterSet]. Let's continue our first example above: @@ -2471,19 +2481,30 @@ Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding The {w1} in the second line of output is the RewriterSet of w1. -A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient -because only equalities (evidenced by coercion holes) are used for rewriting; -other (dictionary) constraints cannot ever rewrite. The rewriter (in -e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet, -consisting of the evidence (a CoercionHole) for any Wanted equalities used in -rewriting. Then GHC.Tc.Solver.Solve.rewriteEvidence and -GHC.Tc.Solver.Equality.rewriteEqEvidence add this RewriterSet to the rewritten -constraint's rewriter set. +Wrinkles: + +(WRW1) When we find a constraint identical to one already in the inert set, + we solve one from the other. Other things being equal, keep the one + that has fewer (better still no) rewriters. + See (CE4) in Note [Combining equalities] in GHC.Tc.Solver.Equality. + + To this accurately we should use `zonkRewriterSet` during canonicalisation, + to eliminate rewriters that have now been solved. Currently we only do so + during error reporting; but perhaps we should change that. + +(WRW2) When zonk a constraint (with `zonkCt` and `zonkCtEvidence`) we take + the opportunity to zonk its `RewriterSet, which eliminates solved ones`. + This doesn't guarantee that rewriter sets are always up to date -- see + (WRW1) -- but it helps, and it de-clutters debug output. + +(WRW3) We use the rewriter set for a slightly different purpose, in (EIK2) + of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality. + This is a bit of a hack. Note [Prioritise Wanteds with empty RewriterSet] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When extending the WorkList, in GHC.Tc.Solver.InertSet.extendWorkListEq, -we priorities constraints that have no rewriters. Here's why. +we prioritise constraints that have no rewriters. Here's why. Consider this, which came up in T22793: inert: {} @@ -2527,11 +2548,11 @@ GHC.Tc.Solver.InertSet.extendWorkListEq, and extendWorkListEqs. Wrinkles -(WRW1) Before checking for an empty RewriterSet, we zonk the RewriterSet, +(PER1) Before checking for an empty RewriterSet, we zonk the RewriterSet, because some of those CoercionHoles may have been filled in since we last looked: see GHC.Tc.Solver.Monad.emitWork. -(WRW2) Despite the prioritisation, it is hard to be /certain/ that we can't end up +(PER2) Despite the prioritisation, it is hard to be /certain/ that we can't end up in a situation where all of the Wanteds have rewritten each other. In order to report /some/ error in this case, we simply report all the Wanteds. The user will get a perhaps-confusing error message, but they've ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -49,7 +49,6 @@ module GHC.Tc.Utils.TcMType ( newCoercionHole, newCoercionHoleO, newVanillaCoercionHole, fillCoercionHole, isFilledCoercionHole, - unpackCoercionHole, unpackCoercionHole_maybe, checkCoercionHole, newImplication, @@ -115,7 +114,6 @@ import GHC.Tc.Types.CtLoc( CtLoc, ctLocOrigin ) import GHC.Tc.Utils.Monad -- TcType, amongst others import GHC.Tc.Utils.TcType import GHC.Tc.Errors.Types -import GHC.Tc.Zonk.Type import GHC.Tc.Zonk.TcType import GHC.Builtin.Names @@ -1583,7 +1581,7 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co go_co dv (SubCo co) = go_co dv co go_co dv (HoleCo hole) - = do m_co <- unpackCoercionHole_maybe hole + = do m_co <- liftZonkM (unpackCoercionHole_maybe hole) case m_co of Just co -> go_co dv co Nothing -> go_cv dv (coHoleCoVar hole) ===================================== compiler/GHC/Tc/Zonk/TcType.hs ===================================== @@ -1,3 +1,5 @@ +{-# LANGUAGE DuplicateRecordFields #-} + {- (c) The University of Glasgow 2006 (c) The AQUA Project, Glasgow University, 1996-1998 @@ -36,6 +38,13 @@ module GHC.Tc.Zonk.TcType -- ** Zonking constraints , zonkCt, zonkWC, zonkSimples, zonkImplication + -- * Rewriter sets + , zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet + + -- * Coercion holes + , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe + + -- * Tidying , tcInitTidyEnv, tcInitOpenTidyEnv , tidyCt, tidyEvVar, tidyDelayedError @@ -81,7 +90,7 @@ import GHC.Core.Coercion import GHC.Core.Predicate import GHC.Utils.Constants -import GHC.Utils.Outputable +import GHC.Utils.Outputable as Outputable import GHC.Utils.Misc import GHC.Utils.Monad ( mapAccumLM ) import GHC.Utils.Panic @@ -89,6 +98,9 @@ import GHC.Utils.Panic import GHC.Data.Bag import GHC.Data.Pair +import Data.Semigroup +import Data.Maybe + {- ********************************************************************* * * Writing to metavariables @@ -366,8 +378,8 @@ checkCoercionHole cv co ; return $ assertPpr (ok cv_ty) (text "Bad coercion hole" <+> - ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role - , ppr cv_ty ]) + ppr cv Outputable.<> colon + <+> vcat [ ppr t1, ppr t2, ppr role, ppr cv_ty ]) co } | otherwise = return co @@ -494,9 +506,15 @@ zonkCt ct ; return (mkNonCanonical fl') } zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence -zonkCtEvidence ctev - = do { pred' <- zonkTcType (ctEvPred ctev) - ; return (setCtEvPredType ctev pred') } +-- Zonks the ctev_pred and the ctev_rewriters; but not ctev_evar +-- For ctev_rewriters, see (WRW2) in Note [Wanteds rewrite Wanteds] +zonkCtEvidence (CtGiven (GivenCt { ctev_pred = pred, ctev_evar = var, ctev_loc = loc })) + = do { pred' <- zonkTcType pred + ; return (CtGiven (GivenCt { ctev_pred = pred', ctev_evar = var, ctev_loc = loc })) } +zonkCtEvidence (CtWanted wanted@(WantedCt { ctev_pred = pred, ctev_rewriters = rws })) + = do { pred' <- zonkTcType pred + ; rws' <- zonkRewriterSet rws + ; return (CtWanted (wanted { ctev_pred = pred', ctev_rewriters = rws' })) } zonkSkolemInfo :: SkolemInfo -> ZonkM SkolemInfo zonkSkolemInfo (SkolemInfo u sk) = SkolemInfo u <$> zonkSkolemInfoAnon sk @@ -530,6 +548,103 @@ win. But c.f Note [Sharing when zonking to Type] in GHC.Tc.Zonk.Type. +%************************************************************************ +%* * + Zonking rewriter sets +* * +************************************************************************ +-} + +zonkCtRewriterSet :: Ct -> ZonkM Ct +zonkCtRewriterSet ct + | isGivenCt ct + = return ct + | otherwise + = case ct of + CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CEqCan (eq { eq_ev = ev' })) } + CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CIrredCan (ir { ir_ev = ev' })) } + CDictCan di@(DictCt { di_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CDictCan (di { di_ev = ev' })) } + CQuantCan {} -> return ct + CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CNonCanonical ev') } + +zonkCtEvRewriterSet :: CtEvidence -> ZonkM CtEvidence +zonkCtEvRewriterSet ev@(CtGiven {}) + = return ev +zonkCtEvRewriterSet ev@(CtWanted wtd) + = do { rewriters' <- zonkRewriterSet (ctEvRewriters ev) + ; return (CtWanted $ setWantedCtEvRewriters wtd rewriters') } + +-- | Check whether any coercion hole in a RewriterSet is still unsolved. +-- Does this by recursively looking through filled coercion holes until +-- one is found that is not yet filled in, at which point this aborts. +zonkRewriterSet :: RewriterSet -> ZonkM RewriterSet +zonkRewriterSet (RewriterSet set) + = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set + -- this does not introduce non-determinism, because the only + -- monadic action is to read, and the combining function is + -- commutative + where + go :: CoercionHole -> ZonkM RewriterSet -> ZonkM RewriterSet + go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc + + check_hole :: CoercionHole -> ZonkM RewriterSet + check_hole hole = do { m_co <- unpackCoercionHole_maybe hole + ; case m_co of + Nothing -> return (unitRewriterSet hole) + Just co -> unUCHM (check_co co) } + + check_ty :: Type -> UnfilledCoercionHoleMonoid + check_co :: Coercion -> UnfilledCoercionHoleMonoid + (check_ty, _, check_co, _) = foldTyCo folder () + + folder :: TyCoFolder () UnfilledCoercionHoleMonoid + folder = TyCoFolder { tcf_view = noView + , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv) + , tcf_covar = \ _ cv -> check_ty (varType cv) + , tcf_hole = \ _ -> UCHM . check_hole + , tcf_tycobinder = \ _ _ _ -> () } + +newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM RewriterSet } + +instance Semigroup UnfilledCoercionHoleMonoid where + UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r) + +instance Monoid UnfilledCoercionHoleMonoid where + mempty = UCHM (return emptyRewriterSet) + + +{- +************************************************************************ +* * + Checking for coercion holes +* * +************************************************************************ +-} + +-- | Is a coercion hole filled in? +isFilledCoercionHole :: CoercionHole -> ZonkM Bool +isFilledCoercionHole (CoercionHole { ch_ref = ref }) + = isJust <$> readTcRef ref + +-- | Retrieve the contents of a coercion hole. Panics if the hole +-- is unfilled +unpackCoercionHole :: CoercionHole -> ZonkM Coercion +unpackCoercionHole hole + = do { contents <- unpackCoercionHole_maybe hole + ; case contents of + Just co -> return co + Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) } + +-- | Retrieve the contents of a coercion hole, if it is filled +unpackCoercionHole_maybe :: CoercionHole -> ZonkM (Maybe Coercion) +unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref + + +{- %************************************************************************ %* * Tidying ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -28,12 +28,6 @@ module GHC.Tc.Zonk.Type ( -- ** 'ZonkEnv', and the 'ZonkT' and 'ZonkBndrT' monad transformers module GHC.Tc.Zonk.Env, - -- * Coercion holes - isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe, - - -- * Rewriter sets - zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet, - -- * Tidying tcInitTidyEnv, tcInitOpenTidyEnv, @@ -55,7 +49,6 @@ import GHC.Tc.TyCl.Build ( TcMethInfo, MethInfo ) import GHC.Tc.Utils.Env ( tcLookupGlobalOnly ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Monad ( newZonkAnyType, setSrcSpanA, liftZonkM, traceTc, addErr ) -import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence import GHC.Tc.Errors.Types import GHC.Tc.Zonk.Env @@ -88,7 +81,6 @@ import GHC.Types.Id import GHC.Types.TypeEnv import GHC.Types.Basic import GHC.Types.SrcLoc -import GHC.Types.Unique.Set import GHC.Types.Unique.FM import GHC.Types.TyThing @@ -99,7 +91,6 @@ import GHC.Data.Bag import Control.Monad import Control.Monad.Trans.Class ( lift ) -import Data.Semigroup import Data.List.NonEmpty ( NonEmpty ) import Data.Foldable ( toList ) @@ -1956,89 +1947,3 @@ finding the free type vars of an expression is necessarily monadic operation. (consider /\a -> f @ b, where b is side-effected to a) -} -{- -************************************************************************ -* * - Checking for coercion holes -* * -************************************************************************ --} - --- | Is a coercion hole filled in? -isFilledCoercionHole :: CoercionHole -> TcM Bool -isFilledCoercionHole (CoercionHole { ch_ref = ref }) - = isJust <$> readTcRef ref - --- | Retrieve the contents of a coercion hole. Panics if the hole --- is unfilled -unpackCoercionHole :: CoercionHole -> TcM Coercion -unpackCoercionHole hole - = do { contents <- unpackCoercionHole_maybe hole - ; case contents of - Just co -> return co - Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) } - --- | Retrieve the contents of a coercion hole, if it is filled -unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion) -unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref - -zonkCtRewriterSet :: Ct -> TcM Ct -zonkCtRewriterSet ct - | isGivenCt ct - = return ct - | otherwise - = case ct of - CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev - ; return (CEqCan (eq { eq_ev = ev' })) } - CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev - ; return (CIrredCan (ir { ir_ev = ev' })) } - CDictCan di@(DictCt { di_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev - ; return (CDictCan (di { di_ev = ev' })) } - CQuantCan {} -> return ct - CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev - ; return (CNonCanonical ev') } - -zonkCtEvRewriterSet :: CtEvidence -> TcM CtEvidence -zonkCtEvRewriterSet ev@(CtGiven {}) - = return ev -zonkCtEvRewriterSet ev@(CtWanted wtd) - = do { rewriters' <- zonkRewriterSet (ctEvRewriters ev) - ; return (CtWanted $ setWantedCtEvRewriters wtd rewriters') } - --- | Check whether any coercion hole in a RewriterSet is still unsolved. --- Does this by recursively looking through filled coercion holes until --- one is found that is not yet filled in, at which point this aborts. -zonkRewriterSet :: RewriterSet -> TcM RewriterSet -zonkRewriterSet (RewriterSet set) - = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set - -- this does not introduce non-determinism, because the only - -- monadic action is to read, and the combining function is - -- commutative - where - go :: CoercionHole -> TcM RewriterSet -> TcM RewriterSet - go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc - - check_hole :: CoercionHole -> TcM RewriterSet - check_hole hole = do { m_co <- unpackCoercionHole_maybe hole - ; case m_co of - Nothing -> return (unitRewriterSet hole) - Just co -> unUCHM (check_co co) } - - check_ty :: Type -> UnfilledCoercionHoleMonoid - check_co :: Coercion -> UnfilledCoercionHoleMonoid - (check_ty, _, check_co, _) = foldTyCo folder () - - folder :: TyCoFolder () UnfilledCoercionHoleMonoid - folder = TyCoFolder { tcf_view = noView - , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv) - , tcf_covar = \ _ cv -> check_ty (varType cv) - , tcf_hole = \ _ -> UCHM . check_hole - , tcf_tycobinder = \ _ _ _ -> () } - -newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM RewriterSet } - -instance Semigroup UnfilledCoercionHoleMonoid where - UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r) - -instance Monoid UnfilledCoercionHoleMonoid where - mempty = UCHM (return emptyRewriterSet) ===================================== testsuite/tests/indexed-types/should_fail/T3330c.stderr ===================================== @@ -1,16 +1,24 @@ - -T3330c.hs:25:43: error: [GHC-18872] - • Couldn't match kind ‘* -> *’ with ‘*’ - When matching types - f1 :: * -> * - f1 x :: * - Expected: Der ((->) x) (Der f1 x) - Actual: R f1 - • In the first argument of ‘plug’, namely ‘rf’ +T3330c.hs:25:38: error: [GHC-25897] + • Could not deduce ‘Der f1 ~ f1’ + from the context: f ~ (f1 :+: g) + bound by a pattern with constructor: + RSum :: forall (f :: * -> *) (g :: * -> *). + R f -> R g -> R (f :+: g), + in an equation for ‘plug'’ + at T3330c.hs:25:8-17 + Expected: x -> f1 x + Actual: x -> Der f1 x + ‘f1’ is a rigid type variable bound by + a pattern with constructor: + RSum :: forall (f :: * -> *) (g :: * -> *). + R f -> R g -> R (f :+: g), + in an equation for ‘plug'’ + at T3330c.hs:25:8-17 + • The function ‘plug’ is applied to three visible arguments, + but its type ‘Rep f => Der f x -> x -> f x’ has only two In the first argument of ‘Inl’, namely ‘(plug rf df x)’ In the expression: Inl (plug rf df x) • Relevant bindings include - x :: x (bound at T3330c.hs:25:29) df :: Der f1 x (bound at T3330c.hs:25:25) rf :: R f1 (bound at T3330c.hs:25:13) - plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:25:1) + ===================================== testsuite/tests/indexed-types/should_fail/T4174.stderr ===================================== @@ -1,6 +1,16 @@ - -T4174.hs:45:12: error: [GHC-18872] - • Couldn't match type ‘False’ with ‘True’ - arising from a use of ‘sync_large_objects’ +T4174.hs:45:12: error: [GHC-25897] + • Couldn't match type ‘a’ with ‘SmStep’ + Expected: m (Field (Way (GHC6'8 minor) n t p) a b) + Actual: m (Field (WayOf m) SmStep RtsSpinLock) + ‘a’ is a rigid type variable bound by + the type signature for: + testcase :: forall (m :: * -> *) minor n t p a b. + Monad m => + m (Field (Way (GHC6'8 minor) n t p) a b) + at T4174.hs:44:1-63 • In the expression: sync_large_objects In an equation for ‘testcase’: testcase = sync_large_objects + • Relevant bindings include + testcase :: m (Field (Way (GHC6'8 minor) n t p) a b) + (bound at T4174.hs:45:1) + ===================================== testsuite/tests/indexed-types/should_fail/T8227.stderr ===================================== @@ -13,12 +13,3 @@ T8227.hs:24:27: error: [GHC-83865] absoluteToParam :: Scalar (V a) -> a -> Scalar (V a) (bound at T8227.hs:24:1) -T8227.hs:24:48: error: [GHC-27958] - • Couldn't match type ‘p0’ with ‘Scalar (V p0)’ - arising from a type equality Scalar (V a) ~ Scalar (V p0) -> p0 - The type variable ‘p0’ is ambiguous - • In the second argument of ‘arcLengthToParam’, namely ‘eps’ - In the expression: arcLengthToParam eps eps - In an equation for ‘absoluteToParam’: - absoluteToParam eps seg = arcLengthToParam eps eps - ===================================== testsuite/tests/typecheck/should_fail/T18851.stderr ===================================== @@ -1,7 +1,7 @@ - T18851.hs:35:5: error: [GHC-18872] - • Couldn't match type ‘B’ with ‘A’ - arising from a superclass required to satisfy ‘C int0 A’, + • Couldn't match type ‘Bool’ with ‘B’ + arising from a superclass required to satisfy ‘C Int B’, arising from a use of ‘f’ • In the expression: f @A @B In an equation for ‘g’: g = f @A @B + View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/be011dacff5ef7a07d59ecd52ef5c6e2... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/be011dacff5ef7a07d59ecd52ef5c6e2... You're receiving this email because of your account on gitlab.haskell.org.