GitLab

It might be worthwhile to add new CheckTyEqProblems for equalities involving concrete metavariables.

• Insoluble, e.g. alpha[conc] ~# a[sk]
• Potentially soluble, e.g. alpha[conc] ~# F beta[tau] for a type family F (the type family could reduce after unifying beta) or alpha[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:

1. When reporting an error involving a concrete metavariable in GHC.Tc.Errors.myTyVarEErr', we need the full ConcreteTvOrigin 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 in mkTyVarEqErr'.)
2. In simplifyTopWanteds, we decide whether to do defaulting depending on whether there are insolubles (call to insolubleWC calling insolubleEqCt calling isInsolubleReason calling cterIsInsoluble). However, we should NOT default the concrete type variable alpha in alpha[conc] ~# F beta[tau] because that will lead to very confusing error messages that we couldn't unify F beta with Lifted 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.