[Git][ghc/ghc][wip/T23051] Be more careful about quantification
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu Mar 16 11:03:12 UTC 2023
Simon Peyton Jones pushed to branch wip/T23051 at Glasgow Haskell Compiler / GHC
Commits:
4e06ba8b by Simon Peyton Jones at 2023-03-16T11:04:41+00:00
Be more careful about quantification
This MR is driven by #23051. It does several things:
* It is guided by the generalisation plan described in #20686.
But it is still far from a complete implementation of that plan.
* Add Note [Inferred type with escaping kind] to GHC.Tc.Gen.Bind.
This explains that we don't (yet, pending #20686) directly
prevent generalising over escaping kinds.
* In `GHC.Tc.Utils.TcMType.defaultTyVar` we default RuntimeRep
and Multiplicity variables, beause we don't want to quantify over
them. We want to do the same for a Concrete tyvar, but there is
nothing sensible to default it to (unless it has kind RuntimeRep,
in which case it'll be caught by an earlier case). So we promote
instead.
* Pure refactoring in GHC.Tc.Solver:
* Rename decideMonoTyVars to decidePromotedTyVars, since that's
what it does.
* Move the actual promotion of the tyvars-to-promote from
`defaultTyVarsAndSimplify` to `decidePromotedTyVars`. This is a
no-op; just tidies up the code. E.g then we don't need to
return the promoted tyvars from `decidePromotedTyVars`.
* A little refactoring in `defaultTyVarsAndSimplify`, but no
change in behaviour.
* When making a TauTv unification variable into a ConcreteTv
(in GHC.Tc.Utils.Concrete.makeTypeConcrete), preserve the occ-name
of the type variable. This just improves error messages.
* Kill off dead code: GHC.Tc.Utils.TcMType.newConcreteHole
- - - - -
26 changed files:
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Utils/Concrete.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Validity.hs
- testsuite/tests/rep-poly/RepPolyArgument.stderr
- testsuite/tests/rep-poly/RepPolyDoBind.stderr
- testsuite/tests/rep-poly/RepPolyDoBody1.stderr
- testsuite/tests/rep-poly/RepPolyDoBody2.stderr
- testsuite/tests/rep-poly/RepPolyLeftSection2.stderr
- testsuite/tests/rep-poly/RepPolyMcBind.stderr
- testsuite/tests/rep-poly/RepPolyMcBody.stderr
- testsuite/tests/rep-poly/RepPolyMcGuard.stderr
- testsuite/tests/rep-poly/RepPolyNPlusK.stderr
- testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr
- testsuite/tests/rep-poly/RepPolyRule1.stderr
- testsuite/tests/rep-poly/RepPolyTupleSection.stderr
- testsuite/tests/rep-poly/T12709.stderr
- testsuite/tests/rep-poly/T12973.stderr
- testsuite/tests/rep-poly/T13929.stderr
- testsuite/tests/rep-poly/T19615.stderr
- testsuite/tests/rep-poly/T19709b.stderr
- + testsuite/tests/rep-poly/T23051.hs
- + testsuite/tests/rep-poly/T23051.stderr
- testsuite/tests/rep-poly/all.T
Changes:
=====================================
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,30 @@ 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 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 could 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.
+
+* 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
=====================================
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
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1397,7 +1397,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 +1408,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 +1432,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 +1560,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 +1610,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 +1648,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 +1686,36 @@ 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.
+-- But we can't generalise over type variables that are:
+-- Namely type variables that are:
+-- (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 +1726,30 @@ 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
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 +1763,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 +1774,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 +1796,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 +1809,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 +1829,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 +2090,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 +2126,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
=====================================
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 at .
; _ ->
- 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 } }
=====================================
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,22 @@ 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, but we definitely do; you get lots of failures otherwise.
+ -- A battle for another day.)
+
| tv `elemDVarSet` kvs
= return dv -- We have met this tyvar already
@@ -1461,17 +1470,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 +1489,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 +1527,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 +1543,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 +1810,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
@@ -1965,7 +1978,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]
=====================================
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.
=====================================
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))’
=====================================
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:
=====================================
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:
=====================================
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:
=====================================
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`)
=====================================
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]
=====================================
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]
=====================================
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]
=====================================
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
=====================================
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’
=====================================
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"
=====================================
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#, #)
=====================================
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
=====================================
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
=====================================
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’:
=====================================
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
=====================================
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")’
=====================================
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#
=====================================
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)
=====================================
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, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4e06ba8b1168d7346090848433aff9311fb1a2f9
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4e06ba8b1168d7346090848433aff9311fb1a2f9
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/20230316/f277faee/attachment-0001.html>
More information about the ghc-commits
mailing list