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.

2 files changed, 49 insertions, 11 deletions

diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 2e535338e6..84eea92b01 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1722,21 +1722,44 @@ pprTcSolverReportMsg ctxt
     maybe_num_args_msg = num_args_msg `orElse` empty
 
     count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
-pprTcSolverReportMsg _ (FixedRuntimeRepError origs_and_tys) =
-  let
+pprTcSolverReportMsg _ (FixedRuntimeRepError frr_infos) =
+  vcat (map make_msg frr_infos) $$ mustBeRefl_msg
+  where
     -- Assemble the error message: pair up each origin with the corresponding type, e.g.
     --   • FixedRuntimeRep origin msg 1 ...
     --       a :: TYPE r1
     --   • FixedRuntimeRep origin msg 2 ...
     --       b :: TYPE r2
-    combine_origin_ty :: FRROrigin -> Type -> SDoc
-    combine_origin_ty frr_orig ty =
-      -- Add bullet points if there is more than one error.
-      (if length origs_and_tys > 1 then (bullet <+>) else id) $
-        vcat [pprFRROrigin frr_orig <> colon
-             ,nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE (typeKind ty)]
-  in
-    vcat $ map (uncurry combine_origin_ty) origs_and_tys
+    make_msg :: FixedRuntimeRepErrorInfo -> SDoc
+    make_msg
+      (FixedRuntimeRepErrorInfo
+        { frrInfo_origin = frr_orig
+        , frrInfo_type   = ty })
+      =
+        -- Add bullet points if there is more than one error.
+        (if length frr_infos > 1 then (bullet <+>) else id) $
+          vcat [ sep [ pprFRROrigin frr_orig
+                     , text "does not have a fixed runtime representation." ]
+               , text "Its type is:"
+               , nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE (typeKind ty) ]
+
+    -- In PHASE 1 of FixedRuntimeRep, we don't allow rewriting in hasFixedRuntimeRep,
+    -- so we add a special message to explain this to the user.
+    --
+    -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.
+    give_mustBeRefl_msg :: Bool
+    give_mustBeRefl_msg = all frrInfo_isReflPrim frr_infos
+
+    mustBeRefl_msg :: SDoc
+    mustBeRefl_msg
+      | give_mustBeRefl_msg
+      = vcat
+         [ text "NB: GHC does not (yet) support rewriting in runtime representations."
+         , text "Please comment on GHC ticket #13105 if this is causing you trouble."
+         , text "<https://gitlab.haskell.org/ghc/ghc/-/issues/13105>" ]
+      | otherwise
+      = empty
+
 pprTcSolverReportMsg _ (SkolemEscape item implic esc_skols) =
   let
     esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index d6004c7b96..ca835a4ae9 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -46,6 +46,7 @@ module GHC.Tc.Errors.Types (
   , SolverReportErrCtxt(..)
   , getUserGivens, discardProvCtxtGivens
   , TcSolverReportMsg(..), TcSolverReportInfo(..)
+  , FixedRuntimeRepErrorInfo(..)
   , CND_Extra(..)
   , mkTcReportWithInfo
   , FitsMbSuppressed(..)
@@ -2239,7 +2240,7 @@ data TcSolverReportMsg
    -- i.e. an unsolved `Concrete# ty` constraint.
    --
    -- See 'FRROrigin' for more information.
-  | FixedRuntimeRepError [(FRROrigin, Type)]
+  | FixedRuntimeRepError [FixedRuntimeRepErrorInfo]
 
   -- | A skolem type variable escapes its scope.
   --
@@ -2346,6 +2347,20 @@ data TcSolverReportMsg
     , unsafeOverlap_matches :: [ClsInst]
     , unsafeOverlapped      :: [ClsInst] }
 
+-- | Stores the information we have when performing a
+-- representation-polymorphism check.
+data FixedRuntimeRepErrorInfo
+  = FixedRuntimeRepErrorInfo
+    { frrInfo_origin     :: !FRROrigin
+        -- ^ Context for the representation-polymorphism check.
+    , frrInfo_type       :: !Type
+       -- ^ The type which we are insisting must have a fixed runtime representation.
+    , frrInfo_isReflPrim :: !Bool }
+        -- ^ Was this check due to 'IsRefl#', i.e. it's a PHASE 1 check?
+        --
+        -- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.
+
+
 -- | Additional information to be given in a 'CouldNotDeduce' message,
 -- which is then passed on to 'mk_supplementary_ea_msg'.
 data CND_Extra = CND_Extra TypeOrKind Type Type