Note [Coercion errors in tcSubMult]
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
- The Concrete mechanism GHC.Tc.Utils.Concrete
Referenced by 6
- GHC.Tc.Types.Constraint call site ×2
- No deferring for multiplicity errors GHC.Tc.Errors
- GHC.Tc.Errors call site
- GHC.Tc.Utils.Monad call site
- GHC.Tc.Utils.Unify call site