Should we use CheckTyEqResult for equalities involving concrete metavariables?
It might be worthwhile to add new CheckTyEqProblem
s for equalities involving concrete metavariables.
- Insoluble, e.g.
alpha[conc] ~# a[sk]
- Potentially soluble, e.g.
alpha[conc] ~# F beta[tau]
for a type familyF
(the type family could reduce after unifying beta) oralpha[conc] ~# (ty |> {co})
for a coercion hole{co}
(the coercion hole could be filled with a reflexive coercion).
Unfortunately this isn't a perfect fit because the use-sites need slightly different information:
- When reporting an error involving a concrete metavariable in
GHC.Tc.Errors.myTyVarEErr'
, we need the fullConcreteTvOrigin
which contains information about why we required the type variable to be concrete (e.g. a representation-polymorphism check), not just whether there was a problem. (Compare with the impredicativity check inmkTyVarEqErr'
.) - In
simplifyTopWanteds
, we decide whether to do defaulting depending on whether there are insolubles (call toinsolubleWC
callinginsolubleEqCt
callingisInsolubleReason
callingcterIsInsoluble
). However, we should NOT default the concrete type variablealpha
inalpha[conc] ~# F beta[tau]
because that will lead to very confusing error messages that we couldn't unifyF beta
withLifted
when instead we want a representation-polymorphism error.
So for the moment I don't see the benefit in doing this, but perhaps once we revisit the defaulting story (#20686) things will be different.