diff options
27 files changed, 272 insertions, 195 deletions
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index c957fc7fcd..1e9a25c63d 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -903,15 +903,19 @@ mkInferredPolyId residual insoluble qtvs inferred_theta poly_name mb_sig_inst mo ; let inferred_poly_ty = mkInvisForAllTys binders (mkPhiTy theta' mono_ty') ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta' - , ppr inferred_poly_ty]) + , ppr inferred_poly_ty + , text "insoluble" <+> ppr insoluble ]) + ; unless insoluble $ addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $ do { checkEscapingKind inferred_poly_ty + -- See Note [Inferred type with escaping kind] ; checkValidType (InfSigCtxt poly_name) inferred_poly_ty } - -- See Note [Validity of inferred types] - -- If we found an insoluble error in the function definition, don't - -- do this check; otherwise (#14000) we may report an ambiguity - -- error for a rather bogus type. + -- See Note [Validity of inferred types] + -- unless insoluble: if we found an insoluble error in the + -- function definition, don't do this check; otherwise + -- (#14000) we may report an ambiguity error for a rather + -- bogus type. ; return (mkLocalId poly_name ManyTy inferred_poly_ty) } @@ -1176,6 +1180,33 @@ 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. + +How else could we avoid generalising over escaping type variables? I +considered: + +* Adjust the generalisation in GHC.Tc.Solver to directly check for + escaping kind variables; instead, promote or default them. But that + gets into the defaulting swamp and is a non-trivial and unforced + change, so I have left it alone for now. + +* When inferring the type of a binding, in `tcMonoBinds`, we create + an ExpSigmaType with `tcInfer`. If we simply gave it an ir_frr field + that said "must have fixed runtime rep", then the kind would be made + Concrete; and we never generalise over Concrete variables. A bit + more indirect, but we need the "don't generalise over Concrete variables" + stuff anyway. + + Note [Impedance matching] ~~~~~~~~~~~~~~~~~~~~~~~~~ Consider diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 374567ce69..c002d8cc3e 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -2037,7 +2037,7 @@ typecheck/should_compile/tc170). Moreover in instance heads we get forall-types with kind Constraint. -It's tempting to check that the body kind is either * or #. But this is +It's tempting to check that the body kind is (TYPE _). But this is wrong. For example: class C a b @@ -2046,7 +2046,7 @@ wrong. For example: We're doing newtype-deriving for C. But notice how `a` isn't in scope in the predicate `C a`. So we quantify, yielding `forall a. C a` even though `C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but -convenient. Bottom line: don't check for * or # here. +convenient. Bottom line: don't check for (TYPE _) here. Note [Body kind of a HsQualTy] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -3547,8 +3547,12 @@ kindGeneralizeSome skol_info wanted kind_or_type -- here will already have all type variables quantified; -- thus, every free variable is really a kv, never a tv. ; dvs <- candidateQTyVarsOfKind kind_or_type - ; dvs <- filterConstrainedCandidates wanted dvs - ; quantifyTyVars skol_info DefaultNonStandardTyVars dvs } + ; filtered_dvs <- filterConstrainedCandidates wanted dvs + ; traceTc "kindGeneralizeSome" $ + vcat [ text "type:" <+> ppr kind_or_type + , text "dvs:" <+> ppr dvs + , text "filtered_dvs:" <+> ppr filtered_dvs ] + ; quantifyTyVars skol_info DefaultNonStandardTyVars filtered_dvs } filterConstrainedCandidates :: WantedConstraints -- Don't quantify over variables free in these diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index fad6cbae4f..b46b994e2f 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -1279,10 +1279,6 @@ emitResidualConstraints rhs_tclvl ev_binds_var -- uniformly. -------------------- -ctsPreds :: Cts -> [PredType] -ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts - , let ev = ctEvidence ct ] - findInferredDiff :: TcThetaType -> TcThetaType -> TcM TcThetaType -- Given a partial type signature f :: (C a, D a, _) => blah -- and the inferred constraints (X a, D a, Y a, C a) @@ -1397,7 +1393,7 @@ Note [Deciding quantification] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If the monomorphism restriction does not apply, then we quantify as follows: -* Step 1: decideMonoTyVars. +* Step 1: decidePromotedTyVars. Take the global tyvars, and "grow" them using functional dependencies E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can happen because alpha is untouchable here) then do not quantify over @@ -1408,10 +1404,11 @@ If the monomorphism restriction does not apply, then we quantify as follows: We also account for the monomorphism restriction; if it applies, add the free vars of all the constraints. - Result is mono_tvs; we will not quantify over these. + Result is mono_tvs; we will promote all of these to the outer levek, + and certainly not quantify over them. * Step 2: defaultTyVarsAndSimplify. - Default any non-mono tyvars (i.e ones that are definitely + Default any non-promoted tyvars (i.e ones that are definitely not going to become further constrained), and re-simplify the candidate constraints. @@ -1431,7 +1428,7 @@ If the monomorphism restriction does not apply, then we quantify as follows: over are determined in Step 3 (not in Step 1), it is OK for the mono_tvs to be missing some variables free in the environment. This is why removing the psig_qtvs is OK in - decideMonoTyVars. Test case for this scenario: T14479. + decidePromotedTyVars. Test case for this scenario: T14479. * Step 3: decideQuantifiedTyVars. Decide which variables to quantify over, as follows: @@ -1559,7 +1556,7 @@ and we are running simplifyInfer over These are two implication constraints, both of which contain a wanted for the class C. Neither constraint mentions the bound -skolem. We might imagine that these constraint could thus float +skolem. We might imagine that these constraints could thus float out of their implications and then interact, causing beta1 to unify with beta2, but constraints do not currently float out of implications. @@ -1609,12 +1606,12 @@ decideQuantification -- See Note [Deciding quantification] decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates = do { -- Step 1: find the mono_tvs - ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode - name_taus psigs candidates + ; (candidates, co_vars) <- decidePromotedTyVars infer_mode + name_taus psigs candidates -- Step 2: default any non-mono tyvars, and re-simplify -- This step may do some unification, but result candidates is zonked - ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates + ; candidates <- defaultTyVarsAndSimplify rhs_tclvl candidates -- Step 3: decide which kind/type variables to quantify over ; qtvs <- decideQuantifiedTyVars skol_info name_taus psigs candidates @@ -1647,7 +1644,6 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates (vcat [ text "infer_mode:" <+> ppr infer_mode , text "candidates:" <+> ppr candidates , text "psig_theta:" <+> ppr psig_theta - , text "mono_tvs:" <+> ppr mono_tvs , text "co_vars:" <+> ppr co_vars , text "qtvs:" <+> ppr qtvs , text "theta:" <+> ppr theta ]) @@ -1686,23 +1682,34 @@ ambiguous types. Something like But that's a battle for another day. -} -decideMonoTyVars :: InferMode - -> [(Name,TcType)] - -> [TcIdSigInst] - -> [PredType] - -> TcM (TcTyCoVarSet, [PredType], CoVarSet) --- Decide which tyvars and covars cannot be generalised: --- (a) Free in the environment --- (b) Mentioned in a constraint we can't generalise --- (c) Connected by an equality or fundep to (a) or (b) +decidePromotedTyVars :: InferMode + -> [(Name,TcType)] + -> [TcIdSigInst] + -> [PredType] + -> TcM ([PredType], CoVarSet) +-- We are about to generalise over type variables at level N +-- Each must be either +-- (P) promoted +-- (D) defaulted +-- (Q) quantified +-- This function finds (P), the type variables that we are going to promote: +-- (a) Mentioned in a constraint we can't generalise (the MR) +-- (b) Mentioned in the kind of a CoVar; we can't quantify over a CoVar, +-- so we must not quantify over a type variable free in its kind +-- (c) Connected by an equality or fundep to +-- * a type variable at level < N, or +-- * A tyvar subject to (a), (b) or (c) +-- Having found all such level-N tyvars that we can't generalise, +-- promote them, to eliminate them from further consideration. +-- -- Also return CoVars that appear free in the final quantified types -- we can't quantify over these, and we must make sure they are in scope -decideMonoTyVars infer_mode name_taus psigs candidates +decidePromotedTyVars infer_mode name_taus psigs candidates = do { (no_quant, maybe_quant) <- pick infer_mode candidates -- If possible, we quantify over partial-sig qtvs, so they are -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs - ; psig_qtvs <- zonkTcTyVarsToTcTyVars $ binderVars $ + ; psig_qtvs <- zonkTcTyVarsToTcTyVars $ binderVars $ concatMap (map snd . sig_inst_skols) psigs ; psig_theta <- mapM TcM.zonkTcType $ @@ -1713,29 +1720,31 @@ decideMonoTyVars infer_mode name_taus psigs candidates ; tc_lvl <- TcM.getTcLevel ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta + -- (b) The co_var_tvs are tvs mentioned in the types of covars or + -- coercion holes. We can't quantify over these covars, so we + -- must include the variable in their types in the mono_tvs. + -- E.g. If we can't quantify over co :: k~Type, then we can't + -- quantify over k either! Hence closeOverKinds + -- Recall that coVarsOfTypes also returns coercion holes co_vars = coVarsOfTypes (psig_tys ++ taus ++ candidates) co_var_tvs = closeOverKinds co_vars - -- The co_var_tvs are tvs mentioned in the types of covars or - -- coercion holes. We can't quantify over these covars, so we - -- must include the variable in their types in the mono_tvs. - -- E.g. If we can't quantify over co :: k~Type, then we can't - -- quantify over k either! Hence closeOverKinds mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $ tyCoVarsOfTypes candidates -- We need to grab all the non-quantifiable tyvars in the -- types so that we can grow this set to find other - -- non-quantifiable tyvars. This can happen with something - -- like + -- non-quantifiable tyvars. This can happen with something like -- f x y = ... -- where z = x 3 -- The body of z tries to unify the type of x (call it alpha[1]) -- with (beta[2] -> gamma[2]). This unification fails because - -- alpha is untouchable. But we need to know not to quantify over - -- beta or gamma, because they are in the equality constraint with - -- alpha. Actual test case: typecheck/should_compile/tc213 + -- alpha is untouchable, leaving [W] alpha[1] ~ (beta[2] -> gamma[2]). + -- We need to know not to quantify over beta or gamma, because they + -- are in the equality constraint with alpha. Actual test case: + -- typecheck/should_compile/tc213 mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs + -- mono_tvs1 is now the set of variables from an outer scope -- (that's mono_tvs0) and the set of covars, closed over kinds. -- Given this set of variables we know we will not quantify, @@ -1749,9 +1758,8 @@ decideMonoTyVars infer_mode name_taus psigs candidates -- (that is, we might have IP "c" Bool and IP "c" Int in different -- places within the same program), and -- skipping this causes implicit params to monomorphise too many - -- variables; see Note [Inheriting implicit parameters] in - -- GHC.Tc.Solver. Skipping causes typecheck/should_compile/tc219 - -- to fail. + -- variables; see Note [Inheriting implicit parameters] in GHC.Tc.Solver. + -- Skipping causes typecheck/should_compile/tc219 to fail. mono_tvs2 = closeWrtFunDeps non_ip_candidates mono_tvs1 -- mono_tvs2 now contains any variable determined by the "root @@ -1761,7 +1769,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates closeWrtFunDeps non_ip_candidates (tyCoVarsOfTypes no_quant) `minusVarSet` mono_tvs2 -- constrained_tvs: the tyvars that we are not going to - -- quantify solely because of the monomorphism restriction + -- quantify /solely/ because of the monomorphism restriction -- -- (`minusVarSet` mono_tvs2): a type variable is only -- "constrained" (so that the MR bites) if it is not @@ -1783,7 +1791,12 @@ decideMonoTyVars infer_mode name_taus psigs candidates let dia = TcRnMonomorphicBindings (map fst name_taus) diagnosticTc (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus) dia - ; traceTc "decideMonoTyVars" $ vcat + -- Promote the mono_tvs + -- See Note [Promote monomorphic tyvars] + ; traceTc "decidePromotedTyVars: promotion:" (ppr mono_tvs) + ; _ <- promoteTyVarSet mono_tvs + + ; traceTc "decidePromotedTyVars" $ vcat [ text "infer_mode =" <+> ppr infer_mode , text "mono_tvs0 =" <+> ppr mono_tvs0 , text "no_quant =" <+> ppr no_quant @@ -1791,7 +1804,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates , text "mono_tvs =" <+> ppr mono_tvs , text "co_vars =" <+> ppr co_vars ] - ; return (mono_tvs, maybe_quant, co_vars) } + ; return (maybe_quant, co_vars) } where pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType]) -- Split the candidates into ones we definitely @@ -1811,48 +1824,34 @@ decideMonoTyVars infer_mode name_taus psigs candidates ------------------- defaultTyVarsAndSimplify :: TcLevel - -> TyCoVarSet -- Promote these mono-tyvars -> [PredType] -- Assumed zonked -> TcM [PredType] -- Guaranteed zonked --- Promote the known-monomorphic tyvars; -- Default any tyvar free in the constraints; -- and re-simplify in case the defaulting allows further simplification -defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates - = do { -- Promote any tyvars that we cannot generalise - -- See Note [Promote monomorphic tyvars] - ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs) - ; _ <- promoteTyVarSet mono_tvs - - -- Default any kind/levity vars +defaultTyVarsAndSimplify rhs_tclvl candidates + = do { -- Default any kind/levity vars ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} <- candidateQTyVarsOfTypes candidates - -- any covars should already be handled by - -- the logic in decideMonoTyVars, which looks at - -- the constraints generated + -- NB1: decidePromotedTyVars has promoted any type variable fixed by the + -- type envt, so they won't be chosen by candidateQTyVarsOfTypes + -- NB2: Defaulting for variables free in tau_tys is done later, by quantifyTyVars + -- Hence looking only at 'candidates' + -- NB3: Any covars should already be handled by + -- the logic in decidePromotedTyVars, which looks at + -- the constraints generated ; poly_kinds <- xoptM LangExt.PolyKinds - ; mapM_ (default_one poly_kinds True) (dVarSetElems cand_kvs) - ; mapM_ (default_one poly_kinds False) (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs)) + ; let default_kv | poly_kinds = default_tv + | otherwise = defaultTyVar DefaultKindVars + default_tv = defaultTyVar (NonStandardDefaulting DefaultNonStandardTyVars) + ; mapM_ default_kv (dVarSetElems cand_kvs) + ; mapM_ default_tv (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs)) ; simplify_cand candidates } where - default_one poly_kinds is_kind_var tv - | not (isMetaTyVar tv) - = return () - | tv `elemVarSet` mono_tvs - = return () - | otherwise - = void $ defaultTyVar - (if not poly_kinds && is_kind_var - then DefaultKindVars - else NonStandardDefaulting DefaultNonStandardTyVars) - -- NB: only pass 'DefaultKindVars' when we know we're dealing with a kind variable. - tv - - -- this common case (no inferred constraints) should be fast - simplify_cand [] = return [] - -- see Note [Unconditionally resimplify constraints when quantifying] + -- See Note [Unconditionally resimplify constraints when quantifying] + simplify_cand [] = return [] -- Fast path simplify_cand candidates = do { clone_wanteds <- newWanteds DefaultOrigin candidates ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $ @@ -2086,7 +2085,7 @@ sure to quantify over them. This leads to several wrinkles: In the signature for 'g', we cannot quantify over 'b' because it turns out to get unified with 'a', which is free in g's environment. So we carefully - refrain from bogusly quantifying, in GHC.Tc.Solver.decideMonoTyVars. We + refrain from bogusly quantifying, in GHC.Tc.Solver.decidePromotedTyVars. We report the error later, in GHC.Tc.Gen.Bind.chooseInferredQuantifiers. Note [growThetaTyVars vs closeWrtFunDeps] @@ -2122,7 +2121,7 @@ constraint (transitively). We use closeWrtFunDeps in places where we need to know which variables are *always* determined by some seed set. This includes - * when determining the mono-tyvars in decideMonoTyVars. If `a` + * when determining the mono-tyvars in decidePromotedTyVars. If `a` is going to be monomorphic, we need b and c to be also: they are determined by the choice for `a`. * when checking instance coverage, in diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index d10c4394f6..7d4911263f 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -15,7 +15,7 @@ module GHC.Tc.Types.Constraint ( assertFuelPrecondition, assertFuelPreconditionStrict, emptyCts, andCts, andManyCts, pprCts, singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList, - isEmptyCts, + isEmptyCts, ctsPreds, isPendingScDict, pendingScDict_maybe, superClassesMightHelp, getPendingWantedScs, isWantedCt, isGivenCt, @@ -1043,6 +1043,9 @@ emptyCts = emptyBag isEmptyCts :: Cts -> Bool isEmptyCts = isEmptyBag +ctsPreds :: Cts -> [PredType] +ctsPreds cts = foldr ((:) . ctPred) [] cts + pprCts :: Cts -> SDoc pprCts cts = vcat (map ppr (bagToList cts)) diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs index 95f2a026a7..d69a3c473a 100644 --- a/compiler/GHC/Tc/Utils/Concrete.hs +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -37,8 +37,12 @@ import GHC.Tc.Utils.TcMType ( newConcreteTyVar, isFilledMetaTyVar_maybe, writ , emitWantedEq ) import GHC.Types.Basic ( TypeOrKind(..) ) +import GHC.Types.Name ( getOccName ) +import GHC.Types.Name.Occurrence( occNameFS ) import GHC.Utils.Misc ( HasDebugCallStack ) import GHC.Utils.Outputable +import GHC.Data.FastString ( fsLit ) + import Control.Monad ( void ) import Data.Functor ( ($>) ) @@ -495,7 +499,7 @@ unifyConcrete frr_orig ty -- Create a new ConcreteTv metavariable @concrete_tv@ -- and unify @ty ~# concrete_tv@. ; _ -> - do { conc_tv <- newConcreteTyVar (ConcreteFRR frr_orig) ki + do { conc_tv <- newConcreteTyVar (ConcreteFRR frr_orig) (fsLit "cx") ki -- NB: newConcreteTyVar asserts that 'ki' is concrete. ; coToMCo <$> emitWantedEq orig KindLevel Nominal ty (mkTyVarTy conc_tv) } } } where @@ -647,9 +651,12 @@ makeTypeConcrete conc_orig ty = , TauTv <- metaTyVarInfo tv -> -- Change the MetaInfo to ConcreteTv, but retain the TcLevel do { kind <- go (tyVarKind tv) + ; let occ_fs = occNameFS (getOccName tv) + -- occ_fs: preserve the occurrence name of the original tyvar + -- This helps in error messages ; lift $ do { conc_tv <- setTcLevel (tcTyVarLevel tv) $ - newConcreteTyVar conc_orig kind + newConcreteTyVar conc_orig occ_fs kind ; let conc_ty = mkTyVarTy conc_tv ; writeMetaTyVar tv conc_ty ; return conc_ty } } diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index d0afe71560..9536f58a58 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -45,8 +45,6 @@ module GHC.Tc.Utils.TcMType ( unpackCoercionHole, unpackCoercionHole_maybe, checkCoercionHole, - ConcreteHole, newConcreteHole, - newImplication, -------------------------------- @@ -414,23 +412,6 @@ checkCoercionHole cv co | otherwise = False --- | A coercion hole used to store evidence for `Concrete#` constraints. --- --- See Note [The Concrete mechanism]. -type ConcreteHole = CoercionHole - --- | Create a new (initially unfilled) coercion hole, --- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint. -newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy') - -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep') - -> TcM (ConcreteHole, TcType) - -- ^ where to put the evidence, and a metavariable to store - -- the concrete type -newConcreteHole ki ty - = do { concrete_ty <- newFlexiTyVarTy ki - ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty - ; hole <- newCoercionHole co_ty - ; return (hole, concrete_ty) } {- ********************************************************************** * @@ -840,11 +821,13 @@ cloneTyVarTyVar name kind -- -- Invariant: the kind must be concrete, as per Note [ConcreteTv]. -- This is checked with an assertion. -newConcreteTyVar :: HasDebugCallStack => ConcreteTvOrigin -> TcKind -> TcM TcTyVar -newConcreteTyVar reason kind = - assertPpr (isConcrete kind) - (text "newConcreteTyVar: non-concrete kind" <+> ppr kind) - $ newAnonMetaTyVar (ConcreteTv reason) kind +newConcreteTyVar :: HasDebugCallStack => ConcreteTvOrigin + -> FastString -> TcKind -> TcM TcTyVar +newConcreteTyVar reason fs kind + = assertPpr (isConcrete kind) assert_msg $ + newNamedAnonMetaTyVar fs (ConcreteTv reason) kind + where + assert_msg = text "newConcreteTyVar: non-concrete kind" <+> ppr kind newPatSigTyVar :: Name -> Kind -> TcM TcTyVar newPatSigTyVar name kind @@ -1242,14 +1225,14 @@ NB: this is all rather similar to, but sadly not the same as Wrinkle: -We must make absolutely sure that alpha indeed is not -from an outer context. (Otherwise, we might indeed learn more information -about it.) This can be done easily: we just check alpha's TcLevel. -That level must be strictly greater than the ambient TcLevel in order -to treat it as naughty. We say "strictly greater than" because the call to +We must make absolutely sure that alpha indeed is not from an outer +context. (Otherwise, we might indeed learn more information about it.) +This can be done easily: we just check alpha's TcLevel. That level +must be strictly greater than the ambient TcLevel in order to treat it +as naughty. We say "strictly greater than" because the call to candidateQTyVars is made outside the bumped TcLevel, as stated in the -comment to candidateQTyVarsOfType. The level check is done in go_tv -in collect_cand_qtvs. Skipping this check caused #16517. +comment to candidateQTyVarsOfType. The level check is done in go_tv in +collect_cand_qtvs. Skipping this check caused #16517. -} @@ -1349,8 +1332,9 @@ candidateQTyVarsWithBinders :: [TyVar] -> Type -> TcM CandidatesQTvs -- Because we are going to scoped-sort the quantified variables -- in among the tvs candidateQTyVarsWithBinders bound_tvs ty - = do { kvs <- candidateQTyVarsOfKinds (map tyVarKind bound_tvs) - ; all_tvs <- collect_cand_qtvs ty False emptyVarSet kvs ty + = do { kvs <- candidateQTyVarsOfKinds (map tyVarKind bound_tvs) + ; cur_lvl <- getTcLevel + ; all_tvs <- collect_cand_qtvs ty False cur_lvl emptyVarSet kvs ty ; return (all_tvs `delCandidates` bound_tvs) } -- | Gathers free variables to use as quantification candidates (in @@ -1362,14 +1346,18 @@ candidateQTyVarsWithBinders bound_tvs ty -- See Note [Dependent type variables] candidateQTyVarsOfType :: TcType -- not necessarily zonked -> TcM CandidatesQTvs -candidateQTyVarsOfType ty = collect_cand_qtvs ty False emptyVarSet mempty ty +candidateQTyVarsOfType ty + = do { cur_lvl <- getTcLevel + ; collect_cand_qtvs ty False cur_lvl emptyVarSet mempty ty } -- | Like 'candidateQTyVarsOfType', but over a list of types -- The variables to quantify must have a TcLevel strictly greater than -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates]) candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs -candidateQTyVarsOfTypes tys = foldlM (\acc ty -> collect_cand_qtvs ty False emptyVarSet acc ty) - mempty tys +candidateQTyVarsOfTypes tys + = do { cur_lvl <- getTcLevel + ; foldlM (\acc ty -> collect_cand_qtvs ty False cur_lvl emptyVarSet acc ty) + mempty tys } -- | Like 'candidateQTyVarsOfType', but consider every free variable -- to be dependent. This is appropriate when generalizing a *kind*, @@ -1377,16 +1365,21 @@ candidateQTyVarsOfTypes tys = foldlM (\acc ty -> collect_cand_qtvs ty False empt -- to Type.) candidateQTyVarsOfKind :: TcKind -- Not necessarily zonked -> TcM CandidatesQTvs -candidateQTyVarsOfKind ty = collect_cand_qtvs ty True emptyVarSet mempty ty +candidateQTyVarsOfKind ty + = do { cur_lvl <- getTcLevel + ; collect_cand_qtvs ty True cur_lvl emptyVarSet mempty ty } candidateQTyVarsOfKinds :: [TcKind] -- Not necessarily zonked -> TcM CandidatesQTvs -candidateQTyVarsOfKinds tys = foldM (\acc ty -> collect_cand_qtvs ty True emptyVarSet acc ty) - mempty tys +candidateQTyVarsOfKinds tys + = do { cur_lvl <- getTcLevel + ; foldM (\acc ty -> collect_cand_qtvs ty True cur_lvl emptyVarSet acc ty) + mempty tys } collect_cand_qtvs - :: TcType -- original type that we started recurring into; for errors + :: TcType -- Original type that we started recurring into; for errors -> Bool -- True <=> consider every fv in Type to be dependent + -> TcLevel -- Current TcLevel; collect only tyvars whose level is greater -> VarSet -- Bound variables (locals only) -> CandidatesQTvs -- Accumulating parameter -> Type -- Not necessarily zonked @@ -1403,7 +1396,7 @@ collect_cand_qtvs -- so that subsequent dependency analysis (to build a well -- scoped telescope) works correctly -collect_cand_qtvs orig_ty is_dep bound dvs ty +collect_cand_qtvs orig_ty is_dep cur_lvl bound dvs ty = go dvs ty where is_bound tv = tv `elemVarSet` bound @@ -1411,13 +1404,13 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty ----------------- go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs -- Uses accumulating-parameter style - go dv (AppTy t1 t2) = foldlM go dv [t1, t2] - go dv (TyConApp tc tys) = go_tc_args dv (tyConBinders tc) tys + go dv (AppTy t1 t2) = foldlM go dv [t1, t2] + go dv (TyConApp tc tys) = go_tc_args dv (tyConBinders tc) tys go dv (FunTy _ w arg res) = foldlM go dv [w, arg, res] - go dv (LitTy {}) = return dv - go dv (CastTy ty co) = do dv1 <- go dv ty - collect_cand_qtvs_co orig_ty bound dv1 co - go dv (CoercionTy co) = collect_cand_qtvs_co orig_ty bound dv co + go dv (LitTy {}) = return dv + go dv (CastTy ty co) = do { dv1 <- go dv ty + ; collect_cand_qtvs_co orig_ty cur_lvl bound dv1 co } + go dv (CoercionTy co) = collect_cand_qtvs_co orig_ty cur_lvl bound dv co go dv (TyVarTy tv) | is_bound tv = return dv @@ -1427,8 +1420,8 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty Nothing -> go_tv dv tv } go dv (ForAllTy (Bndr tv _) ty) - = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv) - ; collect_cand_qtvs orig_ty is_dep (bound `extendVarSet` tv) dv1 ty } + = do { dv1 <- collect_cand_qtvs orig_ty True cur_lvl bound dv (tyVarKind tv) + ; collect_cand_qtvs orig_ty is_dep cur_lvl (bound `extendVarSet` tv) dv1 ty } -- This makes sure that we default e.g. the alpha in Proxy alpha (Any alpha). -- Tested in polykinds/NestedProxies. @@ -1437,7 +1430,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty -- to look at kinds. go_tc_args dv (tc_bndr:tc_bndrs) (ty:tys) = do { dv1 <- collect_cand_qtvs orig_ty (is_dep || isNamedTyConBinder tc_bndr) - bound dv ty + cur_lvl bound dv ty ; go_tc_args dv1 tc_bndrs tys } go_tc_args dv _bndrs tys -- _bndrs might be non-empty: undersaturation -- tys might be non-empty: oversaturation @@ -1446,6 +1439,21 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty ----------------- go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv + | tcTyVarLevel tv <= cur_lvl + = return dv -- This variable is from an outer context; skip + -- See Note [Use level numbers for quantification] + + | case tcTyVarDetails tv of + SkolemTv _ lvl _ -> lvl > pushTcLevel cur_lvl + _ -> False + = return dv -- Skip inner skolems + -- This only happens for erroneous program with bad telescopes + -- e.g. BadTelescope2: forall a k (b :: k). SameKind a b + -- We have (a::k), and at the outer we don't want to quantify + -- over the already-quantified skolem k. + -- (Apparently we /do/ want to quantify over skolems whose level sk_lvl is + -- sk_lvl > cur_lvl; you get lots of failures otherwise. A battle for another day.) + | tv `elemDVarSet` kvs = return dv -- We have met this tyvar already @@ -1461,17 +1469,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty -- (which comes next) works correctly ; let tv_kind_vars = tyCoVarsOfType tv_kind - ; cur_lvl <- getTcLevel - ; if | tcTyVarLevel tv <= cur_lvl - -> return dv -- this variable is from an outer context; skip - -- See Note [Use level numbers for quantification] - - | case tcTyVarDetails tv of - SkolemTv _ lvl _ -> lvl > pushTcLevel cur_lvl - _ -> False - -> return dv -- Skip inner skolems; ToDo: explain - - | intersectsVarSet bound tv_kind_vars + ; if | intersectsVarSet bound tv_kind_vars -- the tyvar must not be from an outer context, but we have -- already checked for this. -- See Note [Naughty quantification candidates] @@ -1490,25 +1488,26 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty -- See Note [Order of accumulation] -- See Note [Recurring into kinds for candidateQTyVars] - ; collect_cand_qtvs orig_ty True bound dv' tv_kind } } + ; collect_cand_qtvs orig_ty True cur_lvl bound dv' tv_kind } } collect_cand_qtvs_co :: TcType -- original type at top of recursion; for errors + -> TcLevel -> VarSet -- bound variables -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs -collect_cand_qtvs_co orig_ty bound = go_co +collect_cand_qtvs_co orig_ty cur_lvl bound = go_co where - go_co dv (Refl ty) = collect_cand_qtvs orig_ty True bound dv ty - go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs orig_ty True bound dv ty - go_mco dv1 mco + go_co dv (Refl ty) = collect_cand_qtvs orig_ty True cur_lvl bound dv ty + go_co dv (GRefl _ ty mco) = do { dv1 <- collect_cand_qtvs orig_ty True cur_lvl bound dv ty + ; go_mco dv1 mco } go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2] go_co dv (FunCo _ _ _ w co1 co2) = foldlM go_co dv [w, co1, co2] go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos - go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov - dv2 <- collect_cand_qtvs orig_ty True bound dv1 t1 - collect_cand_qtvs orig_ty True bound dv2 t2 + go_co dv (UnivCo prov _ t1 t2) = do { dv1 <- go_prov dv prov + ; dv2 <- collect_cand_qtvs orig_ty True cur_lvl bound dv1 t1 + ; collect_cand_qtvs orig_ty True cur_lvl bound dv2 t2 } go_co dv (SymCo co) = go_co dv co go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2] go_co dv (SelCo _ co) = go_co dv co @@ -1527,7 +1526,7 @@ collect_cand_qtvs_co orig_ty bound = go_co go_co dv (ForAllCo tcv kind_co co) = do { dv1 <- go_co dv kind_co - ; collect_cand_qtvs_co orig_ty (bound `extendVarSet` tcv) dv1 co } + ; collect_cand_qtvs_co orig_ty cur_lvl (bound `extendVarSet` tcv) dv1 co } go_mco dv MRefl = return dv go_mco dv (MCo co) = go_co dv co @@ -1543,7 +1542,7 @@ collect_cand_qtvs_co orig_ty bound = go_co | cv `elemVarSet` cvs = return dv -- See Note [Recurring into kinds for candidateQTyVars] - | otherwise = collect_cand_qtvs orig_ty True bound + | otherwise = collect_cand_qtvs orig_ty True cur_lvl bound (dv { dv_cvs = cvs `extendVarSet` cv }) (idType cv) @@ -1810,17 +1809,30 @@ defaultTyVar def_strat tv = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv) ; writeMetaTyVar tv liftedRepTy ; return True } + | isLevityVar tv , default_ns_vars = do { traceTc "Defaulting a Levity var to Lifted" (ppr tv) ; writeMetaTyVar tv liftedDataConTy ; return True } + | isMultiplicityVar tv , default_ns_vars = do { traceTc "Defaulting a Multiplicity var to Many" (ppr 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 @@ -1872,9 +1884,8 @@ defaultTyVars ns_strat dvs ; let def_tvs, def_kvs :: DefaultingStrategy def_tvs = NonStandardDefaulting ns_strat - def_kvs - | poly_kinds = def_tvs - | otherwise = DefaultKindVars + def_kvs | poly_kinds = def_tvs + | otherwise = DefaultKindVars -- As -XNoPolyKinds precludes polymorphic kind variables, we default them. -- For example: -- @@ -1965,7 +1976,7 @@ What do do? D. We could error. We choose (D), as described in #17567, and implement this choice in -doNotQuantifyTyVars. Discussion of alternativs A-C is below. +doNotQuantifyTyVars. Discussion of alternatives A-C is below. NB: this is all rather similar to, but sadly not the same as Note [Naughty quantification candidates] diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index f088a7e6ab..d9df4913bc 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -475,7 +475,7 @@ This is not OK: we get MkT :: forall l. T @l :: TYPE (BoxedRep l) which is ill-kinded. -For ordinary /user-written type signatures f :: blah, we make this +For ordinary /user-written/ type signatures f :: blah, we make this check as part of kind-checking the type signature in tcHsSigType; see Note [Escaping kind in type signatures] in GHC.Tc.Gen.HsType. diff --git a/testsuite/tests/rep-poly/RepPolyArgument.stderr b/testsuite/tests/rep-poly/RepPolyArgument.stderr index c6aaded15b..45c9474839 100644 --- a/testsuite/tests/rep-poly/RepPolyArgument.stderr +++ b/testsuite/tests/rep-poly/RepPolyArgument.stderr @@ -3,8 +3,8 @@ RepPolyArgument.hs:10:18: error: [GHC-55287] • The argument ‘(undefined @(R @RuntimeRep))’ of ‘undefined’ does not have a fixed runtime representation. Its type is: - t0 :: TYPE c0 - Cannot unify ‘R’ with the type variable ‘c0’ + t1 :: TYPE t0 + Cannot unify ‘R’ with the type variable ‘t0’ because it is not a concrete ‘RuntimeRep’. • In the first argument of ‘undefined’, namely ‘(undefined @(R @RuntimeRep))’ diff --git a/testsuite/tests/rep-poly/RepPolyDoBind.stderr b/testsuite/tests/rep-poly/RepPolyDoBind.stderr index 920499675a..5a4468761a 100644 --- a/testsuite/tests/rep-poly/RepPolyDoBind.stderr +++ b/testsuite/tests/rep-poly/RepPolyDoBind.stderr @@ -4,8 +4,8 @@ RepPolyDoBind.hs:26:3: error: [GHC-55287] arising from a do statement does not have a fixed runtime representation. Its type is: - ma0 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + ma0 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In a stmt of a 'do' block: a <- undefined In the expression: diff --git a/testsuite/tests/rep-poly/RepPolyDoBody1.stderr b/testsuite/tests/rep-poly/RepPolyDoBody1.stderr index a1126fd637..d683950855 100644 --- a/testsuite/tests/rep-poly/RepPolyDoBody1.stderr +++ b/testsuite/tests/rep-poly/RepPolyDoBody1.stderr @@ -4,8 +4,8 @@ RepPolyDoBody1.hs:24:3: error: [GHC-55287] arising from a do statement does not have a fixed runtime representation. Its type is: - ma0 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + ma0 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In a stmt of a 'do' block: undefined :: ma In the expression: diff --git a/testsuite/tests/rep-poly/RepPolyDoBody2.stderr b/testsuite/tests/rep-poly/RepPolyDoBody2.stderr index 2678d90f33..70ea8834bd 100644 --- a/testsuite/tests/rep-poly/RepPolyDoBody2.stderr +++ b/testsuite/tests/rep-poly/RepPolyDoBody2.stderr @@ -4,8 +4,8 @@ RepPolyDoBody2.hs:23:3: error: [GHC-55287] arising from a do statement does not have a fixed runtime representation. Its type is: - mb0 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + mb0 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In a stmt of a 'do' block: undefined :: () In the expression: diff --git a/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr b/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr index 9597abade3..32e6635ce7 100644 --- a/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr +++ b/testsuite/tests/rep-poly/RepPolyLeftSection2.stderr @@ -3,8 +3,8 @@ RepPolyLeftSection2.hs:14:11: error: [GHC-55287] • The argument ‘undefined’ of ‘f’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE c0 - Cannot unify ‘r’ with the type variable ‘c0’ + a0 :: TYPE r0 + Cannot unify ‘r’ with the type variable ‘r0’ because it is not a concrete ‘RuntimeRep’. • In the expression: undefined `f` In an equation for ‘test1’: test1 = (undefined `f`) diff --git a/testsuite/tests/rep-poly/RepPolyMcBind.stderr b/testsuite/tests/rep-poly/RepPolyMcBind.stderr index d08ef575a4..b0e6947606 100644 --- a/testsuite/tests/rep-poly/RepPolyMcBind.stderr +++ b/testsuite/tests/rep-poly/RepPolyMcBind.stderr @@ -4,8 +4,8 @@ RepPolyMcBind.hs:26:16: error: [GHC-55287] arising from a statement in a monad comprehension does not have a fixed runtime representation. Its type is: - ma0 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + ma0 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In a stmt of a monad comprehension: x <- undefined :: ma In the expression: [() | x <- undefined :: ma] diff --git a/testsuite/tests/rep-poly/RepPolyMcBody.stderr b/testsuite/tests/rep-poly/RepPolyMcBody.stderr index 4c52bb4729..1d92c6db46 100644 --- a/testsuite/tests/rep-poly/RepPolyMcBody.stderr +++ b/testsuite/tests/rep-poly/RepPolyMcBody.stderr @@ -4,8 +4,8 @@ RepPolyMcBody.hs:30:16: error: [GHC-55287] arising from a statement in a monad comprehension does not have a fixed runtime representation. Its type is: - ma0 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + ma0 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In a stmt of a monad comprehension: True In the expression: [() | True] diff --git a/testsuite/tests/rep-poly/RepPolyMcGuard.stderr b/testsuite/tests/rep-poly/RepPolyMcGuard.stderr index 69d4bf2bf5..90768aaab3 100644 --- a/testsuite/tests/rep-poly/RepPolyMcGuard.stderr +++ b/testsuite/tests/rep-poly/RepPolyMcGuard.stderr @@ -4,8 +4,8 @@ RepPolyMcGuard.hs:30:16: error: [GHC-55287] arising from a statement in a monad comprehension does not have a fixed runtime representation. Its type is: - a0 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + a0 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In a stmt of a monad comprehension: undefined In the expression: [() | undefined] diff --git a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr index a227f454f6..103b295263 100644 --- a/testsuite/tests/rep-poly/RepPolyNPlusK.stderr +++ b/testsuite/tests/rep-poly/RepPolyNPlusK.stderr @@ -3,4 +3,4 @@ RepPolyNPlusK.hs:22:1: error: [GHC-55287] The first pattern in the equation for ‘foo’ does not have a fixed runtime representation. Its type is: - a :: TYPE rep1 + a :: TYPE rep2 diff --git a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr index f7a47b4a4f..51a57fe27d 100644 --- a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr +++ b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr @@ -17,8 +17,8 @@ RepPolyRecordUpdate.hs:13:9: error: [GHC-55287] • The record update at field ‘fld’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE c1 - Cannot unify ‘rep’ with the type variable ‘c1’ + a0 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In a record update at field ‘fld’, with type constructor ‘X’ diff --git a/testsuite/tests/rep-poly/RepPolyRule1.stderr b/testsuite/tests/rep-poly/RepPolyRule1.stderr index a7f524cf99..a160eacffc 100644 --- a/testsuite/tests/rep-poly/RepPolyRule1.stderr +++ b/testsuite/tests/rep-poly/RepPolyRule1.stderr @@ -3,8 +3,8 @@ RepPolyRule1.hs:11:51: error: [GHC-55287] • The argument ‘x’ of ‘f’ does not have a fixed runtime representation. Its type is: - a1 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + a1 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In the first argument of ‘f’, namely ‘x’ In the expression: f x @@ -16,8 +16,8 @@ RepPolyRule1.hs:11:55: error: [GHC-55287] • The argument ‘x’ of ‘f’ does not have a fixed runtime representation. Its type is: - a1 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + a1 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In the expression: x When checking the rewrite rule "f_id" diff --git a/testsuite/tests/rep-poly/RepPolyTupleSection.stderr b/testsuite/tests/rep-poly/RepPolyTupleSection.stderr index a6f03bf2a1..5b3e6656da 100644 --- a/testsuite/tests/rep-poly/RepPolyTupleSection.stderr +++ b/testsuite/tests/rep-poly/RepPolyTupleSection.stderr @@ -3,8 +3,8 @@ RepPolyTupleSection.hs:11:7: error: [GHC-55287] • The second component of the tuple section does not have a fixed runtime representation. Its type is: - t0 :: TYPE c0 - Cannot unify ‘r’ with the type variable ‘c0’ + t1 :: TYPE t0 + Cannot unify ‘r’ with the type variable ‘t0’ because it is not a concrete ‘RuntimeRep’. • In the expression: (# 3#, #) In an equation for ‘foo’: foo = (# 3#, #) diff --git a/testsuite/tests/rep-poly/T12709.stderr b/testsuite/tests/rep-poly/T12709.stderr index 3dea77979e..083f24d46a 100644 --- a/testsuite/tests/rep-poly/T12709.stderr +++ b/testsuite/tests/rep-poly/T12709.stderr @@ -3,8 +3,8 @@ T12709.hs:28:13: error: [GHC-55287] • The argument ‘1’ of ‘(+)’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE c0 - Cannot unify ‘rep’ with the type variable ‘c0’ + a0 :: TYPE rep0 + Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In the expression: 1 + 2 + 3 + 4 In an equation for ‘u’: u = 1 + 2 + 3 + 4 diff --git a/testsuite/tests/rep-poly/T12973.stderr b/testsuite/tests/rep-poly/T12973.stderr index f0c89e63a9..00c84add32 100644 --- a/testsuite/tests/rep-poly/T12973.stderr +++ b/testsuite/tests/rep-poly/T12973.stderr @@ -3,8 +3,8 @@ T12973.hs:13:7: error: [GHC-55287] • The argument ‘3’ of ‘(+)’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE c0 - Cannot unify ‘r’ with the type variable ‘c0’ + a0 :: TYPE r0 + Cannot unify ‘r’ with the type variable ‘r0’ because it is not a concrete ‘RuntimeRep’. • In the expression: 3 + 4 In an equation for ‘foo’: foo = 3 + 4 diff --git a/testsuite/tests/rep-poly/T13929.stderr b/testsuite/tests/rep-poly/T13929.stderr index fe8c845a8b..837c1d4501 100644 --- a/testsuite/tests/rep-poly/T13929.stderr +++ b/testsuite/tests/rep-poly/T13929.stderr @@ -3,8 +3,8 @@ T13929.hs:29:24: error: [GHC-55287] • The tuple argument in first position does not have a fixed runtime representation. Its type is: - a0 :: TYPE c0 - Cannot unify ‘rf’ with the type variable ‘c0’ + a0 :: TYPE k00 + Cannot unify ‘rf’ with the type variable ‘k00’ because it is not a concrete ‘RuntimeRep’. • In the expression: (# gunbox x, gunbox y #) In an equation for ‘gunbox’: diff --git a/testsuite/tests/rep-poly/T19615.stderr b/testsuite/tests/rep-poly/T19615.stderr index eb56692c3c..4fb11522da 100644 --- a/testsuite/tests/rep-poly/T19615.stderr +++ b/testsuite/tests/rep-poly/T19615.stderr @@ -3,8 +3,8 @@ T19615.hs:17:21: error: [GHC-55287] • The argument ‘(f x)’ of ‘lift'’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE c0 - Cannot unify ‘r'’ with the type variable ‘c0’ + a0 :: TYPE r0 + Cannot unify ‘r'’ with the type variable ‘r0’ because it is not a concrete ‘RuntimeRep’. • In the first argument of ‘lift'’, namely ‘(f x)’ In the expression: lift' (f x) id diff --git a/testsuite/tests/rep-poly/T19709b.stderr b/testsuite/tests/rep-poly/T19709b.stderr index da2d53d272..d098a1ee83 100644 --- a/testsuite/tests/rep-poly/T19709b.stderr +++ b/testsuite/tests/rep-poly/T19709b.stderr @@ -3,8 +3,8 @@ T19709b.hs:11:15: error: [GHC-55287] • The argument ‘(error @Any "e2")’ of ‘levfun’ does not have a fixed runtime representation. Its type is: - a1 :: TYPE c0 - Cannot unify ‘Any’ with the type variable ‘c0’ + a1 :: TYPE r0 + Cannot unify ‘Any’ with the type variable ‘r0’ because it is not a concrete ‘RuntimeRep’. • In the first argument of ‘levfun’, namely ‘(error @Any "e2")’ In the first argument of ‘seq’, namely ‘levfun (error @Any "e2")’ diff --git a/testsuite/tests/rep-poly/T23051.hs b/testsuite/tests/rep-poly/T23051.hs new file mode 100644 index 0000000000..e8455b53b2 --- /dev/null +++ b/testsuite/tests/rep-poly/T23051.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE MagicHash #-} +module M where + +import GHC.Exts + +i :: forall k (f :: k -> RuntimeRep) (g :: k) (a :: TYPE (f g)). a -> a +i = i + +x = i 0# diff --git a/testsuite/tests/rep-poly/T23051.stderr b/testsuite/tests/rep-poly/T23051.stderr new file mode 100644 index 0000000000..778ca7a1a7 --- /dev/null +++ b/testsuite/tests/rep-poly/T23051.stderr @@ -0,0 +1,10 @@ + +T23051.hs:9:7: error: [GHC-18872] + • Couldn't match kind ‘IntRep’ with ‘f0 g0’ + When matching types + a :: TYPE (f0 g0) + Int# :: TYPE IntRep + • In the first argument of ‘i’, namely ‘0#’ + In the expression: i 0# + In an equation for ‘x’: x = i 0# + • Relevant bindings include x :: a (bound at T23051.hs:9:1) diff --git a/testsuite/tests/rep-poly/all.T b/testsuite/tests/rep-poly/all.T index 33044ae9fe..a01a2529ae 100644 --- a/testsuite/tests/rep-poly/all.T +++ b/testsuite/tests/rep-poly/all.T @@ -113,3 +113,6 @@ test('RepPolyTuple2', normal, compile_fail, ['']) ## see #21683 ## test('T21650_a', normal, compile_fail, ['-Wno-deprecated-flags']) ## test('T21650_b', normal, compile_fail, ['-Wno-deprecated-flags']) ## ############################################################################### + + +test('T23051', normal, compile_fail, ['']) |