Incorrect documentation around EqualCtList
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.