Simon Peyton Jones pushed to branch wip/T26582 at Glasgow Haskell Compiler / GHC Commits: 5851a7c1 by Simon Peyton Jones at 2025-11-17T10:26:20+00:00 Fix a bug in defaulting Addresses #26582 Defaulting was doing some unification but then failing to iterate. Silly. I discovered that the main solver was unnecessarily iterating even if there was a unification for an /outer/ unification variable, so I fixed that too. - - - - - 6 changed files: - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Utils/TcType.hs - + testsuite/tests/typecheck/should_compile/T26582.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -395,9 +395,11 @@ tryConstraintDefaulting wc | isEmptyWC wc = return wc | otherwise - = do { (unif_happened, better_wc) <- reportCoarseGrainUnifications $ - go_wc False wc - -- We may have done unifications; so solve again + = do { (outermost_unif_lvl, better_wc) <- reportCoarseGrainUnifications $ + go_wc False wc + + -- We may have done unifications; if so, solve again + ; let unif_happened = not (isInfiniteTcLevel outermost_unif_lvl) ; solveAgainIf unif_happened better_wc } where go_wc :: Bool -> WantedConstraints -> TcS WantedConstraints @@ -414,14 +416,17 @@ tryConstraintDefaulting wc else return (Just ct) } go_implic :: Bool -> Implication -> TcS Implication - go_implic encl_eqs implic@(Implic { ic_status = status, ic_wanted = wanteds - , ic_given_eqs = given_eqs, ic_binds = binds }) + go_implic encl_eqs implic@(Implic { ic_tclvl = tclvl + , ic_status = status, ic_wanted = wanteds + , ic_given_eqs = given_eqs, ic_binds = binds }) | isSolvedStatus status = return implic -- Nothing to solve inside here | otherwise = do { let encl_eqs' = encl_eqs || given_eqs /= NoGivenEqs - ; wanteds' <- setEvBindsTcS binds $ + ; wanteds' <- setTcLevelTcS tclvl $ + -- Set the levels so that reportCoareseGrainUnifications works + setEvBindsTcS binds $ -- defaultCallStack sets a binding, so -- we must set the correct binding group go_wc encl_eqs' wanteds @@ -660,7 +665,9 @@ Wrinkles: f x = case x of T1 -> True Should we infer f :: T a -> Bool, or f :: T a -> a. Both are valid, but - neither is more general than the other. + neither is more general than the other. But by the time defaulting takes + place all let-bound variables have got their final types; defaulting won't + affect let-generalisation. (DE2) We still can't unify if there is a skolem-escape check, or an occurs check, or it it'd mean unifying a TyVarTv with a non-tyvar. It's only the ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -1877,18 +1877,18 @@ reportFineGrainUnifications (TcS thing_inside) ; recordUnifications outer_wu unif_tvs ; return (unif_tvs, res) } -reportCoarseGrainUnifications :: TcS a -> TcS (Bool, a) +reportCoarseGrainUnifications :: TcS a -> TcS (TcLevel, a) -- Record whether any useful unifications are done by thing_inside +-- Specifically: return the TcLevel of the outermost (smallest level) +-- unification variable that has been unified, or infiniteTcLevel if none -- Remember to propagate the information to the enclosing context reportCoarseGrainUnifications (TcS thing_inside) = TcS $ \ env@(TcSEnv { tcs_what = outer_what }) -> case outer_what of - WU_None - -> do { (unif_happened, _, res) <- report_coarse_grain_unifs env thing_inside - ; return (unif_happened, res) } + WU_None -> report_coarse_grain_unifs env thing_inside WU_Coarse outer_ul_ref - -> do { (unif_happened, inner_ul, res) <- report_coarse_grain_unifs env thing_inside + -> do { (inner_ul, res) <- report_coarse_grain_unifs env thing_inside -- Propagate to outer_ul_ref ; outer_ul <- TcM.readTcRef outer_ul_ref @@ -1897,31 +1897,32 @@ reportCoarseGrainUnifications (TcS thing_inside) ; TcM.traceTc "reportCoarse(Coarse)" $ vcat [ text "outer_ul" <+> ppr outer_ul - , text "inner_ul" <+> ppr inner_ul - , text "unif_happened" <+> ppr unif_happened ] - ; return (unif_happened, res) } + , text "inner_ul" <+> ppr inner_ul] + ; return (inner_ul, res) } WU_Fine outer_tvs_ref -> do { (unif_tvs,res) <- report_fine_grain_unifs env thing_inside - ; let unif_happened = not (isEmptyVarSet unif_tvs) - ; when unif_happened $ - TcM.updTcRef outer_tvs_ref (`unionVarSet` unif_tvs) + + -- Propagate to outer_tvs_rev + ; TcM.updTcRef outer_tvs_ref (`unionVarSet` unif_tvs) + + ; let outermost_unif_lvl = minTcTyVarSetLevel unif_tvs ; TcM.traceTc "reportCoarse(Fine)" $ vcat [ text "unif_tvs" <+> ppr unif_tvs - , text "unif_happened" <+> ppr unif_happened ] - ; return (unif_happened, res) } + , text "unif_happened" <+> ppr outermost_unif_lvl ] + ; return (outermost_unif_lvl, res) } report_coarse_grain_unifs :: TcSEnv -> (TcSEnv -> TcM a) - -> TcM (Bool, TcLevel, a) --- Returns (unif_happened, coarse_inner_ul, res) + -> TcM (TcLevel, a) +-- Returns the level number of the outermost +-- unification variable that is unified report_coarse_grain_unifs env thing_inside = do { inner_ul_ref <- TcM.newTcRef infiniteTcLevel ; res <- thing_inside (env { tcs_what = WU_Coarse inner_ul_ref }) - ; inner_ul <- TcM.readTcRef inner_ul_ref - ; ambient_lvl <- TcM.getTcLevel - ; let unif_happened = ambient_lvl `deeperThanOrSame` inner_ul - ; return (unif_happened, inner_ul, res) } - + ; inner_ul <- TcM.readTcRef inner_ul_ref + ; TcM.traceTc "report_coarse" $ + text "inner_lvl =" <+> ppr inner_ul + ; return (inner_ul, res) } report_fine_grain_unifs :: TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcTyVarSet, a) ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -118,28 +118,34 @@ simplify_loop n limit definitely_redo_implications , int (lengthBag simples) <+> text "simples to solve" ]) ; traceTcS "simplify_loop: wc =" (ppr wc) - ; (simple_unif_happened, wc1) + ; ambient_lvl <- getTcLevel + ; (simple_unif_lvl, wc1) <- reportCoarseGrainUnifications $ -- See Note [Superclass iteration] solveSimpleWanteds simples -- Any insoluble constraints are in 'simples' and so get rewritten -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet -- Next, solve implications from wc_impl - ; (impl_unif_happened, implics') + ; let simple_unif_happened = ambient_lvl `deeperThanOrSame` simple_unif_lvl + ; (implic_unif_lvl, implics') <- if not (definitely_redo_implications -- See Note [Superclass iteration] || simple_unif_happened) -- for this conditional - then return (False, implics) + then return (infiniteTcLevel, implics) else reportCoarseGrainUnifications $ solveNestedImplications implics ; let wc' = wc1 { wc_impl = wc_impl wc1 `unionBags` implics' } - ; csTraceTcS $ text "unif_happened" <+> ppr impl_unif_happened - -- We iterate the loop only if the /implications/ did some relevant - -- unification. Even if the /simples/ did unifications we don't need - -- to re-do them. - ; maybe_simplify_again (n+1) limit impl_unif_happened wc' } + -- unification, hence looking only at `implic_unif_lvl`. (Even if the + -- /simples/ did unifications we don't need to re-do them.) + -- Also note that we only iterate if `implic_unify_lvl` is /equal to/ + -- the current level; if it is less , we'll iterate some outer level, + -- which will bring us back here anyway. + -- See Note [When to iterate the solver: unifications] + ; let implic_unif_happened = implic_unif_lvl `sameDepthAs` ambient_lvl + ; csTraceTcS $ text "implic_unif_happened" <+> ppr implic_unif_happened + ; maybe_simplify_again (n+1) limit implic_unif_happened wc' } data NextAction = NA_Stop -- Just return the WantedConstraints @@ -148,7 +154,9 @@ data NextAction Bool -- See `definitely_redo_implications` in the comment -- for `simplify_loop` -maybe_simplify_again :: Int -> IntWithInf -> Bool +maybe_simplify_again :: Int -> IntWithInf + -> Bool -- True <=> Solving the implications did some unifications + -- at the current level; so iterate -> WantedConstraints -> TcS WantedConstraints maybe_simplify_again n limit unif_happened wc@(WC { wc_simple = simples }) = do { -- Look for reasons to stop or continue @@ -222,10 +230,10 @@ and if so it seems a pity to waste time iterating the implications (forall b. bl (If we add new Given superclasses it's a different matter: it's really worth looking at the implications.) -Hence the definitely_redo_implications flag to simplify_loop. It's usually -True, but False in the case where the only reason to iterate is new Wanted -superclasses. In that case we check whether the new Wanteds actually led to -any new unifications, and iterate the implications only if so. +Hence the `definitely_redo_implications` flag to `simplify_loop`. It's usually True, +but False in the case where the only reason to iterate is new Wanted superclasses. +In that case we check whether the new Wanteds actually led to any new unifications +(at all), and iterate the implications only if so. Note [When to iterate the solver: unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -45,7 +45,7 @@ module GHC.Tc.Utils.TcType ( TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, strictlyDeeperThan, deeperThanOrSame, sameDepthAs, tcTypeLevel, tcTyVarLevel, maxTcLevel, minTcLevel, - infiniteTcLevel, + infiniteTcLevel, isInfiniteTcLevel, -------------------------------- -- MetaDetails @@ -879,6 +879,10 @@ isTopTcLevel :: TcLevel -> Bool isTopTcLevel (TcLevel 0) = True isTopTcLevel _ = False +isInfiniteTcLevel :: TcLevel -> Bool +isInfiniteTcLevel QLInstVar = True +isInfiniteTcLevel _ = False + pushTcLevel :: TcLevel -> TcLevel -- See Note [TcLevel assignment] pushTcLevel (TcLevel us) = TcLevel (us + 1) ===================================== testsuite/tests/typecheck/should_compile/T26582.hs ===================================== @@ -0,0 +1,35 @@ +{-# LANGUAGE GADTs #-} + +module T26582 where + +sametype :: a -> a -> Int +sametype = sametype + +f :: Eq a => (a->Int) -> Int +f = f + +data T b where T1 :: T Bool + +g1 :: T b -> Int +g1 v = f (\x -> case v of { T1 -> sametype x True }) + +g2 :: Eq c => c -> T b -> Int +g2 c v = f (\x -> case v of { T1 -> sametype x c }) + +{- The point is that we get something like + + Wanted: [W] d : Eq alpha[1] + Implication + level: 2 + Given: b~Bool + + Wanted: [W] alpha[1]~Bool -- For g1 + Wanted: [W] alpha[1]~c -- For g2 + +So alpha is untouchable under the (b~Bool) from the GADT. +And yet in the end it's easy to solve +via alpha:=Bool, or alpha:=c resp + +But having done that defaulting we must then remember to +solved that `d : Eq alpha`! We forgot to so so in #26582. +-} ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -956,3 +956,4 @@ test('T26457', normal, compile, ['']) test('T17705', normal, compile, ['']) test('T14745', normal, compile, ['']) test('T26451', normal, compile, ['']) +test('T26582', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5851a7c1ecf9473ad7f8a9ccb9c894fb... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5851a7c1ecf9473ad7f8a9ccb9c894fb... You're receiving this email because of your account on gitlab.haskell.org.