[Git][ghc/ghc][wip/9.4.6-backports] 3 commits: Show an error when we cannot default a concrete tyvar

Zubin (@wz1000) gitlab at gitlab.haskell.org
Fri Aug 4 11:45:41 UTC 2023



Zubin pushed to branch wip/9.4.6-backports at Glasgow Haskell Compiler / GHC


Commits:
689a3ad2 by Krzysztof Gogolewski at 2023-08-04T17:08:55+05:30
Show an error when we cannot default a concrete tyvar

Fixes #23153

(cherry picked from commit 0da18eb79540181ae9835e73d52ba47ec79fff6b)
(cherry picked from commit ca34a7c79a8855d08e491814db9d656b00a8fe3e)

- - - - -
734ad762 by sheaf at 2023-08-04T17:08:55+05:30
Handle ConcreteTvs in inferResultToType

This patch fixes two issues.

  1. 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.

  2. startSolvingByUnification can make some type variables concrete.
     However, it didn't return an updated type, so callers of this
     function, if they don't zonk, might miss this and accidentally
     perform a double update of a metavariable.

     We now return the updated type from this function, which avoids
     this issue.

Fixes #23154

(cherry picked from commit 9ab9b30ec1affe22b188f9a6637ac3bdea75bdba)

- - - - -
dc2e9d2d by Krzysztof Gogolewski at 2023-08-04T17:09:34+05:30
Use tcInferFRR to prevent bad generalisation

Fixes #23176

(cherry picked from commit 4b89bb54a1d1d6a7b30a6bbfd21eed5d85506813)

- - - - -


20 changed files:

- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Tc/Utils/Zonk.hs
- testsuite/tests/polykinds/T22743.stderr
- testsuite/tests/rep-poly/RepPolyPatBind.stderr
- + testsuite/tests/rep-poly/T23153.hs
- + testsuite/tests/rep-poly/T23153.stderr
- + testsuite/tests/rep-poly/T23154.hs
- + testsuite/tests/rep-poly/T23154.stderr
- + testsuite/tests/rep-poly/T23176.hs
- + testsuite/tests/rep-poly/T23176.stderr
- testsuite/tests/rep-poly/all.T
- testsuite/tests/typecheck/should_fail/VtaFail.stderr


Changes:

=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -799,6 +799,11 @@ instance Diagnostic TcRnMessage where
     TcRnInvalidCIdentifier target
       -> mkSimpleDecorated $
            sep [quotes (ppr target) <+> text "is not a valid C identifier"]
+    TcRnCannotDefaultConcrete frr
+      -> mkSimpleDecorated $
+         ppr (frr_context frr) $$
+         text "cannot be assigned a fixed runtime representation," <+>
+         text "not even by defaulting."
 
   diagnosticReason = \case
     TcRnUnknownMessage m
@@ -1059,6 +1064,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnInvalidCIdentifier{}
       -> ErrorWithoutFlag
+    TcRnCannotDefaultConcrete{}
+      -> ErrorWithoutFlag
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -1318,6 +1325,9 @@ instance Diagnostic TcRnMessage where
            _ -> noHints
     TcRnInvalidCIdentifier{}
       -> noHints
+    TcRnCannotDefaultConcrete{}
+      -> [SuggestAddTypeSignatures UnnamedBinding]
+
 
 deriveInstanceErrReasonHints :: Class
                              -> UsingGeneralizedNewtypeDeriving


=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -1790,6 +1790,16 @@ data TcRnMessage where
   -}
   TcRnInvalidCIdentifier :: !CLabelString -> TcRnMessage
 
+  {- TcRnCannotDefaultConcrete is an error occurring when a concrete
+    type variable cannot be defaulted.
+
+    Test cases:
+      T23153
+  -}
+  TcRnCannotDefaultConcrete
+    :: !FixedRuntimeRepOrigin
+    -> TcRnMessage
+
 -- | Specifies which backend code generators where expected for an FFI declaration
 data ExpectedBackends
   = COrAsmOrLlvm         -- ^ C, Asm, or LLVM


=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -1095,6 +1095,22 @@ Examples that might fail:
                                 or multi-parameter type classes
  - an inferred type that includes unboxed tuples
 
+Note [Inferred type with escaping kind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Check for an inferred type with an escaping kind; e.g. #23051
+   forall {k} {f :: k -> RuntimeRep} {g :: k} {a :: TYPE (f g)}. a
+where the kind of the body of the forall mentions `f` and `g` which
+are bound by the forall.  No no no.
+
+This check, mkInferredPolyId, is really in the wrong place:
+`inferred_poly_ty` doesn't obey the PKTI and it would be better not to
+generalise it in the first place; see #20686.  But for now it works.
+
+I considered adjusting the generalisation in GHC.Tc.Solver to directly check for
+escaping kind variables; instead, promoting or defaulting them. But that
+gets into the defaulting swamp and is a non-trivial and unforced
+change, so I have left it alone for now.
+
 Note [Impedance matching]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
@@ -1184,7 +1200,9 @@ tcMonoBinds is_rec sig_fn no_gen
   , Nothing <- sig_fn name   -- ...with no type signature
   = setSrcSpanA b_loc    $
     do  { ((co_fn, matches'), rhs_ty')
-            <- tcInfer $ \ exp_ty ->
+            <- tcInferFRR (FRRBinder name) $ \ exp_ty ->
+                          -- tcInferFRR: the type of a let-binder must have
+                          -- a fixed runtime rep. See #23176
                        tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
                           -- We extend the error context even for a non-recursive
                           -- function so that in type error messages we show the
@@ -1206,7 +1224,9 @@ tcMonoBinds is_rec sig_fn no_gen
   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
   , all (isNothing . sig_fn) bndrs
   = addErrCtxt (patMonoBindsCtxt pat grhss) $
-    do { (grhss', pat_ty) <- tcInfer $ \ exp_ty ->
+    do { (grhss', pat_ty) <- tcInferFRR FRRPatBind $ \ exp_ty ->
+                          -- tcInferFRR: the type of each let-binder must have
+                          -- a fixed runtime rep. See #23176
                              tcGRHSsPat grhss exp_ty
 
        ; let exp_pat_ty :: Scaled ExpSigmaTypeFRR


=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -583,7 +583,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


=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2303,7 +2303,7 @@ canEqTyVarFunEq :: CtEvidence               -- :: lhs ~ (rhs |> mco)
                 -> MCoercion                -- :: kind(rhs) ~N kind(lhs)
                 -> TcS (StopOrContinue Ct)
 canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
-  = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv1 rhs
+  = do { (is_touchable, rhs) <- touchabilityTest (ctEvFlavour ev) tv1 rhs
        ; if | case is_touchable of { Untouchable -> False; _ -> True }
             , cterHasNoProblem $
                 checkTyVarEq tv1 rhs `cterRemoveProblem` cteTypeFamily


=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -1563,7 +1563,7 @@ tryToSolveByUnification :: Ct -> CtEvidence
                         -> TcType    -- RHS
                         -> TcS (StopOrContinue Ct)
 tryToSolveByUnification work_item ev tv rhs
-  = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv rhs
+  = do { (is_touchable, rhs) <- touchabilityTest (ctEvFlavour ev) tv rhs
        ; traceTcS "tryToSolveByUnification" (vcat [ ppr tv <+> char '~' <+> ppr rhs
                                                   , ppr is_touchable ])
 


=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1250,35 +1250,37 @@ instance Outputable TouchabilityTestResult where
   ppr (TouchableOuterLevel tvs lvl) = text "TouchableOuterLevel" <> parens (ppr lvl <+> ppr tvs)
   ppr Untouchable                   = text "Untouchable"
 
-touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS TouchabilityTestResult
--- This is the key test for untouchability:
+touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS (TouchabilityTestResult, TcType)
+-- ^ This is the key test for untouchability:
 -- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
 -- and Note [Solve by unification] in GHC.Tc.Solver.Interact
+--
+-- Returns a new rhs type, as this function can turn make some metavariables concrete.
 touchabilityTest flav tv1 rhs
   | flav /= Given  -- See Note [Do not unify Givens]
   , MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1
-  = do { can_continue_solving <- wrapTcS $ startSolvingByUnification info rhs
-       ; if not can_continue_solving
-         then return Untouchable
-         else
-    do { ambient_lvl  <- getTcLevel
+  = do { continue_solving <- wrapTcS $ startSolvingByUnification info rhs
+       ; case continue_solving of
+       { Nothing -> return (Untouchable, rhs)
+       ; Just rhs ->
+    do { let (free_metas, free_skols) = partition isPromotableMetaTyVar $
+                                        nonDetEltsUniqSet               $
+                                        tyCoVarsOfType rhs
+       ; ambient_lvl  <- getTcLevel
        ; given_eq_lvl <- getInnermostGivenEqLevel
 
        ; if | tv_lvl `sameDepthAs` ambient_lvl
-            -> return TouchableSameLevel
+            -> return (TouchableSameLevel, rhs)
 
             | tv_lvl `deeperThanOrSame` given_eq_lvl   -- No intervening given equalities
             , all (does_not_escape tv_lvl) free_skols  -- No skolem escapes
-            -> return (TouchableOuterLevel free_metas tv_lvl)
+            -> return (TouchableOuterLevel free_metas tv_lvl, rhs)
 
             | otherwise
-            -> return Untouchable } }
+            -> return (Untouchable, rhs) } } }
   | otherwise
-  = return Untouchable
+  = return (Untouchable, rhs)
   where
-     (free_metas, free_skols) = partition isPromotableMetaTyVar $
-                                nonDetEltsUniqSet               $
-                                tyCoVarsOfType rhs
 
      does_not_escape tv_lvl fv
        | isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv
@@ -1919,23 +1921,21 @@ breakTyEqCycle_maybe ev cte_result lhs rhs
      -- See Detail (8) of the Note.
 
   = do { should_break <- final_check
-       ; if should_break then do { redn <- go rhs
-                                 ; return (Just redn) }
-                         else return Nothing }
+       ; mapM go should_break }
   where
     flavour = ctEvFlavour ev
     eq_rel  = ctEvEqRel ev
 
     final_check = case flavour of
-      Given  -> return True
+      Given  -> return $ Just rhs
       Wanted    -- Wanteds work only with a touchable tyvar on the left
                 -- See "Wanted" section of the Note.
         | TyVarLHS lhs_tv <- lhs ->
-          do { result <- touchabilityTest Wanted lhs_tv rhs
+          do { (result, rhs) <- touchabilityTest Wanted lhs_tv rhs
              ; return $ case result of
-                          Untouchable -> False
-                          _           -> True }
-        | otherwise -> return False
+                          Untouchable -> Nothing
+                          _           -> Just rhs }
+        | otherwise -> return Nothing
 
     -- This could be considerably more efficient. See Detail (5) of Note.
     go :: TcType -> TcS ReductionN


=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1,5 +1,6 @@
 
 {-# LANGUAGE MultiWayIf      #-}
+{-# LANGUAGE RecursiveDo     #-}
 {-# LANGUAGE TupleSections   #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -501,7 +502,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
@@ -557,20 +567,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  <- newConcreteTyVarAtLevel conc_orig tc_lvl runtimeRepTy
+                      ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr)
+                      ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr
+                      ; return tau }
 
 {- Note [inferResultToType]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -893,6 +911,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) $
@@ -938,7 +963,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
@@ -956,7 +981,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
@@ -1123,6 +1148,13 @@ newMetaTyVarTyAtLevel tc_lvl kind
         ; name    <- newMetaTyVarName (fsLit "p")
         ; return (mkTyVarTy (mkTcTyVar name kind details)) }
 
+newConcreteTyVarAtLevel :: ConcreteTvOrigin -> TcLevel -> TcKind -> TcM TcType
+newConcreteTyVarAtLevel conc_orig tc_lvl kind
+  = do  { details <- newConcreteTvDetailsAtLevel conc_orig tc_lvl
+        ; name    <- newMetaTyVarName (fsLit "c")
+        ; return (mkTyVarTy (mkTcTyVar name kind details)) }
+
+
 {- *********************************************************************
 *                                                                      *
           Finding variables to quantify over
@@ -1826,6 +1858,17 @@ defaultTyVar def_strat tv
        ; writeMetaTyVar tv manyDataConTy
        ; return True }
 
+  | isConcreteTyVar tv
+    -- We don't want to quantify; but neither can we default to
+    -- anything sensible.  (If it has kind RuntimeRep or Levity, as is
+    -- often the case, it'll have been caught earlier by earlier
+    -- cases. So in this exotic situation we just promote.  Not very
+    -- satisfing, but it's very much a corner case: #23051)
+    -- We should really implement the plan in #20686.
+  = do { lvl <- getTcLevel
+       ; _ <- promoteMetaTyVarTo lvl tv
+       ; return True }
+
   | DefaultKindVars <- def_strat -- -XNoPolyKinds and this is a kind var: we must default it
   = default_kind_var tv
 
@@ -2240,7 +2283,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
@@ -2258,7 +2301,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)  $


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2055,10 +2055,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
            -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
       , cterHasNoProblem (checkTyVarEq tv1 ty2)
            -- See Note [Prevent unification with type families]
-      = do { can_continue_solving <- startSolvingByUnification (metaTyVarInfo tv1) ty2
-           ; if not can_continue_solving
-             then not_ok_so_defer
-             else
+      = do { mb_continue_solving <- startSolvingByUnification (metaTyVarInfo tv1) ty2
+           ; case mb_continue_solving of
+           { Nothing -> not_ok_so_defer
+           ; Just ty2 ->
         do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1)
            ; traceTc "uUnfilledVar2 ok" $
              vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
@@ -2072,9 +2072,9 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
              then do { writeMetaTyVar tv1 ty2
                      ; return (mkTcNomReflCo ty2) }
 
-             else defer }} -- This cannot be solved now.  See GHC.Tc.Solver.Canonical
-                           -- Note [Equalities with incompatible kinds] for how
-                           -- this will be dealt with in the solver
+             else defer }}} -- This cannot be solved now.  See GHC.Tc.Solver.Canonical
+                            -- Note [Equalities with incompatible kinds] for how
+                            -- this will be dealt with in the solver
 
       | otherwise
       = not_ok_so_defer
@@ -2094,39 +2094,38 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
 -- | Checks (TYVAR-TV), (COERCION-HOLE) and (CONCRETE) of
 -- Note [Unification preconditions]; returns True if these conditions
 -- are satisfied. But see the Note for other preconditions, too.
-startSolvingByUnification :: MetaInfo -> TcType  -- zonked
-                          -> TcM Bool
+startSolvingByUnification :: MetaInfo -> TcType -- zonked
+                          -> TcM (Maybe TcType)
 startSolvingByUnification _ xi
   | hasCoercionHoleTy xi  -- (COERCION-HOLE) check
-  = return False
+  = return Nothing
 startSolvingByUnification info xi
   = case info of
-      CycleBreakerTv -> return False
+      CycleBreakerTv -> return Nothing
       ConcreteTv conc_orig ->
-        do { (_, not_conc_reasons) <- makeTypeConcrete conc_orig xi
+        do { (xi, not_conc_reasons) <- makeTypeConcrete conc_orig xi
                  -- NB: makeTypeConcrete has the side-effect of turning
                  -- some TauTvs into ConcreteTvs, e.g.
                  -- alpha[conc] ~# TYPE (TupleRep '[ beta[tau], IntRep ])
                  -- will write `beta[tau] := beta[conc]`.
                  --
-                 -- We don't need to track these unifications for the purposes
-                 -- of constraint solving (e.g. updating tcs_unified or tcs_unif_lvl),
-                 -- as they don't unlock any further progress.
+                 -- We return the new type, so that callers of this function
+                 -- aren't required to zonk.
            ; case not_conc_reasons of
-               [] -> return True
-               _  -> return False }
+               [] -> return $ Just xi
+               _  -> return Nothing }
       TyVarTv ->
         case tcGetTyVar_maybe xi of
-           Nothing -> return False
+           Nothing -> return Nothing
            Just tv ->
              case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle
-                SkolemTv {} -> return True
-                RuntimeUnk  -> return True
+                SkolemTv {} -> return $ Just xi
+                RuntimeUnk  -> return $ Just xi
                 MetaTv { mtv_info = info } ->
                   case info of
-                    TyVarTv -> return True
-                    _       -> return False
-      _ -> return True
+                    TyVarTv -> return $ Just xi
+                    _       -> return Nothing
+      _ -> return $ Just xi
 
 swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
 swapOverTyVars is_given tv1 tv2


=====================================
compiler/GHC/Tc/Utils/Zonk.hs
=====================================
@@ -56,6 +56,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Tc.Utils.TcMType
 import GHC.Tc.Utils.Env   ( tcLookupGlobalOnly )
 import GHC.Tc.Types.Evidence
+import GHC.Tc.Errors.Types
 
 import GHC.Core.TyCo.Ppr ( pprTyVar )
 import GHC.Core.TyCon
@@ -1771,7 +1772,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
@@ -1844,6 +1845,9 @@ commitFlexi flexi tv zonked_kind
         | isMultiplicityTy zonked_kind
         -> do { traceTc "Defaulting flexi tyvar to Many:" (pprTyVar tv)
               ; return manyDataConTy }
+        | Just (ConcreteFRR origin) <- isConcreteTyVar_maybe tv
+        -> do { addErr $ TcRnCannotDefaultConcrete origin
+              ; return (anyTypeOfKind zonked_kind) }
         | otherwise
         -> do { traceTc "Defaulting flexi tyvar to Any:" (pprTyVar tv)
               ; return (anyTypeOfKind zonked_kind) }


=====================================
testsuite/tests/polykinds/T22743.stderr
=====================================
@@ -1,7 +1,10 @@
 
 T22743.hs:10:1: error:
-    • Quantified type's kind mentions quantified type variable
-        type: ‘forall {f :: * -> RuntimeRep} {g} {a :: TYPE (f g)}. a’
-      where the body of the forall has this kind: ‘TYPE (f g)’
-    • When checking the inferred type
-        x :: forall {f :: * -> RuntimeRep} {g} {a :: TYPE (f g)}. a
+    The binder ‘x’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T22743.hs:10:1: error:
+    The binder ‘x’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.


=====================================
testsuite/tests/rep-poly/RepPolyPatBind.stderr
=====================================
@@ -17,3 +17,36 @@ RepPolyPatBind.hs:18:5: error:
                 x, y :: a
                 (# x, y #) = undefined
               in x
+
+RepPolyPatBind.hs:18:8: error: [GHC-55287]
+    • The pattern binding does not have a fixed runtime representation.
+      Its type is:
+        (# a0, b0 #) :: TYPE (TupleRep [k00, k10])
+      Cannot unify ‘rep’ with the type variable ‘k00’
+      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:11: error: [GHC-55287]
+    • The pattern binding does not have a fixed runtime representation.
+      Its type is:
+        (# a0, b0 #) :: TYPE (TupleRep [k00, k10])
+      Cannot unify ‘rep’ with the type variable ‘k10’
+      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
+        x :: a (bound at RepPolyPatBind.hs:18:8)
+        foo :: () -> a (bound at RepPolyPatBind.hs:15:1)


=====================================
testsuite/tests/rep-poly/T23153.hs
=====================================
@@ -0,0 +1,8 @@
+module T23153 where
+
+import GHC.Exts
+
+f :: forall r s (a :: TYPE (r s)). a -> ()
+f = f
+
+g h = f (h ())


=====================================
testsuite/tests/rep-poly/T23153.stderr
=====================================
@@ -0,0 +1,15 @@
+
+T23153.hs:8:1: error:
+    The argument ‘(h ())’ of ‘f’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T23153.hs:8:1: error:
+    The argument ‘(h ())’ of ‘f’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T23153.hs:8:1: error:
+    The argument ‘(h ())’ of ‘f’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.


=====================================
testsuite/tests/rep-poly/T23154.hs
=====================================
@@ -0,0 +1,7 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+
+module T23154 where
+
+import GHC.Exts
+
+f x = x :: (_ :: (TYPE (_ _)))


=====================================
testsuite/tests/rep-poly/T23154.stderr
=====================================
@@ -0,0 +1,15 @@
+
+T23154.hs:7:1: error:
+    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:
+    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:
+    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.


=====================================
testsuite/tests/rep-poly/T23176.hs
=====================================
@@ -0,0 +1,6 @@
+module T23176 where
+
+import GHC.Exts
+
+f = outOfScope :: (_ :: TYPE (r s))
+(g :: _) = outOfScope :: (_ :: TYPE (r s))


=====================================
testsuite/tests/rep-poly/T23176.stderr
=====================================
@@ -0,0 +1,30 @@
+
+T23176.hs:5:1: error:
+    The binder ‘f’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T23176.hs:5:1: error:
+    The binder ‘f’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T23176.hs:5:1: error:
+    The binder ‘f’
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T23176.hs:6:1: error:
+    The pattern binding
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T23176.hs:6:1: error:
+    The pattern binding
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.
+
+T23176.hs:6:1: error:
+    The pattern binding
+    cannot be assigned a fixed runtime representation, not even by defaulting.
+    Suggested fix: Add a type signature.


=====================================
testsuite/tests/rep-poly/all.T
=====================================
@@ -111,3 +111,6 @@ test('T20363b', normal, compile_fail, [''])                         ##
 test('RepPolyCase2', normal, compile_fail, [''])                    ##
 test('RepPolyRule3', normal, compile_fail, [''])                    ##
 ######################################################################
+test('T23153', normal, compile_fail, [''])
+test('T23154', normal, compile_fail, [''])
+test('T23176', normal, compile_fail, ['-XPartialTypeSignatures -fdefer-out-of-scope-variables'])


=====================================
testsuite/tests/typecheck/should_fail/VtaFail.stderr
=====================================
@@ -6,8 +6,8 @@ VtaFail.hs:7:16: error:
       In an equation for ‘answer_nosig’:
           answer_nosig = pairup_nosig @Int @Bool 5 True
 
-VtaFail.hs:14:17: error:
-    • Cannot apply expression of type ‘p1 -> p1’
+VtaFail.hs:14:17: error: [GHC-95781]
+    • 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’:



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/30fed8fabdd2833c754834e3b4131f2277dcc650...dc2e9d2d977b9e9555339086a84ee3f1511baa82

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/30fed8fabdd2833c754834e3b4131f2277dcc650...dc2e9d2d977b9e9555339086a84ee3f1511baa82
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230804/ae33117b/attachment-0001.html>


More information about the ghc-commits mailing list