Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: 6b850513 by Simon Peyton Jones at 2025-12-08T23:49:06+00:00 Further wibbles Finally cracks #T22652! A bit more to document though - - - - - 5 changed files: - compiler/GHC/Core/TyCon.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - testsuite/tests/typecheck/should_fail/T15767.stderr Changes: ===================================== compiler/GHC/Core/TyCon.hs ===================================== @@ -64,7 +64,7 @@ module GHC.Core.TyCon( isTypeDataTyCon, isEnumerationTyCon, isNewTyCon, isAbstractTyCon, - isFamilyTyCon, isOpenFamilyTyCon, + isFamilyTyCon, isOpenFamilyTyCon, famTyConHasInjectivity, isTypeFamilyTyCon, isDataFamilyTyCon, isOpenTypeFamilyTyCon, isClosedFamilyTyCon_maybe, tyConInjectivityInfo, @@ -2524,6 +2524,19 @@ isBuiltInSynFamTyCon_maybe (TyCon { tyConDetails = details }) | FamilyTyCon {famTcFlav = BuiltInSynFamTyCon ops} <- details = Just ops | otherwise = Nothing +famTyConHasInjectivity :: TyCon -> Bool +-- True if knowing something about the result may tell us +-- something (not necessarily everything) about the arguments +famTyConHasInjectivity (TyCon { tyConDetails = details }) + | FamilyTyCon { famTcFlav = flav, famTcInj = inj } <- details + = case (flav, inj) of + (ClosedSynFamilyTyCon (Just {}), _) -> True + (BuiltInSynFamTyCon {}, _) -> True + (_, Injective {}) -> True + _ -> False + | otherwise + = False + -- | Extract type variable naming the result of injective type family tyConFamilyResVar_maybe :: TyCon -> Maybe Name tyConFamilyResVar_maybe (TyCon { tyConDetails = details }) ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -36,6 +36,7 @@ import GHC.Types.Var.Set import GHC.Utils.Outputable import GHC.Utils.Panic +import Control.Monad( unless ) import GHC.Data.Pair import Data.Maybe( isNothing, isJust, mapMaybe ) @@ -350,9 +351,9 @@ tryDictFunDepsLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) | otherwise = improveFromAnother (ctEvPred inert_ev) work_pred -insolubleFunDep :: CtEvidence -> TcS (StopOrContinue ()) +insolubleFunDep :: CtEvidence -> TcS (StopOrContinue a) -- The fundeps generated an insoluble constraint. --- Stop solving with an (insoluble) CIrredCan +-- Stop solving with an (insoluble) CIrredCan -- a bit like thowing an exception -- It's valuable to flag such constraints as insoluble becuase that improves -- pattern-match overlap checking insolubleFunDep ev @@ -495,16 +496,16 @@ tryFamEqFunDeps eqs_for_me fam_tc work_args = if isGiven ev then tryGivenBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_item else do { -- Note [Do local fundeps before top-level instances] - tryFDEqns fam_tc work_args work_item $ - mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs + eqns <- mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs + ; tryFDEqns fam_tc work_args work_item eqns - ; if hasRelevantGiven eqs_for_me work_args work_item - ; then nopStage () - else tryFDEqns fam_tc work_args work_item $ - mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs } + ; unless (hasRelevantGiven eqs_for_me work_args work_item) $ + do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs + ; tryFDEqns fam_tc work_args work_item eqns } } - | isGiven ev -- See (INJFAM:Given) - = nopStage () +-- | isGiven ev -- See (INJFAM:Given) +-- = nopStage () +-- Continue even for Givens in the hope of discovering insolubility -- Only Wanted constraints below here @@ -512,24 +513,23 @@ tryFamEqFunDeps eqs_for_me fam_tc work_args = do { -- Note [Do local fundeps before top-level instances] case tyConInjectivityInfo fam_tc of NotInjective -> nopStage () - Injective inj -> tryFDEqns fam_tc work_args work_item $ - mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs + Injective inj -> do { eqns <- mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs + ; tryFDEqns fam_tc work_args work_item eqns } - ; if hasRelevantGiven eqs_for_me work_args work_item - then nopStage () - else tryFDEqns fam_tc work_args work_item $ - mkTopFamEqFDs fam_tc work_args work_rhs } + ; unless (hasRelevantGiven eqs_for_me work_args work_item) $ + do { eqns <- mkTopFamEqFDs fam_tc work_args work_item + ; tryFDEqns fam_tc work_args work_item eqns } } -mkTopFamEqFDs :: TyCon -> [TcType] -> Xi -> TcS [FunDepEqns] -mkTopFamEqFDs fam_tc work_args work_rhs +mkTopFamEqFDs :: TyCon -> [TcType] -> EqCt -> SolverStage [FunDepEqns] +mkTopFamEqFDs fam_tc work_args work_item | isOpenTypeFamilyTyCon fam_tc , Injective inj_flags <- tyConInjectivityInfo fam_tc = -- Open, injective type families - mkTopOpenFamEqFDs fam_tc inj_flags work_args work_rhs + simpleStage (mkTopOpenFamEqFDs fam_tc inj_flags work_args work_item) | Just ax <- isClosedFamilyTyCon_maybe fam_tc = -- Closed type families - mkTopClosedFamEqFDs ax work_args work_rhs + mkTopClosedFamEqFDs ax work_args work_item | otherwise = -- Data families, abstract families, @@ -537,13 +537,13 @@ mkTopFamEqFDs fam_tc work_args work_rhs -- closed type families with no equations (isClosedFamilyTyCon_maybe returns Nothing) return [] -tryFDEqns :: TyCon -> [TcType] -> EqCt -> TcS [FunDepEqns] -> SolverStage () -tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eqns +tryFDEqns :: TyCon -> [TcType] -> EqCt -> [FunDepEqns] -> SolverStage () +tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) fd_eqns = Stage $ - do { fd_eqns <- mk_fd_eqns - ; traceTcS "tryFDEqns" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr work_args + do { traceTcS "tryFDEqns" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr work_args , text "rhs:" <+> ppr rhs , text "eqns:" <+> ppr fd_eqns ]) + ; (insoluble, unif_happened) <- solveFunDeps ev fd_eqns ; if | unif_happened -> startAgainWith (CEqCan work_item) @@ -553,17 +553,19 @@ tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eq ----------------------------------------- -- User-defined type families ----------------------------------------- -mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> Xi -> TcS [FunDepEqns] +mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunDepEqns] -- Look at the top-level axioms; we effectively infer injectivity, -- so we don't need tyConInjectivtyInfo. This works fine for closed -- type families without injectivity info -- See Note [Exploiting closed type families] -mkTopClosedFamEqFDs ax work_args work_rhs - = do { let branches = fromBranches (coAxiomBranches ax) +mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs }) + = Stage $ + do { let branches = fromBranches (coAxiomBranches ax) ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs) ; case getRelevantBranches ax work_args work_rhs of - [eqn] -> return [eqn] -- If there is just one relevant equation, use it - _ -> return [] } + [] -> insolubleFunDep ev + [eqn] -> continueWith [eqn] -- If there is just one relevant equation, use it + _ -> continueWith [] } hasRelevantGiven :: [EqCt] -> [TcType] -> EqCt -> Bool -- A Given is relevant if it is not apart from the Wanted @@ -606,9 +608,9 @@ getRelevantBranches ax work_args work_rhs no_match lhs_tys (CoAxBranch { cab_lhs = lhs_tys1 }) = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys) -mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> Xi -> TcS [FunDepEqns] +mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns] -- Implements (INJFAM:Wanted/top) -mkTopOpenFamEqFDs fam_tc inj_flags work_args work_rhs +mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) = do { fam_envs <- getFamInstEnvs ; let branches :: [CoAxBranch] branches = concatMap (fromBranches . coAxiomBranches . fi_axiom) $ @@ -629,7 +631,7 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args work_rhs | otherwise = Nothing -mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> TcS [FunDepEqns] +mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> SolverStage [FunDepEqns] mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs = do { let -- eqns_from_inerts: see (INJFAM:Wanted/other) eqns_from_inerts = mapMaybe do_one eqs_for_me @@ -723,13 +725,13 @@ tryGivenBuiltinFamEqFDs eqs_for_me fam_tc ops work_args do_one _ = return () -mkTopBuiltinFamEqFDs :: TyCon -> BuiltInSynFamily -> [TcType] -> Xi -> TcS [FunDepEqns] +mkTopBuiltinFamEqFDs :: TyCon -> BuiltInSynFamily -> [TcType] -> Xi -> SolverStage [FunDepEqns] mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs = return [FDEqns { fd_qtvs = [] , fd_eqs = map snd $ tryInteractTopFam ops fam_tc work_args work_rhs }] mkLocalBuiltinFamEqFDs :: [EqCt] -> TyCon -> BuiltInSynFamily - -> [TcType] -> Xi -> TcS [FunDepEqns] + -> [TcType] -> Xi -> SolverStage [FunDepEqns] mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs = do { let do_one :: EqCt -> [FunDepEqns] do_one (EqCt { eq_lhs = TyFamLHS _ inert_args, eq_rhs = inert_rhs }) ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -1050,6 +1050,10 @@ Here are the KickOut Criteria: * (KK3b) If the role of `fs` is Representational: kick out if `rhs_s` is of form `(lhs_w t1 .. tn)` + * (KK4: completeness) Kick out if + * lhs_s = F lhs_tys, and + * lhs_w is rewritable (anywhere) in rhs_s + Rationale * (KK0) kick out only if `fw` can rewrite `fs`. @@ -1063,6 +1067,13 @@ Rationale * (KK3) see Note [KK3: completeness of solving] +* (KK4) is about completeness. If we have + Inert: F alpha ~ beta + Work: beta ~ Int + and F is closed or injective, then we want to kick out the inert item, in + case we get injectivity information from `F alpha ~ Int` that allows us to + solve it. + The above story is a bit vague wrt roles, but the code is not. See Note [Flavours with roles] @@ -1187,7 +1198,7 @@ Wrinkles: by the inert item. And too much kick-out is positively harmful. (Historical example #14363.) -* (KK3b) addresses teh main example above for KK3. Another way to understand +* (KK3b) addresses the main example above for KK3. Another way to understand (KK3b) is that we treat an inert item a -f-> b in the same way as @@ -1732,6 +1743,12 @@ kickOutRewritableLHS ko_spec new_fr@(_, new_role) -- The above check redundantly checks the role & flavour, -- but it's very convenient + -- (KK4) + | TyFamLHS tc _ <- lhs + , famTyConHasInjectivity tc + , fr_can_rewrite_ty LookEverywhere eq_rel rhs_ty + = True + -- (KK2) | let where_to_look | fs_can_rewrite_fr = LookOnlyUnderFamApps | otherwise = LookEverywhere ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -479,6 +479,7 @@ kickOutRewritable ko_spec new_fr n_kicked = lengthBag kicked_out ; setInertCans ics' + ; traceTcS "kickOutRewritable" (ppr ko_spec $$ ppr new_fr $$ ppr kicked_out) ; unless (isEmptyBag kicked_out) $ do { emitWork kicked_out ===================================== testsuite/tests/typecheck/should_fail/T15767.stderr ===================================== @@ -1,6 +1,6 @@ T15767.hs:7:5: error: [GHC-39999] - • No instance for ‘C () b0’ arising from a use of ‘x’ + • No instance for ‘C () b’ arising from a use of ‘x’ • In the expression: x In an equation for ‘y’: y = x View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6b8505139ac30818c949722c390617f7... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6b8505139ac30818c949722c390617f7... You're receiving this email because of your account on gitlab.haskell.org.