Note [Coercion errors in tcSubMult]

GHC/Tc/Utils/Unify.hs:1595 compiler 2 tickets

At the moment, we insist that all sub-multiplicity tests turn out
(once the typechecker has finished its work) to be equalities,
i.e. implementable by ReflCo.  Why?  Because our type system has
no way to express non-Refl sub-multiplicities.

How can we check that every call to `tcSubMult` returns `Refl`?
It might not be `Refl` *yet*.

[TODO: add counterexample #25130]

So we take the following approach

* In `tcEqMult`:
  - Emit a perfectly ordinary Wanted equality constraint for the equality,
    returning a coercion.

  - Wrap that coercion with `DE_Multiplicity` to make a `DelayedError`, and put
    that delayed error into `wc_errors` of the current WantedConstraints.  This
    is done by `ensureReflMultiplicityCo`.

* When solving constraints, discard any `DE_Multiplicity` errors that wrap a
  reflective coercion, of kind `ty ~ ty`.  This is done in
  `GHC.Tc.Solver.simplifyDelayedErrors`

* After constraint solving is complete report an error if there are any
  remaining `DE_Multiplicity` errors.  See
  `GHC.Tc.Errors.reportMultiplicityCoercionErrs`

Wrinkles

(DME1) If the multiplicity constraint is /solved/, but with a non-reflective
   coercion, we'll have just a `DE_Multiplicity` error left over.

   But if the multiplicity constraint is /unsolved/ (e.g. ManyTy ~ OneTy), we
   will have /both/ an unsolved Wanted in `wc_simple`, /and/ a `DE_Multiplicity`
   in `wc_errors`.  We don't want to report both.  Solution: suppress all
   `DE_Multiplicity` constraints if there are any unsolved wanted.

   This way, the delayed error is indeed only reported when the constraint is
   solved with a non-reflexivity coercion.

An alternative would be to have a kind of constraint which can only produce
trivial evidence. This would allow such checks to happen in the constraint
solver (#18756).  This would be similar to the existing setup for Concrete, see
Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete (PHASE 1 in particular).

References 1

Referenced by 6