Use ConcreteTv for metavariables that must only be unified with concrete types

Currently, when we have a constraint of the form Concrete# ty, we have a separate evidence term in the form of a coercion hole {co} :: ty #~ concrete_tv, for some metavariable concrete_tv. This metavariable really belongs to this Concrete# constraint, and should not be unified with anything else. This isn't a problem in PHASE 1 of the FixedRuntimeRep plan outlined on the wiki, because the metavariable concrete_tv never leaks out. However, once we start actually using the evidence for these constraints, we will insert casts into the typechecked program and suddenly it becomes possible for some other part of the typechecker to unify this metavariable. If we end up unifying with a non-concrete type (e.g. a type family application), then the whole exercise will have been for nought.

The plan to address this is to introduce a special kind of metavariable that can only be unified with concrete types, by adding a new field to MetaInfo, say ConcreteTv.

Using ConcreteTv instead of Concrete# constraints

@simonpj then points out that, once we do this, then perhaps we no longer need the Concrete# special predicate at all, and could instead work directly with ConcreteTv metavariables. I've started thinking about this, here are a few observations:

Phase 2 for free?

Using ConcreteTv directly allows us to re-use GHC's existing infrastructure for inserting casts in some circumstances, instead of manually having to insert them as described in the FixedRuntimeRep wiki page.

For example:

f x = ... g x ...

g :: forall (a :: TYPE (F Int)). a -> ...

type family F a where
  F Int = LiftedRep

When typechecking f, if we can set things up to have x :: ty :: TYPE conc_tv for conc_tv one of these ConcreteTv metavariables, then we've in very good shape. Indeed, then we will refuse to unify conc_tv := F Int because F Int is not concrete, but we will rewrite conc_tv ~# F_Int to conc_tv ~# LiftedRep and will unify conc_tv := LiftedRep. Then the rest of the machinery in tcApp will insert the necessary casts for the application g x.

The problem, as far as I see it, is that this optimistically assumes that the relevant metavariables are assigned ConcreteTv at birth. In this particular case I think we're OK: the first thing we see is x in a binding position but we otherwise know nothing about x, so it stands to reason that we can conjure up a ConcreteTv metavariable for its kind and go from there.

However, now that I look at where the existing hasFixedRuntimeRep checks take place, we might well instead come across a type first (and do some unification), and only later come across a situation which requires concreteness (e.g. it appears as the kind of a bound variable).
It seems plausible to me that we could end up in a situation where we have x :: ty :: alpha for a normal unification variable alpha, then we unify alpha ~ F Int, and then later on we come across e.g. x used in an application, realising too late "oh shoot, we should have made alpha a ConcreteTv!".

Error messages

Currently, metavariables don't store any origin information. If we want to report informative representation-polymorphism error messages, we should add some origin information so that if we end up with an unfilled ConcreteTv metavariable we can report an appropriate error message.

Re-using ~#

It seems like we might benefit from re-using primitive equality. In particular, decomposition of Concrete# constraints is quite similar to decomposition for ~#, so it seems to make sense.
When we come across a type ty that we must ensure is concrete, we create a new ConcreteTv metavariable conc_tv and directly emit ty ~# conc_tv. We can attach a CtOrigin just as before, so we still have the error messages.
This would avoid a fair bit of special casing, as currently Concrete# is unique in the fact that the predicate Concrete# a does not match the type of its evidence a ~ concrete_tv.