GitLab

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

 +{-# 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, [''])