Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: 5d658dd6 by Simon Peyton Jones at 2025-10-13T07:55:47+01:00 Wibbles - - - - - 8e5e75c3 by Simon Peyton Jones at 2025-10-13T16:47:43+01:00 Wibble defaulting repr eqs - - - - - 467db3c2 by Simon Peyton Jones at 2025-10-13T16:47:56+01:00 Improve kick-out after filling coercion holes The Note needs updating if CI is happy - - - - - 8 changed files: - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Zonk/TcType.hs - testsuite/tests/rep-poly/RepPolyNPlusK.stderr - testsuite/tests/rep-poly/T14561b.stderr - testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr Changes: ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -485,13 +485,14 @@ defaultEquality encl_eqs ct ReprEq -- See Note [Defaulting representational equalities] - -- Don't even try this for definitely-insoluble representational - -- equalities such as Int ~R# Bool. + -- Don't even try this for definitely-insoluble + -- representational equalities such as Int ~R# Bool. | CIrredCan (IrredCt { ir_reason }) <- ct , isInsolubleReason ir_reason -> return False -- Nor if there are enclosing equalities + -- See (DRE1) in Note [Defaulting representational equalities] | encl_eqs -> return False @@ -697,15 +698,7 @@ Wrinkles: See #10009, and Note [Limited defaulting in the ambiguity check]. - -Note [Must simplify after defaulting] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We may have a deeply buried constraint - (t:*) ~ (a:Open) -which we couldn't solve because of the kind incompatibility, and 'a' is free. -Then when we default 'a' we can solve the constraint. And we want to do -that before starting in on type classes. We MUST do it before reporting -errors, because it isn't an error! #7967 was due to this. +(DE7) For representational equalities see Note [Defaulting representational equalities] Note [Defaulting representational equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -766,6 +759,23 @@ in which case unifying alpha := Int would be wrong, as the correct solution is alpha := Age. This worry doesn't concern us in top-level defaulting, because defaulting takes place after generalisation; it is fully monomorphic. +(DRE1) Suppose we have (see test UnliftedNewtypesCoerceFail) + [G] Coercible a b + [W] alpha ~R# beta + Then we don't want to make alpha:=beta, because we probably should really solve it + from the Given Coercible constraint. So we check first for the absence of enclosing + equalities. This is a bit ad-hoc, but so is all of defaulting really. + +Note [Must simplify after defaulting] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We may have a deeply buried constraint + (t:*) ~ (a:Open) +which we couldn't solve because of the kind incompatibility, and 'a' is free. +Then when we default 'a' we can solve the constraint. And we want to do +that before starting in on type classes. We MUST do it before reporting +errors, because it isn't an error! #7967 was due to this. + + ********************************************************************************* * * * Type-class defaulting ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -24,7 +24,7 @@ module GHC.Tc.Solver.InertSet ( -- * Inert equalities InertEqs, foldTyEqs, delEq, findEq, - partitionInertEqs, partitionFunEqs, + partitionInertEqs, partitionFunEqs, transformAndPartitionTyVarEqs, filterInertEqs, filterFunEqs, foldFunEqs, addEqToCans, @@ -1359,27 +1359,30 @@ findEq icans (TyVarLHS tv) = findTyEqs icans tv findEq icans (TyFamLHS fun_tc fun_args) = concat @Maybe (findFunEq (inert_funeqs icans) fun_tc fun_args) -{-# INLINE partition_eqs_container #-} -partition_eqs_container - :: forall container - . container -- empty container - -> (forall b. (EqCt -> b -> b) -> container -> b -> b) -- folder - -> (EqCt -> container -> container) -- extender - -> (EqCt -> Bool) - -> container - -> ([EqCt], container) -partition_eqs_container empty_container fold_container extend_container pred orig_inerts - = fold_container folder orig_inerts ([], empty_container) +transformAndPartitionTyVarEqs + :: (EqCt -> Either EqCt EqCt) -- Left => chuck out, Right => keep + -> InertEqs + -> ([EqCt], InertEqs) -- (chuck-out, keep) +transformAndPartitionTyVarEqs pred orig_inerts + = foldTyEqs folder orig_inerts ([], emptyTyEqs) where - folder :: EqCt -> ([EqCt], container) -> ([EqCt], container) + folder :: EqCt -> ([EqCt], InertEqs) -> ([EqCt], InertEqs) folder eq_ct (acc_true, acc_false) - | pred eq_ct = (eq_ct : acc_true, acc_false) - | otherwise = (acc_true, extend_container eq_ct acc_false) + = case pred eq_ct of + Left eq_ct' -> (eq_ct' : acc_true, acc_false) + Right eq_ct' -> (acc_true, addInertEqs eq_ct' acc_false) partitionInertEqs :: (EqCt -> Bool) -- EqCt will always have a TyVarLHS -> InertEqs -> ([EqCt], InertEqs) -partitionInertEqs = partition_eqs_container emptyTyEqs foldTyEqs addInertEqs +partitionInertEqs pred orig_inerts + = foldTyEqs folder orig_inerts ([], emptyTyEqs) + where + folder :: EqCt -> ([EqCt], InertEqs) -> ([EqCt], InertEqs) + folder eq_ct (acc_true, acc_false) + = case pred eq_ct of + True -> (eq_ct : acc_true, acc_false) + False -> (acc_true, addInertEqs eq_ct acc_false) addInertEqs :: EqCt -> InertEqs -> InertEqs -- Precondition: CanEqLHS is a TyVarLHS @@ -1412,7 +1415,14 @@ foldFunEqs k fun_eqs z = foldTcAppMap (\eqs z -> foldr k z eqs) fun_eqs z partitionFunEqs :: (EqCt -> Bool) -- EqCt will have a TyFamLHS -> InertFunEqs -> ([EqCt], InertFunEqs) -partitionFunEqs = partition_eqs_container emptyFunEqs foldFunEqs addFunEqs +partitionFunEqs pred orig_inerts + = foldFunEqs folder orig_inerts ([], emptyFunEqs) + where + folder :: EqCt -> ([EqCt], InertFunEqs) -> ([EqCt], InertFunEqs) + folder eq_ct (acc_true, acc_false) + = case pred eq_ct of + True -> (eq_ct : acc_true, acc_false) + False -> (acc_true, addFunEqs eq_ct acc_false) addFunEqs :: EqCt -> InertFunEqs -> InertFunEqs -- Precondition: EqCt is a TyFamLHS @@ -1424,12 +1434,11 @@ addFunEqs other _ = pprPanic "extendFunEqs" (ppr other) filterFunEqs :: (EqCt -> Bool) -> InertFunEqs -> InertFunEqs filterFunEqs f = mapMaybeTcAppMap g where - g xs = - let filtered = filter f xs - in - if null filtered - then Nothing - else Just filtered + g xs | null filtered = Nothing + | otherwise = Just filtered + where + filtered = filter f xs + {- ********************************************************************* * * ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -190,7 +190,6 @@ import GHC.Types.DefaultEnv ( DefaultEnv ) import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Unique.Supply -import GHC.Types.Unique.Set( elementOfUniqSet ) import GHC.Types.Id import GHC.Types.Basic (allImportLevels) import GHC.Types.ThLevelIndex (thLevelIndexFromImportLevel) @@ -458,15 +457,16 @@ kickOutAfterUnification tv_set ; traceTcS "kickOutAfterUnification" (ppr tv_set $$ text "n_kicked =" <+> ppr n_kicked) ; return n_kicked } -kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () +kickOutAfterFillingCoercionHole :: CoercionHole -> Coercion -> TcS () -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty] -- in GHC.Tc.Solver.Equality -- -- It's possible that this could just go ahead and unify, but could there -- be occurs-check problems? Seems simpler just to kick out. -kickOutAfterFillingCoercionHole hole +kickOutAfterFillingCoercionHole hole co = do { ics <- getInertCans - ; let (kicked_out, ics') = kick_out ics + ; new_holes <- liftZonkTcS $ TcM.freeHolesOfCoercion co + ; let (kicked_out, ics') = kick_out new_holes ics n_kicked = length kicked_out ; unless (n_kicked == 0) $ @@ -479,20 +479,25 @@ kickOutAfterFillingCoercionHole hole ; setInertCans ics' } where - kick_out :: InertCans -> ([EqCt], InertCans) - kick_out ics@(IC { inert_eqs = eqs }) + kick_out :: RewriterSet -> InertCans -> ([EqCt], InertCans) + kick_out new_holes ics@(IC { inert_eqs = eqs }) = (eqs_to_kick, ics { inert_eqs = eqs_to_keep }) where - (eqs_to_kick, eqs_to_keep) = partitionInertEqs kick_out_eq eqs + (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs (kick_out_eq new_holes) eqs - kick_out_eq :: EqCt -> Bool -- True: kick out; False: keep. - kick_out_eq (EqCt { eq_ev = ev ,eq_lhs = lhs }) - | CtWanted (WantedCt { ctev_rewriters = RewriterSet rewriters }) <- ev + kick_out_eq :: RewriterSet -> EqCt -> Either EqCt EqCt + kick_out_eq new_holes eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs }) + | CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev , TyVarLHS tv <- lhs , isMetaTyVar tv - = hole `elementOfUniqSet` rewriters + , hole `elemRewriterSet` rewriters + , let holes' = (rewriters `delRewriterSet` hole) `mappend` new_holes + eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) } + = if isEmptyRewriterSet holes' + then Left eq_ct' -- Kick out + else Right eq_ct' -- Keep, but with trimmed holes | otherwise - = False + = Right eq_ct -------------- insertSafeOverlapFailureTcS :: InstanceWhat -> DictCt -> TcS () @@ -1990,7 +1995,7 @@ Yuk! fillCoercionHole :: CoercionHole -> Coercion -> TcS () fillCoercionHole hole co = do { wrapTcS $ TcM.fillCoercionHole hole co - ; kickOutAfterFillingCoercionHole hole } + ; kickOutAfterFillingCoercionHole hole co } setEvBindIfWanted :: CtEvidence -> CanonicalEvidence -> EvTerm -> TcS () setEvBindIfWanted ev canonical tm ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -88,9 +88,10 @@ module GHC.Tc.Types.Constraint ( GivenCtEvidence(..), WantedCtEvidence(..), -- RewriterSet - RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, - -- exported concretely only for zonkRewriterSet + -- RewriterSet(..) is exported concretely only for zonkRewriterSet + RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, elemRewriterSet, addRewriter, unitRewriterSet, unionRewriterSet, rewriterSetFromCts, + delRewriterSet, wrapType, @@ -2506,6 +2507,12 @@ emptyRewriterSet = RewriterSet emptyUniqSet unitRewriterSet :: CoercionHole -> RewriterSet unitRewriterSet = coerce (unitUniqSet @CoercionHole) +elemRewriterSet :: CoercionHole -> RewriterSet -> Bool +elemRewriterSet = coerce (elementOfUniqSet @CoercionHole) + +delRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet +delRewriterSet = coerce (delOneFromUniqSet @CoercionHole) + unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet unionRewriterSet = coerce (unionUniqSets @CoercionHole) ===================================== compiler/GHC/Tc/Zonk/TcType.hs ===================================== @@ -43,6 +43,7 @@ module GHC.Tc.Zonk.TcType -- * Coercion holes , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe + , freeHolesOfCoercion -- * Tidying @@ -583,30 +584,33 @@ zonkCtEvRewriterSet ev@(CtWanted wtd) -- find all the free un-filled coercion holes in the coercion that fills it zonkRewriterSet :: RewriterSet -> ZonkM RewriterSet zonkRewriterSet (RewriterSet set) - = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set + = unUCHM (nonDetStrictFoldUniqSet go mempty 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) -- Not filled - Just co -> unUCHM (check_co co) } -- Filled: look inside - - 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 + go :: CoercionHole -> UnfilledCoercionHoleMonoid -> UnfilledCoercionHoleMonoid + go hole m_acc = freeHolesOfHole hole `mappend` m_acc + +freeHolesOfCoercion :: Coercion -> ZonkM RewriterSet +freeHolesOfCoercion co = unUCHM (freeHolesOfCo co) + +freeHolesOfHole :: CoercionHole -> UnfilledCoercionHoleMonoid +freeHolesOfHole hole + = UCHM $ do { m_co <- unpackCoercionHole_maybe hole + ; case m_co of + Nothing -> return (unitRewriterSet hole) -- Not filled + Just co -> unUCHM (freeHolesOfCo co) } -- Filled: look inside + +freeHolesOfTy :: Type -> UnfilledCoercionHoleMonoid +freeHolesOfCo :: Coercion -> UnfilledCoercionHoleMonoid +(freeHolesOfTy, _, freeHolesOfCo, _) = foldTyCo freeHolesFolder () + +freeHolesFolder :: TyCoFolder () UnfilledCoercionHoleMonoid +freeHolesFolder = TyCoFolder { tcf_view = noView + , tcf_tyvar = \ _ tv -> freeHolesOfTy (tyVarKind tv) + , tcf_covar = \ _ cv -> freeHolesOfTy (varType cv) + , tcf_hole = \ _ h -> freeHolesOfHole h , tcf_tycobinder = \ _ _ _ -> () } newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM RewriterSet } ===================================== testsuite/tests/rep-poly/RepPolyNPlusK.stderr ===================================== @@ -9,21 +9,21 @@ RepPolyNPlusK.hs:22:6: error: [GHC-55287] arising from the literal ‘2’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE rep0 + a1 :: TYPE rep2 When unifying: - • a0 + • a1 • a - Cannot unify ‘rep1’ with the type variable ‘rep0’ + Cannot unify ‘rep1’ with the type variable ‘rep2’ because the former is not a concrete ‘RuntimeRep’. • The first argument of the rebindable syntax operator ‘(-)’ arising from the literal ‘2’ does not have a fixed runtime representation. Its type is: - a1 :: TYPE rep2 + a0 :: TYPE rep0 When unifying: - • a1 + • a0 • a - Cannot unify ‘rep1’ with the type variable ‘rep2’ + Cannot unify ‘rep1’ with the type variable ‘rep0’ because the former is not a concrete ‘RuntimeRep’. • In the pattern: bndr_a+2 In an equation for ‘foo’: foo (bndr_a+2) = () ===================================== testsuite/tests/rep-poly/T14561b.stderr ===================================== @@ -2,9 +2,9 @@ T14561b.hs:12:9: error: [GHC-55287] • The first argument of ‘coerce’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE k0 + b0 :: TYPE k0 When unifying: - • a0 -> b0 + • b0 -> b0 • a -> a Cannot unify ‘r’ with the type variable ‘k0’ because the former is not a concrete ‘RuntimeRep’. ===================================== testsuite/tests/rep-poly/UnliftedNewtypesCoerceFail.stderr ===================================== @@ -2,9 +2,9 @@ UnliftedNewtypesCoerceFail.hs:14:8: error: [GHC-55287] • The first argument of ‘coerce’ does not have a fixed runtime representation. Its type is: - b0 :: TYPE k0 + a0 :: TYPE k0 When unifying: - • b0 -> b0 + • a0 -> b0 • x -> y Cannot unify ‘rep’ with the type variable ‘k0’ because the former is not a concrete ‘RuntimeRep’. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/c6ea5c8355a2600e145f0cfb833c97d... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/c6ea5c8355a2600e145f0cfb833c97d... You're receiving this email because of your account on gitlab.haskell.org.