GitLab

The solver maintains a structure EqualCtList, with this Note:

Note [EqualCtList invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    * All are equalities
    * All these equalities have the same LHS
    * The list is never empty
    * No element of the list can rewrite any other
    * Derived before Wanted

From the fourth invariant it follows that the list is
   - A single [G], or
   - Zero or one [D] or [WD], followed by any number of [W]

The Wanteds can't rewrite anything which is why we put them last

Yet this isn't quite accurate. If we have a [G] a ~R Bool and a [D] a ~ Int, neither can rewrite the other. Both can live in the EqualCtList quite peacefully. Thus, the "it follows that" is wrong. Worse, the rewriter contains the code

       ; case lookupDVarEnv ieqs tv of
           Just (EqualCtList (ct :| _))   -- If the first doesn't work,
                                          -- the subsequent ones won't either
             | CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv
                      , cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } <- ct

but the comment there isn't true: the first might not work, but maybe a later one will.

I tried quite hard to come up with some misbehavior that this misunderstanding caused, but it's quite hard. An example with a Given that contains a touchable metavariable wouldn't be convincing (#18929 (closed)), and all other examples seem to lead to program rejection. And because the prioritization of some errors over others, it's hard to see the bad error.

Yet I still think there is a problem here, and that we should search through the list looking for a valid inert.