GitLab

Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC

Commits:

0fe38b69

by Simon Peyton Jones at 2025-10-17T13:38:17+01:00

Improve equality checking for foralls a bit

...by re-using the TcEvBindsVar

25c7f66e
by Simon Peyton Jones at 2025-10-17T14:57:35+01:00
```
Comments on rewriter sets
```

3 changed files:

compiler/GHC/Tc/Solver/Equality.hs
compiler/GHC/Tc/Types/Constraint.hs
compiler/GHC/Tc/Types/Evidence.hs

Changes:

compiler/GHC/Tc/Solver/Equality.hs

@@ -554,24 +554,21 @@ can_eq_nc_forall ev eq_rel s1 s2
                     ; traceTcS "Trying to solve the implication" (ppr s1 $$ ppr s2 $$ ppr wanteds)
                     -- Solve the `wanteds` in a nested context
 -                   ; ev_binds_var <- newNoTcEvBinds
 +                   -- Use the /same/ TcEvBinds var as the context; we do not expect any dict binds
 +                   -- but we do want to record any used Given coercions (in `evb_tcvs`) so that
 +                   -- they are kept alive by `neededEvVars`. Admittedly they are free in `all_co`,
 +                   -- but only if we zonk it, which `neededEvVars` does not do (see test T7196).
 +                   ; ev_binds_var <- getTcEvBindsVar
                     ; residual_wanted <- nestImplicTcS skol_info_anon ev_binds_var tclvl $
                                          solveSimpleWanteds wanteds
                     ; return (all_co, isSolvedWC residual_wanted) }
+-
        -- Kick out any inerts constraints that mention unified type variables
        ; kickOutAfterUnification unifs
        ; if solved
 -        then do { all_co <- zonkCo all_co
 -                     -- setWantedEq will add `all_co` to the `ebv_tcvs`, to record
 -                     -- that `all_co` is used.  But if `all_co` contains filled
 -                     -- CoercionHoles, from the nested solve, and we may miss the
 -                     -- use of CoVars.  Test T7196 showed this up
+-
 -                ; setWantedEq orig_dest emptyCoHoleSet all_co
 +        then do { setWantedEq orig_dest emptyCoHoleSet all_co
                       -- emptyCoHoleSet: fully solved, so all_co has no holes
                  ; stopWith ev "Polytype equality: solved" }

compiler/GHC/Tc/Types/Constraint.hs

@@ -2568,42 +2568,41 @@ Note [Wanteds rewrite Wanteds]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Should one Wanted constraint be allowed to rewrite another?
 -This example (along with #8450) suggests not:
 -   f :: a -> Bool
 -   f x = ( [x,'c'], [x,True] ) `seq` True
 -Here we get
 -  [W] a ~ Char
 -  [W] a ~ Bool
 -but we do not want to complain about Bool ~ Char!
+-
 -This example suggests yes (indexed-types/should_fail/T4093a):
 -  type family Foo a
 -  f :: (Foo e ~ Maybe e) => Foo e
 -In the ambiguity check, we get
 -  [G] g1 :: Foo e ~ Maybe e
 -  [W] w1 :: Foo alpha ~ Foo e
 -  [W] w2 :: Foo alpha ~ Maybe alpha
 -w1 gets rewritten by the Given to become
 -  [W] w3 :: Foo alpha ~ Maybe e
 -Now, the only way to make progress is to allow Wanteds to rewrite Wanteds.
 -Rewriting w3 with w2 gives us
 -  [W] w4 :: Maybe alpha ~ Maybe e
 -which will soon get us to alpha := e and thence to victory.
+-
 -TL;DR we want equality saturation.
 +This example (along with #8450) suggests "no":
 +       f :: a -> Bool
 +       f x = ( [x,'c'], [x,True] ) `seq` True
 +    Here we get
 +      [W] a ~ Char
 +      [W] a ~ Bool
 +    but we do not want to complain about Bool ~ Char!
++
 +This example suggests "yes" (indexed-types/should_fail/T4093a):
 +      type family Foo a
 +      f :: (Foo e ~ Maybe e) => Foo e
 +    In the ambiguity check, we get
 +      [G] g1 :: Foo e ~ Maybe e
 +      [W] w1 :: Foo alpha ~ Foo e
 +      [W] w2 :: Foo alpha ~ Maybe alpha
 +    w1 gets rewritten by the Given to become
 +      [W] w3 :: Foo alpha ~ Maybe e
 +    Now, the only way to make progress is to allow Wanteds to rewrite Wanteds.
 +    Rewriting w3 with w2 gives us
 +      [W] w4 :: Maybe alpha ~ Maybe e
 +    which will soon get us to alpha := e and thence to victory.
 +    TL;DR we want equality saturation.
  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:
 -(WRW1) The rewriters of a Wanted.  We do allow Wanteds to rewrite Wanteds, but each
 -  unsolved Wanted tracks
 +(WRW1) ctev_rewriters: the rewriters of a Wanted.  We /do/ allow Wanteds to
 +  rewrite Wanteds, but each unsolved Wanted tracks
       the set of Wanteds that it has been rewritten by
    in its CoHoleSet, stored in the `ctev_rewriters` field of the CtWanted
    constructor of CtEvidence.  (Only Wanteds have CoHoleSets.)
 -  If the rewriter set is empty, then the constaint has been not been rewritten
 -  by any unsolved constraint.
 +  Key point: if the rewriter set is empty, then the constaint has been not been
 +  rewritten by any unsolved constraint.
  (WRW2) A CoHoleSet is just a set of CoercionHoles. This is sufficient because only
    equalities (evidenced by coercion holes) are used for rewriting; other

compiler/GHC/Tc/Types/Evidence.hs

@@ -392,6 +392,8 @@ data EvBindsVar
        --  so that we can report unused given constraints,
        --  in GHC.Tc.Solver.neededEvVars
        -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
 +      -- Also: we garbage-collect unused bindings in `neededEvVars`,
 +      --       so this matters for correctness too.
+     }
    | CoEvBindsVar {  -- See Note [Coercion evidence only]