Handle ConcreteTvs in inferResultToTypewip/T23153

inferResultToType was discarding the ir_frr information, which meant
some metavariables ended up being MetaTvs instead of ConcreteTvs.

This function now creates new ConcreteTvs as necessary, instead of
always creating MetaTvs.

Fixes #23154

13 files changed, 90 insertions, 34 deletions

diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 6e58e6b033..a8d7c30846 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -3473,7 +3473,7 @@ data TcRnMessage where
                        -> ![LIdP GhcRn] -- ^ The LHS args
                        -> !PatSynInvalidRhsReason -- ^ The number of equation arguments
                        -> TcRnMessage
-  {- TcRnCannotDefaultConcrete is an error occurring when a concrete
+  {-| TcRnCannotDefaultConcrete is an error occurring when a concrete
     type variable cannot be defaulted.
 
     Test cases:
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index d5721ff5e1..a5ad2f1733 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -883,7 +883,7 @@ tcExprWithSig expr hs_ty
     loc = getLocA (dropWildCards hs_ty)
     ctxt = ExprSigCtxt (lhsSigWcTypeContextSpan hs_ty)
 
-tcExprSig :: UserTypeCtxt -> LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType)
+tcExprSig :: UserTypeCtxt -> LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcSigmaType)
 tcExprSig ctxt expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
   = setSrcSpan loc $   -- Sets the location for the implication constraint
     do { let poly_ty = idType poly_id
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index f3d0097f93..49699d865d 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -2119,14 +2119,17 @@ checkTouchableTyVarEq ev lhs_tv rhs
            ; if not (cterHasNoProblem reason)  -- Failed to promote free vars
              then failCheckWith reason
              else
-        do { let tv_info | isConcreteInfo lhs_tv_info = lhs_tv_info
-                         | otherwise                  = TauTv
-                -- Make a concrete tyvar if lhs_tv is concrete
-                -- e.g.  alpha[2,conc] ~ Maybe (F beta[4])
-                --       We want to flatten to
-                --       alpha[2,conc] ~ Maybe gamma[2,conc]
-                --       gamma[2,conc] ~ F beta[4]
-           ; new_tv_ty <- TcM.newMetaTyVarTyWithInfo lhs_tv_lvl tv_info fam_app_kind
+        do { new_tv_ty <-
+              case lhs_tv_info of
+                ConcreteTv conc_info ->
+                  -- Make a concrete tyvar if lhs_tv is concrete
+                  -- e.g.  alpha[2,conc] ~ Maybe (F beta[4])
+                  --       We want to flatten to
+                  --       alpha[2,conc] ~ Maybe gamma[2,conc]
+                  --       gamma[2,conc] ~ F beta[4]
+                  TcM.newConcreteTyVarTyAtLevel conc_info lhs_tv_lvl fam_app_kind
+                _ -> TcM.newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind
+
            ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty
            ; hole <- TcM.newCoercionHole pty
            ; let new_ev = CtWanted { ctev_pred      = pty
diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs
index fe0f261005..a07401ec74 100644
--- a/compiler/GHC/Tc/Utils/Concrete.hs
+++ b/compiler/GHC/Tc/Utils/Concrete.hs
@@ -8,9 +8,6 @@ module GHC.Tc.Utils.Concrete
   ( -- * Ensuring that a type has a fixed runtime representation
     hasFixedRuntimeRep
   , hasFixedRuntimeRep_syntactic
-
-    -- * Making a type concrete
-  , makeTypeConcrete
   )
  where
 
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index b4971210fd..873ff2979a 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE MultiWayIf      #-}
+{-# LANGUAGE RecursiveDo     #-}
 {-# LANGUAGE TupleSections   #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -24,7 +25,7 @@ module GHC.Tc.Utils.TcMType (
   newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind,
   newOpenBoxedTypeKind,
   newMetaKindVar, newMetaKindVars,
-  newMetaTyVarTyAtLevel, newMetaTyVarTyWithInfo,
+  newMetaTyVarTyAtLevel, newConcreteTyVarTyAtLevel,
   newAnonMetaTyVar, newConcreteTyVar,
   cloneMetaTyVar, cloneMetaTyVarWithInfo,
   newCycleBreakerTyVar,
@@ -482,7 +483,16 @@ newInferExpType :: TcM ExpType
 newInferExpType = new_inferExpType Nothing
 
 newInferExpTypeFRR :: FixedRuntimeRepContext -> TcM ExpTypeFRR
-newInferExpTypeFRR frr_orig = new_inferExpType (Just frr_orig)
+newInferExpTypeFRR frr_orig
+  = do { th_stage <- getStage
+       ; if
+          -- See [Wrinkle: Typed Template Haskell]
+          -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete.
+          | Brack _ (TcPending {}) <- th_stage
+          -> new_inferExpType Nothing
+
+          | otherwise
+          -> new_inferExpType (Just frr_orig) }
 
 new_inferExpType :: Maybe FixedRuntimeRepContext -> TcM ExpType
 new_inferExpType mb_frr_orig
@@ -538,20 +548,28 @@ expTypeToType (Infer inf_res) = inferResultToType inf_res
 
 inferResultToType :: InferResult -> TcM Type
 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
-                      , ir_ref = ref })
+                      , ir_ref = ref
+                      , ir_frr = mb_frr })
   = do { mb_inferred_ty <- readTcRef ref
        ; tau <- case mb_inferred_ty of
             Just ty -> do { ensureMonoType ty
                             -- See Note [inferResultToType]
                           ; return ty }
-            Nothing -> do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
-                          ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr)
-                            -- See Note [TcLevel of ExpType]
+            Nothing -> do { tau <- new_meta
                           ; writeMutVar ref (Just tau)
                           ; return tau }
        ; traceTc "Forcing ExpType to be monomorphic:"
                  (ppr u <+> text ":=" <+> ppr tau)
        ; return tau }
+  where
+    -- See Note [TcLevel of ExpType]
+    new_meta = case mb_frr of
+      Nothing  ->  do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
+                      ; newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr) }
+      Just frr -> mdo { rr  <- newConcreteTyVarTyAtLevel conc_orig tc_lvl runtimeRepTy
+                      ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr)
+                      ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr
+                      ; return tau }
 
 {- Note [inferResultToType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -874,6 +892,13 @@ newTauTvDetailsAtLevel tclvl
                         , mtv_ref   = ref
                         , mtv_tclvl = tclvl }) }
 
+newConcreteTvDetailsAtLevel :: ConcreteTvOrigin -> TcLevel -> TcM TcTyVarDetails
+newConcreteTvDetailsAtLevel conc_orig tclvl
+  = do { ref <- newMutVar Flexi
+       ; return (MetaTv { mtv_info  = ConcreteTv conc_orig
+                        , mtv_ref   = ref
+                        , mtv_tclvl = tclvl }) }
+
 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
 cloneMetaTyVar tv
   = assert (isTcTyVar tv) $
@@ -931,7 +956,7 @@ isUnfilledMetaTyVar tv
 
 --------------------
 -- Works with both type and kind variables
-writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
+writeMetaTyVar :: HasDebugCallStack => TcTyVar -> TcType -> TcM ()
 -- Write into a currently-empty MetaTyVar
 
 writeMetaTyVar tyvar ty
@@ -949,7 +974,7 @@ writeMetaTyVar tyvar ty
   = massertPpr False (text "Writing to non-meta tyvar" <+> ppr tyvar)
 
 --------------------
-writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
+writeMetaTyVarRef :: HasDebugCallStack => TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
 -- Here the tyvar is for error checking only;
 -- the ref cell must be for the same tyvar
 writeMetaTyVarRef tyvar ref ty
@@ -1114,13 +1139,10 @@ newMetaTyVarTyAtLevel tc_lvl kind
         ; name    <- newMetaTyVarName (fsLit "p")
         ; return (mkTyVarTy (mkTcTyVar name kind details)) }
 
-newMetaTyVarTyWithInfo :: TcLevel -> MetaInfo -> TcKind -> TcM TcType
-newMetaTyVarTyWithInfo tc_lvl info kind
-  = do { ref <- newMutVar Flexi
-       ; let details = MetaTv { mtv_info  = info
-                              , mtv_ref   = ref
-                              , mtv_tclvl = tc_lvl }
-        ; name <- newMetaTyVarName (fsLit "p")
+newConcreteTyVarTyAtLevel :: ConcreteTvOrigin -> TcLevel -> TcKind -> TcM TcType
+newConcreteTyVarTyAtLevel conc_orig tc_lvl kind
+  = do  { details <- newConcreteTvDetailsAtLevel conc_orig tc_lvl
+        ; name    <- newMetaTyVarName (fsLit "c")
         ; return (mkTyVarTy (mkTcTyVar name kind details)) }
 
 {- *********************************************************************
@@ -2258,7 +2280,7 @@ a \/\a in the final result but all the occurrences of a will be zonked to ()
 *                                                                      *
 ********************************************************************* -}
 
-promoteMetaTyVarTo :: TcLevel -> TcTyVar -> TcM Bool
+promoteMetaTyVarTo :: HasDebugCallStack => TcLevel -> TcTyVar -> TcM Bool
 -- When we float a constraint out of an implication we must restore
 -- invariant (WantedInv) in Note [TcLevel invariants] in GHC.Tc.Utils.TcType
 -- Return True <=> we did some promotion
@@ -2276,7 +2298,7 @@ promoteMetaTyVarTo tclvl tv
    = return False
 
 -- Returns whether or not *any* tyvar is defaulted
-promoteTyVarSet :: TcTyVarSet -> TcM Bool
+promoteTyVarSet :: HasDebugCallStack => TcTyVarSet -> TcM Bool
 promoteTyVarSet tvs
   = do { tclvl <- getTcLevel
        ; bools <- mapM (promoteMetaTyVarTo tclvl)  $
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index 7a2c0de793..aa2ffa8bae 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -1738,7 +1738,7 @@ change.  But in some cases it makes a HUGE difference: see test
 T9198 and #19668.  So yes, it seems worth it.
 -}
 
-zonkTyVarOcc :: ZonkEnv -> TcTyVar -> TcM Type
+zonkTyVarOcc :: HasDebugCallStack => ZonkEnv -> TcTyVar -> TcM Type
 zonkTyVarOcc env@(ZonkEnv { ze_flexi = flexi
                           , ze_tv_env = tv_env
                           , ze_meta_tv_env = mtv_env_ref }) tv
diff --git a/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
index a9643f4b73..b85e0be15e 100644
--- a/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
+++ b/testsuite/tests/rep-poly/RepPolyInferPatBind.stderr
@@ -8,7 +8,7 @@ RepPolyInferPatBind.hs:21:2: error: [GHC-55287]
     • The pattern binding does not have a fixed runtime representation.
       Its type is:
         T :: TYPE R
-      Cannot unify ‘R’ with the type variable ‘p0’
+      Cannot unify ‘R’ with the type variable ‘c0’
       because it is not a concrete ‘RuntimeRep’.
     • When checking that the pattern signature: T
         fits the type of its context: T
diff --git a/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
index 4515832b21..a0eb6a6916 100644
--- a/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
+++ b/testsuite/tests/rep-poly/RepPolyInferPatSyn.stderr
@@ -4,7 +4,7 @@ RepPolyInferPatSyn.hs:22:16: error: [GHC-55287]
       does not have a fixed runtime representation.
       Its type is:
         T :: TYPE R
-      Cannot unify ‘R’ with the type variable ‘p0’
+      Cannot unify ‘R’ with the type variable ‘c0’
       because it is not a concrete ‘RuntimeRep’.
     • When checking that the pattern signature: T
         fits the type of its context: T
diff --git a/testsuite/tests/rep-poly/RepPolyPatBind.stderr b/testsuite/tests/rep-poly/RepPolyPatBind.stderr
index 40637215fe..fca59b9777 100644
--- a/testsuite/tests/rep-poly/RepPolyPatBind.stderr
+++ b/testsuite/tests/rep-poly/RepPolyPatBind.stderr
@@ -1,5 +1,21 @@
 
 RepPolyPatBind.hs:18:5: error: [GHC-55287]
+    • The pattern binding does not have a fixed runtime representation.
+      Its type is:
+        p0 :: TYPE c0
+      Cannot unify ‘TupleRep [rep, rep]’ with the type variable ‘c0’
+      because it is not a concrete ‘RuntimeRep’.
+    • In the pattern: (# x, y #)
+      In a pattern binding: (# x, y #) = undefined
+      In the expression:
+        let
+          x, y :: a
+          (# x, y #) = undefined
+        in x
+    • Relevant bindings include
+        foo :: () -> a (bound at RepPolyPatBind.hs:15:1)
+
+RepPolyPatBind.hs:18:5: error: [GHC-55287]
     • • The binder ‘y’ does not have a fixed runtime representation.
         Its type is:
           a :: TYPE rep
diff --git a/testsuite/tests/rep-poly/T23154.hs b/testsuite/tests/rep-poly/T23154.hs
new file mode 100644
index 0000000000..b0048e441f
--- /dev/null
+++ b/testsuite/tests/rep-poly/T23154.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+
+module T23154 where
+
+import GHC.Exts
+
+f x = x :: (_ :: (TYPE (_ _)))
diff --git a/testsuite/tests/rep-poly/T23154.stderr b/testsuite/tests/rep-poly/T23154.stderr
new file mode 100644
index 0000000000..46d416a0d0
--- /dev/null
+++ b/testsuite/tests/rep-poly/T23154.stderr
@@ -0,0 +1,10 @@
+
+T23154.hs:7:1: error: [GHC-52083]
+    The first pattern in the equation for ‘f’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T23154.hs:7:1: error: [GHC-52083]
+    The first pattern in the equation for ‘f’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
diff --git a/testsuite/tests/rep-poly/all.T b/testsuite/tests/rep-poly/all.T
index a05a6bb7e5..0be5b954af 100644
--- a/testsuite/tests/rep-poly/all.T
+++ b/testsuite/tests/rep-poly/all.T
@@ -117,3 +117,4 @@ test('T21650_b', normal, compile_fail, ['-Wno-deprecated-flags'])            ##
 
 test('T23051', normal, compile_fail, [''])
 test('T23153', normal, compile_fail, [''])
+test('T23154', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
index 4d01d8b8bb..925189c0fc 100644
--- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr
@@ -7,7 +7,7 @@ VtaFail.hs:7:16: error: [GHC-95781]
           answer_nosig = pairup_nosig @Int @Bool 5 True
 
 VtaFail.hs:14:17: error: [GHC-95781]
-    • Cannot apply expression of type ‘p1 -> p1’
+    • Cannot apply expression of type ‘p0 -> p0’
       to a visible type argument ‘Int’
     • In the expression: (\ x -> x) @Int 12
       In an equation for ‘answer_lambda’: