Introduce ConcreteTv metavariables

  This patch introduces a new kind of metavariable, by adding the
  constructor `ConcreteTv` to `MetaInfo`. A metavariable with
  `ConcreteTv` `MetaInfo`, henceforth a concrete metavariable, can only
  be unified with a type that is concrete (that is, a type that answers
  `True` to `GHC.Core.Type.isConcrete`).

  This solves the problem of dangling metavariables in `Concrete#`
  constraints: instead of emitting `Concrete# ty`, which contains a
  secret existential metavariable, we simply emit a primitive equality
  constraint `ty ~# concrete_tv` where `concrete_tv` is a fresh concrete
  metavariable.

  This means we can avoid all the complexity of canonicalising
  `Concrete#` constraints, as we can just re-use the existing machinery
  for `~#`.

  To finish things up, this patch then removes the `Concrete#` special
  predicate, and instead introduces the special predicate `IsRefl#`
  which enforces that a coercion is reflexive.
  Such a constraint is needed because the canonicaliser is quite happy
  to rewrite an equality constraint such as `ty ~# concrete_tv`, but
  such a rewriting is not handled by the rest of the compiler currently,
  as we need to make use of the resulting coercion, as outlined in the
  FixedRuntimeRep plan.

  The big upside of this approach (on top of simplifying the code)
  is that we can now selectively implement PHASE 2 of FixedRuntimeRep,
  by changing individual calls of `hasFixedRuntimeRep_MustBeRefl` to
  `hasFixedRuntimeRep` and making use of the obtained coercion.

1 files changed, 8 insertions, 5 deletions

diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index b753a3c902..75a117798e 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -429,7 +429,9 @@ interactWithInertsStage wi
              CEqCan       {} -> interactEq      ics wi
              CIrredCan    {} -> interactIrred   ics wi
              CDictCan     {} -> interactDict    ics wi
-             CSpecialCan  {} -> continueWith wi -- cannot have Special Givens, so nothing to interact with
+             CSpecialCan { cc_special_pred = spec } ->
+               case spec of
+                 IsReflPrimPred {} -> continueWith wi -- cannot have IsRefl# Givens, so nothing to interact with
              _ -> pprPanic "interactWithInerts" (ppr wi) }
                 -- CNonCanonical have been canonicalised
 
@@ -1891,13 +1893,14 @@ topReactionsStage work_item
            CEqCan {} ->
              doTopReactEq work_item
 
-           CSpecialCan {} ->
-             -- No top-level interactions for special constraints.
-             continueWith work_item
-
            CIrredCan {} ->
              doTopReactOther work_item
 
+           CSpecialCan { cc_special_pred = spec } ->
+             case spec of
+               IsReflPrimPred {} -> continueWith work_item
+               -- No top-level interactions for IsRefl# constraints.
+
            -- Any other work item does not react with any top-level equations
            _  -> continueWith work_item }