Commit c8c63dde authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Never Anyify during kind inference

See Note [Error on unconstrained meta-variables] in TcMType.

Close #17301
Close #17567
Close #17562
Close #15474
parent f88fb8c7
Pipeline #29704 canceled with stages
......@@ -440,7 +440,7 @@ emptyLHsQTvs = HsQTvs { hsq_ext = [], hsq_explicit = [] }
-- we use use HsOuterImplicit, wrapped around a HsForAllTy
-- for the visible quantification
--
-- See Note [forall-or-nothing] rule
-- See Note [forall-or-nothing rule]
-- | The outermost type variables in a type that obeys the @forall@-or-nothing
-- rule. See @Note [forall-or-nothing rule]@.
......
......@@ -537,7 +537,8 @@ tc_top_lhs_type tyki ctxt (L loc sig_ty@(HsSig { sig_bndrs = hs_outer_bndrs
; kvs <- kindGeneralizeAll ty1 -- "All" because it's a top-level type
; reportUnsolvedEqualities skol_info kvs tclvl wanted
; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)
; ze <- mkEmptyZonkEnv NoFlexi
; final_ty <- zonkTcTypeToTypeX ze (mkInfForAllTys kvs ty1)
; traceTc "tc_top_lhs_type }" (vcat [ppr sig_ty, ppr final_ty])
; return final_ty }
where
......
......@@ -410,13 +410,14 @@ tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty
-- These are /signatures/ so we zonk to squeeze out any kind
-- unification variables. Do this after kindGeneralizeAll which may
-- default kind variables to *.
; (ze, kv_bndrs) <- zonkTyVarBinders (mkTyVarBinders InferredSpec kvs)
; (ze, implicit_bndrs) <- zonkTyVarBindersX ze implicit_bndrs
; (ze, univ_bndrs) <- zonkTyVarBindersX ze univ_bndrs
; (ze, ex_bndrs) <- zonkTyVarBindersX ze ex_bndrs
; req <- zonkTcTypesToTypesX ze req
; prov <- zonkTcTypesToTypesX ze prov
; body_ty <- zonkTcTypeToTypeX ze body_ty
; ze <- mkEmptyZonkEnv NoFlexi
; (ze, kv_bndrs) <- zonkTyVarBindersX ze (mkTyVarBinders InferredSpec kvs)
; (ze, implicit_bndrs) <- zonkTyVarBindersX ze implicit_bndrs
; (ze, univ_bndrs) <- zonkTyVarBindersX ze univ_bndrs
; (ze, ex_bndrs) <- zonkTyVarBindersX ze ex_bndrs
; req <- zonkTcTypesToTypesX ze req
; prov <- zonkTcTypesToTypesX ze prov
; body_ty <- zonkTcTypeToTypeX ze body_ty
-- Now do validity checking
; checkValidType ctxt $
......
......@@ -662,7 +662,7 @@ rewrite_vector ki roles tys
tys
}
where
(bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki -- "RAE" fix
(bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
fvs = tyCoVarsOfType ki
{-# INLINE rewrite_vector #-}
......
......@@ -887,10 +887,10 @@ generaliseTcTyCon (tc, scoped_prs, tc_res_kind)
-- Step 3: Final zonk (following kind generalisation)
-- See Note [Swizzling the tyvars before generaliseTcTyCon]
; ze <- emptyZonkEnv
; (ze, inferred) <- zonkTyBndrsX ze inferred
; (ze, sorted_spec_tvs) <- zonkTyBndrsX ze sorted_spec_tvs
; (ze, req_tvs) <- zonkTyBndrsX ze req_tvs
; ze <- mkEmptyZonkEnv NoFlexi
; (ze, inferred) <- zonkTyBndrsX ze inferred
; (ze, sorted_spec_tvs) <- zonkTyBndrsX ze sorted_spec_tvs
; (ze, req_tvs) <- zonkTyBndrsX ze req_tvs
; tc_res_kind <- zonkTcTypeToTypeX ze tc_res_kind
; traceTc "generaliseTcTyCon: post zonk" $
......@@ -2346,13 +2346,24 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
; at_stuff <- tcClassATs class_name clas ats at_defs
; return (ctxt, fds, sig_stuff, at_stuff) }
-- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
-- Example: (typecheck/should_fail/T17562)
-- type C :: Type -> Type -> Constraint
-- class (forall a. a b ~ a c) => C b c
-- The kind of `a` is unconstrained.
; dvs <- candidateQTyVarsOfTypes ctxt
; let mk_doc tidy_env = do { (tidy_env2, ctxt) <- zonkTidyTcTypes tidy_env ctxt
; return ( tidy_env2
, sep [ text "the class context:"
, pprTheta ctxt ] ) }
; doNotQuantifyTyVars dvs mk_doc
-- The pushLevelAndSolveEqualities will report errors for any
-- unsolved equalities, so these zonks should not encounter
-- any unfilled coercion variables unless there is such an error
-- The zonk also squeeze out the TcTyCons, and converts
-- Skolems to tyvars.
; ze <- emptyZonkEnv
; ze <- mkEmptyZonkEnv NoFlexi
; ctxt <- zonkTcTypesToTypesX ze ctxt
; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff
-- ToDo: do we need to zonk at_stuff?
......@@ -2739,7 +2750,20 @@ tcTySynRhs roles_info tc_name hs_ty
; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
; rhs_ty <- pushLevelAndSolveEqualities skol_info (binderVars binders) $
tcCheckLHsType hs_ty (TheKind res_kind)
; rhs_ty <- zonkTcTypeToType rhs_ty
-- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
-- Example: (typecheck/should_fail/T17567)
-- type T = forall a. Proxy a
-- The kind of `a` is unconstrained.
; dvs <- candidateQTyVarsOfType rhs_ty
; let mk_doc tidy_env = do { (tidy_env2, rhs_ty) <- zonkTidyTcType tidy_env rhs_ty
; return ( tidy_env2
, sep [ text "the type synonym right-hand side:"
, ppr rhs_ty ] ) }
; doNotQuantifyTyVars dvs mk_doc
; ze <- mkEmptyZonkEnv NoFlexi
; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty
; let roles = roles_info tc_name
; return (buildSynTyCon tc_name binders res_kind roles rhs_ty) }
where
......@@ -2776,10 +2800,24 @@ tcDataDefn err_ctxt roles_info tc_name
; let skol_tvs = binderVars tycon_binders
; stupid_tc_theta <- pushLevelAndSolveEqualities skol_info skol_tvs $
tcHsContext ctxt
; stupid_theta <- zonkTcTypesToTypes stupid_tc_theta
; kind_signatures <- xoptM LangExt.KindSignatures
-- Check that we don't use kind signatures without Glasgow extensions
-- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
-- Example: (typecheck/should_fail/T17567StupidTheta)
-- data (forall a. a b ~ a c) => T b c
-- The kind of 'a' is unconstrained.
; dvs <- candidateQTyVarsOfTypes stupid_tc_theta
; let mk_doc tidy_env
= do { (tidy_env2, theta) <- zonkTidyTcTypes tidy_env stupid_tc_theta
; return ( tidy_env2
, sep [ text "the datatype context:"
, pprTheta theta ] ) }
; doNotQuantifyTyVars dvs mk_doc
; ze <- mkEmptyZonkEnv NoFlexi
; stupid_theta <- zonkTcTypesToTypesX ze stupid_tc_theta
-- Check that we don't use kind signatures without the extension
; kind_signatures <- xoptM LangExt.KindSignatures
; when (isJust mb_ksig) $
checkTc (kind_signatures) (badSigTyDecl tc_name)
......@@ -3016,7 +3054,18 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
, text "lhs_ty" <+> ppr lhs_ty
, text "qtvs" <+> pprTyVars qtvs ]
; (ze, qtvs) <- zonkTyBndrs qtvs
-- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType
-- Example: typecheck/should_fail/T17301
; dvs_rhs <- candidateQTyVarsOfType rhs_ty
; let mk_doc tidy_env
= do { (tidy_env2, rhs_ty) <- zonkTidyTcType tidy_env rhs_ty
; return ( tidy_env2
, sep [ text "type family equation right-hand side:"
, ppr rhs_ty ] ) }
; doNotQuantifyTyVars dvs_rhs mk_doc
; ze <- mkEmptyZonkEnv NoFlexi
; (ze, qtvs) <- zonkTyBndrsX ze qtvs
; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty
......@@ -3283,10 +3332,11 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs res_kind tag_map
-- See test dependent/should_fail/T13780a
-- Zonk to Types
; (ze, qkvs) <- zonkTyBndrs kvs
; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs
; ze <- mkEmptyZonkEnv NoFlexi
; (ze, qkvs) <- zonkTyBndrsX ze kvs
; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs
; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys
; ctxt <- zonkTcTypesToTypesX ze ctxt
; ctxt <- zonkTcTypesToTypesX ze ctxt
-- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
......@@ -3368,10 +3418,11 @@ tcConDecl new_or_data dd_info rep_tycon tc_bndrs _res_kind tag_map
; let tvbndrs = mkTyVarBinders InferredSpec tkvs ++ outer_tv_bndrs
-- Zonk to Types
; (ze, tvbndrs) <- zonkTyVarBinders tvbndrs
; ze <- mkEmptyZonkEnv NoFlexi
; (ze, tvbndrs) <- zonkTyVarBindersX ze tvbndrs
; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys
; ctxt <- zonkTcTypesToTypesX ze ctxt
; res_ty <- zonkTcTypeToTypeX ze res_ty
; ctxt <- zonkTcTypesToTypesX ze ctxt
; res_ty <- zonkTcTypeToTypeX ze res_ty
; let res_tmpl = mkDDHeaderTy dd_info rep_tycon tc_bndrs
(univ_tvs, ex_tvs, tvbndrs', eq_preds, arg_subst)
......
......@@ -912,9 +912,10 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
-- Zonk the patterns etc into the Type world
; (ze, qtvs) <- zonkTyBndrs qtvs
; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
; ze <- mkEmptyZonkEnv NoFlexi
; (ze, qtvs) <- zonkTyBndrsX ze qtvs
; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
; master_res_kind <- zonkTcTypeToTypeX ze master_res_kind
; instance_res_kind <- zonkTcTypeToTypeX ze instance_res_kind
......
......@@ -228,7 +228,7 @@ mkProvEvidence ev_id
dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
-- See Note [Coercions that escape]
dependentArgErr (arg, bad_cos)
= addErrTc $
= failWithTc $ -- fail here: otherwise we get downstream errors
vcat [ text "Iceland Jack! Iceland Jack! Stop torturing me!"
, hang (text "Pattern-bound variable")
2 (ppr arg <+> dcolon <+> ppr (idType arg))
......@@ -675,11 +675,12 @@ tc_patsyn_finish lname dir is_infix lpat' prag_fn
= do { -- Zonk everything. We are about to build a final PatSyn
-- so there had better be no unification variables in there
(ze, univ_tvs') <- zonkTyVarBinders univ_tvs
; ze <- mkEmptyZonkEnv NoFlexi
; (ze, univ_tvs') <- zonkTyVarBindersX ze univ_tvs
; req_theta' <- zonkTcTypesToTypesX ze req_theta
; (ze, ex_tvs') <- zonkTyVarBindersX ze ex_tvs
; (ze, ex_tvs') <- zonkTyVarBindersX ze ex_tvs
; prov_theta' <- zonkTcTypesToTypesX ze prov_theta
; pat_ty' <- zonkTcTypeToTypeX ze pat_ty
; pat_ty' <- zonkTcTypeToTypeX ze pat_ty
; arg_tys' <- zonkTcTypesToTypesX ze arg_tys
; let (env1, univ_tvs) = tidyTyCoVarBinders emptyTidyEnv univ_tvs'
......
......@@ -83,6 +83,7 @@ module GHC.Tc.Utils.TcMType (
defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
quantifyTyVars, isQuantifiableTv,
skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar,
doNotQuantifyTyVars,
candidateQTyVarsOfType, candidateQTyVarsOfKind,
candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
......@@ -1299,6 +1300,29 @@ instance Outputable CandidatesQTvs where
, text "dv_tvs =" <+> ppr tvs
, text "dv_cvs =" <+> ppr cvs ])
isEmptyCandidates :: CandidatesQTvs -> Bool
isEmptyCandidates (DV { dv_kvs = kvs, dv_tvs = tvs })
= isEmptyDVarSet kvs && isEmptyDVarSet tvs
-- | Extract out the kind vars (in order) and type vars (in order) from
-- a 'CandidatesQTvs'. The lists are guaranteed to be distinct. Keeping
-- the lists separate is important only in the -XNoPolyKinds case.
candidateVars :: CandidatesQTvs -> ([TcTyVar], [TcTyVar])
candidateVars (DV { dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
= (dep_kvs, nondep_tvs)
where
dep_kvs = scopedSort $ dVarSetElems dep_kv_set
-- scopedSort: put the kind variables into
-- well-scoped order.
-- E.g. [k, (a::k)] not the other way round
nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
-- See Note [Dependent type variables]
-- The `minus` dep_tkvs removes any kind-level vars
-- e.g. T k (a::k) Since k appear in a kind it'll
-- be in dv_kvs, and is dependent. So remove it from
-- dv_tvs which will also contain k
-- NB kinds of tvs are already zonked
candidateKindVars :: CandidatesQTvs -> TyVarSet
candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
......@@ -1377,7 +1401,7 @@ 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 _ tys) = foldlM go dv tys
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
......@@ -1395,6 +1419,20 @@ collect_cand_qtvs orig_ty is_dep bound dvs 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 }
-- This makes sure that we default e.g. the alpha in Proxy alpha (Any alpha).
-- Tested in polykinds/NestedProxies.
-- We just might get this wrong in AppTy, but I don't think that's possible
-- with -XNoPolyKinds. And fixing it would be non-performant, as we'd need
-- 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
; 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
-- either way, the foldlM is correct
= foldlM go dv tys
-----------------
go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
| tv `elemDVarSet` kvs
......@@ -1415,7 +1453,7 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
; cur_lvl <- getTcLevel
; if | tcTyVarLevel tv <= cur_lvl
-> return dv -- this variable is from an outer context; skip
-- See Note [Use level numbers ofor quantification]
-- See Note [Use level numbers for quantification]
| intersectsVarSet bound tv_kind_vars
-- the tyvar must not be from an outer context, but we have
......@@ -1566,7 +1604,7 @@ are about to wrap in a forall.
It takes these free type/kind variables (partitioned into dependent and
non-dependent variables) skolemises metavariables with a TcLevel greater
than the ambient level (see Note [Use level numbers of quantification]).
than the ambient level (see Note [Use level numbers for quantification]).
* This function distinguishes between dependent and non-dependent
variables only to keep correct defaulting behavior with -XNoPolyKinds.
......@@ -1642,46 +1680,21 @@ quantifyTyVars :: CandidatesQTvs -- See Note [Dependent type variables]
-- invariants on CandidateQTvs, we do not have to filter out variables
-- free in the environment here. Just quantify unconditionally, subject
-- to the restrictions in Note [quantifyTyVars].
quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
quantifyTyVars dvs
-- short-circuit common case
| isEmptyDVarSet dep_kv_set
, isEmptyDVarSet nondep_tkv_set
| isEmptyCandidates dvs
= do { traceTc "quantifyTyVars has nothing to quantify" empty
; return [] }
| otherwise
= do { traceTc "quantifyTyVars {" (ppr dvs)
; let dep_kvs = scopedSort $ dVarSetElems dep_kv_set
-- scopedSort: put the kind variables into
-- well-scoped order.
-- E.g. [k, (a::k)] not the other way round
nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
-- See Note [Dependent type variables]
-- The `minus` dep_tkvs removes any kind-level vars
-- e.g. T k (a::k) Since k appear in a kind it'll
-- be in dv_kvs, and is dependent. So remove it from
-- dv_tvs which will also contain k
-- NB kinds of tvs are already zonked
-- In the non-PolyKinds case, default the kind variables
-- to *, and zonk the tyvars as usual. Notice that this
-- may make quantifyTyVars return a shorter list
-- than it was passed, but that's ok
; poly_kinds <- xoptM LangExt.PolyKinds
; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs
; let final_qtvs = dep_kvs' ++ nondep_tvs'
-- Because of the order, any kind variables
-- mentioned in the kinds of the nondep_tvs'
-- now refer to the dep_kvs'
; undefaulted <- defaultTyVars dvs
; final_qtvs <- mapMaybeM zonk_quant undefaulted
; traceTc "quantifyTyVars }"
(vcat [ text "nondep:" <+> pprTyVars nondep_tvs
, text "dep:" <+> pprTyVars dep_kvs
, text "dep_kvs'" <+> pprTyVars dep_kvs'
, text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
(vcat [ text "undefaulted:" <+> pprTyVars undefaulted
, text "final_qtvs:" <+> pprTyVars final_qtvs ])
-- We should never quantify over coercion variables; check this
; let co_vars = filter isCoVar final_qtvs
......@@ -1691,9 +1704,8 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
where
-- zonk_quant returns a tyvar if it should be quantified over;
-- otherwise, it returns Nothing. The latter case happens for
-- * Kind variables, with -XNoPolyKinds: don't quantify over these
-- * RuntimeRep variables: we never quantify over these
zonk_quant default_kind tkv
-- non-meta-tyvars
zonk_quant tkv
| not (isTyVar tkv)
= return Nothing -- this can happen for a covar that's associated with
-- a coercion hole. Test case: typecheck/should_compile/T2494
......@@ -1703,11 +1715,7 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
-- kind signature, we have the class variables in
-- scope, and they are TyVars not TcTyVars
| otherwise
= do { deflt_done <- defaultTyVar default_kind tkv
; case deflt_done of
True -> return Nothing
False -> do { tv <- skolemiseQuantifiedTyVar tkv
; return (Just tv) } }
= Just <$> skolemiseQuantifiedTyVar tkv
isQuantifiableTv :: TcLevel -- Level of the context, outside the quantification
-> TcTyVar
......@@ -1817,6 +1825,24 @@ defaultTyVar default_kind tv
where
(_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
-- | Default some unconstrained type variables:
-- RuntimeRep tyvars default to LiftedRep
-- Multiplicity tyvars default to Many
-- Type tyvars from dv_kvs default to Type, when -XNoPolyKinds
-- (under -XNoPolyKinds, non-defaulting vars in dv_kvs is an error)
defaultTyVars :: CandidatesQTvs -- ^ all candidates for quantification
-> TcM [TcTyVar] -- ^ those variables not defaulted
defaultTyVars dvs
= do { poly_kinds <- xoptM LangExt.PolyKinds
; defaulted_kvs <- mapM (defaultTyVar (not poly_kinds)) dep_kvs
; defaulted_tvs <- mapM (defaultTyVar False) nondep_tvs
; let undefaulted_kvs = [ kv | (kv, False) <- dep_kvs `zip` defaulted_kvs ]
undefaulted_tvs = [ tv | (tv, False) <- nondep_tvs `zip` defaulted_tvs ]
; return (undefaulted_kvs ++ undefaulted_tvs) }
-- NB: kvs before tvs because tvs may depend on kvs
where
(dep_kvs, nondep_tvs) = candidateVars dvs
skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar
-- We have a Meta tyvar with a ref-cell inside it
-- Skolemise it, so that we are totally out of Meta-tyvar-land
......@@ -1851,6 +1877,134 @@ skolemiseUnboundMetaTyVar tv
Indirect ty -> WARN( True, ppr tv $$ ppr ty )
return () }
{- Note [Error on unconstrained meta-variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
type C :: Type -> Type -> Constraint
class (forall a. a b ~ a c) => C b c
or
type T = forall a. Proxy a
or
data (forall a. a b ~ a c) => T b c
We will infer a :: Type -> kappa... but then we get no further information
on kappa. What to do?
A. We could choose kappa := Type. But this only works when the kind of kappa
is Type (true in this example, but not always).
B. We could default to Any.
C. We could quantify.
D. We could error.
We choose (D), as described in #17567. Discussion of alternatives is below.
(One last example: type instance F Int = Proxy Any, where the unconstrained
kind variable is the inferred kind of Any. The four examples here illustrate
all cases in which this Note applies.)
To do this, we must take an extra step before doing the final zonk to create
e.g. a TyCon. (There is no problem in the final term-level zonk. See the
section on alternative (B) below.) This extra step is needed only for
constructs that do not quantify their free meta-variables, such as a class
constraint or right-hand side of a type synonym.
Specifically: before the final zonk, every construct must either call
quantifyTyVars or doNotQuantifyTyVars. The latter issues an error
if it is passed any free variables. (Exception: we still default
RuntimeRep and Multiplicity variables.)
Because no meta-variables remain after quantifying or erroring, we perform
the zonk with NoFlexi, which panics upon seeing a meta-variable.
Alternatives not implemented:
A. As stated above, this works only sometimes. We might have a free
meta-variable of kind Nat, for example.
B. This is what we used to do, but it caused Any to appear in error
messages sometimes. See #17567 for several examples. Defaulting to
Any during the final, whole-program zonk is OK, though, because
we are completely done type-checking at that point. No chance to
leak into an error message.
C. Examine the class declaration at the top of this Note again.
Where should we quantify? We might imagine quantifying and
putting the kind variable in the forall of the quantified constraint.
But what if there are nested foralls? Which one should get the
variable? Other constructs have other problems. (For example,
the right-hand side of a type family instance equation may not
be a poly-type.)
More broadly, the GHC AST defines a set of places where it performs
implicit lexical generalization. For example, in a type
signature
f :: Proxy a -> Bool
the otherwise-unbound a is lexically quantified, giving us
f :: forall a. Proxy a -> Bool
The places that allow lexical quantification are marked in the AST with
HsImplicitBndrs. HsImplicitBndrs offers a binding site for otherwise-unbound
variables.
Later, during type-checking, we discover that a's kind is unconstrained.
We thus quantify *again*, to
f :: forall {k} (a :: k). Proxy @k a -> Bool
It is this second quantification that this Note is really about --
let's call it *inferred quantification*.
So there are two sorts of implicit quantification in types:
1. Lexical quantification: signalled by HsImplicitBndrs, occurs over
variables mentioned by the user but with no explicit binding site,
suppressed by a user-written forall (by the forall-or-nothing rule,
in Note [forall-or-nothing rule] in GHC.Hs.Type).
2. Inferred quantification: no signal in HsSyn, occurs over unconstrained
variables invented by the type-checker, possible only with -XPolyKinds,
unaffected by forall-or-nothing rule
These two quantifications are performed in different compiler phases, and are
essentially unrelated. However, it is convenient
for programmers to remember only one set of implicit quantification
sites. So, we choose to use the same places (those with HsImplicitBndrs)
for lexical quantification as for inferred quantification of unconstrained
meta-variables. Accordingly, there is no quantification in a class
constraint, or the other constructs that call doNotQuantifyTyVars.
-}
doNotQuantifyTyVars :: CandidatesQTvs
-> (TidyEnv -> TcM (TidyEnv, SDoc))
-- ^ like "the class context (D a b, E foogle)"
-> TcM ()
doNotQuantifyTyVars dvs where_found
| isEmptyCandidates dvs
= traceTc "doNotQuantifyTyVars has nothing to error on" empty
| otherwise
= do { traceTc "doNotQuantifyTyVars" (ppr dvs)
; undefaulted <- defaultTyVars dvs
-- could have regular TyVars here, in an associated type RHS, or
-- bound by a type declaration head. So filter looking only for
-- metavars. e.g. b and c in `class (forall a. a b ~ a c) => C b c`
-- are OK
; let leftover_metas = filter isMetaTyVar undefaulted
; unless (null leftover_metas) $
do { let (tidy_env1, tidied_tvs) = tidyOpenTyCoVars emptyTidyEnv leftover_metas
; (tidy_env2, where_doc) <- where_found tidy_env1
; let doc = vcat [ text "Uninferrable type variable"
<> plural tidied_tvs
<+> pprWithCommas pprTyVar tidied_tvs
<+> text "in"
, where_doc ]
; failWithTcM (tidy_env2, pprWithExplicitKindsWhen True doc) }
; traceTc "doNotQuantifyTyVars success" empty }
{- Note [Defaulting with -XNoPolyKinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
......
......@@ -33,10 +33,10 @@ module GHC.Tc.Utils.Zonk (
zonkTopDecls, zonkTopExpr, zonkTopLExpr,
zonkTopBndrs,
ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX,
zonkTyVarBindersX, zonkTyVarBinderX,
zonkTyBndrs, zonkTyBndrsX,
zonkTcTypeToType, zonkTcTypeToTypeX,
zonkTcTypesToTypes, zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX,
zonkTcTypesToTypesX, zonkScaledTcTypesToTypesX,
zonkTyVarOcc,
zonkCoToCo,
zonkEvBinds, zonkTcEvBinds,
......@@ -284,6 +284,10 @@ There are three possibilities:
It's a way to have a variable that is not a mutable
unification variable, but doesn't have a binding site
either.
* NoFlexi: See Note [Error on unconstrained meta-variables]
in GHC.Tc.Utils.TcMType. This mode will panic on unfilled
meta-variables.
-}
data ZonkFlexi -- See Note [Un-unified unification variables]
......@@ -291,6 +295,9 @@ data ZonkFlexi -- See Note [Un-unified unification variables]
| SkolemiseFlexi -- Skolemise unbound unification variables
-- See Note [Zonking the LHS of a RULE]
| RuntimeUnkFlexi -- Used in the GHCi debugger
| NoFlexi -- Panic on unfilled meta-variables
-- See Note [Error on unconstrained meta-variables]
-- in GHC.Tc.Utils.TcMType
instance Outputable ZonkEnv where
ppr (ZonkEnv { ze_tv_env = tv_env
......@@ -452,10 +459,6 @@ zonkTyBndrX env tv
; let tv' = mkTyVar (tyVarName tv) ki
; return (extendTyZonkEnv env tv', tv') }
zonkTyVarBinders :: [VarBndr TcTyVar vis]
-> TcM (ZonkEnv, [VarBndr TyVar vis])
zonkTyVarBinders tvbs = initZonkEnv $ \ ze -> zonkTyVarBindersX ze tvbs
zonkTyVarBindersX :: ZonkEnv -> [VarBndr TcTyVar vis]
-> TcM (ZonkEnv, [VarBndr TyVar vis])
zonkTyVarBindersX = mapAccumLM zonkTyVarBinderX
......@@ -1847,6 +1850,9 @@ commitFlexi flexi tv zonked_kind
-- otherwise-unconstrained unification variables are
-- turned into RuntimeUnks as they leave the
-- typechecker's monad
NoFlexi -> pprPanic "NoFlexi" (ppr tv <+> dcolon <+> ppr zonked_kind)
where
name = tyVarName tv
......@@ -1899,9 +1905,6 @@ zonkTcTyConToTyCon tc
zonkTcTypeToType :: TcType -> TcM Type
zonkTcTypeToType ty = initZonkEnv $ \ ze -> zonkTcTypeToTypeX ze ty
zonkTcTypesToTypes :: [TcType] -> TcM [Type]
zonkTcTypesToTypes tys = initZonkEnv $ \ ze -> zonkTcTypesToTypesX ze tys
zonkScaledTcTypeToTypeX :: ZonkEnv -> Scaled TcType -> TcM (Scaled TcType)
zonkScaledTcTypeToTypeX env (Scaled m ty) = Scaled <$> zonkTcTypeToTypeX env m
<*> zonkTcTypeToTypeX env ty
......
......@@ -128,7 +128,7 @@ gcast x = do Refl <- eqT (typeRep :: TypeRep a)
return x