summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc
diff options
context:
space:
mode:
authorRyan Scott <ryan.gl.scott@gmail.com>2020-07-05 16:15:01 -0400
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-11-06 03:45:28 -0500
commite07e383a3250cb27a9128ad8d5c68def5c3df336 (patch)
treeb580fd84319138a3508303356318ac9b78750009 /compiler/GHC/Tc
parent2125b1d6bea0c620e3a089603dace6bb38020c81 (diff)
downloadhaskell-e07e383a3250cb27a9128ad8d5c68def5c3df336.tar.gz
Replace HsImplicitBndrs with HsOuterTyVarBndrs
This refactors the GHC AST to remove `HsImplicitBndrs` and replace it with `HsOuterTyVarBndrs`, a type which records whether the outermost quantification in a type is explicit (i.e., with an outermost, invisible `forall`) or implicit. As a result of this refactoring, it is now evident in the AST where the `forall`-or-nothing rule applies: it's all the places that use `HsOuterTyVarBndrs`. See the revamped `Note [forall-or-nothing rule]` in `GHC.Hs.Type` (previously in `GHC.Rename.HsType`). Moreover, the places where `ScopedTypeVariables` brings lexically scoped type variables into scope are a subset of the places that adhere to the `forall`-or-nothing rule, so this also makes places that interact with `ScopedTypeVariables` easier to find. See the revamped `Note [Lexically scoped type variables]` in `GHC.Hs.Type` (previously in `GHC.Tc.Gen.Sig`). `HsOuterTyVarBndrs` are used in type signatures (see `HsOuterSigTyVarBndrs`) and type family equations (see `HsOuterFamEqnTyVarBndrs`). The main difference between the former and the latter is that the former cares about specificity but the latter does not. There are a number of knock-on consequences: * There is now a dedicated `HsSigType` type, which is the combination of `HsOuterSigTyVarBndrs` and `HsType`. `LHsSigType` is now an alias for an `XRec` of `HsSigType`. * Working out the details led us to a substantial refactoring of the handling of explicit (user-written) and implicit type-variable bindings in `GHC.Tc.Gen.HsType`. Instead of a confusing family of higher order functions, we now have a local data type, `SkolemInfo`, that controls how these binders are kind-checked. It remains very fiddly, not fully satisfying. But it's better than it was. Fixes #16762. Bumps the Haddock submodule. Co-authored-by: Simon Peyton Jones <simonpj@microsoft.com> Co-authored-by: Richard Eisenberg <rae@richarde.dev> Co-authored-by: Zubin Duggal <zubin@cmi.ac.in>
Diffstat (limited to 'compiler/GHC/Tc')
-rw-r--r--compiler/GHC/Tc/Deriv.hs19
-rw-r--r--compiler/GHC/Tc/Deriv/Generate.hs23
-rw-r--r--compiler/GHC/Tc/Errors.hs11
-rw-r--r--compiler/GHC/Tc/Gen/Bind.hs2
-rw-r--r--compiler/GHC/Tc/Gen/Head.hs2
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs805
-rw-r--r--compiler/GHC/Tc/Gen/Pat.hs12
-rw-r--r--compiler/GHC/Tc/Gen/Sig.hs119
-rw-r--r--compiler/GHC/Tc/Module.hs14
-rw-r--r--compiler/GHC/Tc/Solver.hs50
-rw-r--r--compiler/GHC/Tc/Solver/Canonical.hs2
-rw-r--r--compiler/GHC/Tc/TyCl.hs170
-rw-r--r--compiler/GHC/Tc/TyCl/Class.hs10
-rw-r--r--compiler/GHC/Tc/TyCl/Instance.hs39
-rw-r--r--compiler/GHC/Tc/TyCl/PatSyn.hs104
-rw-r--r--compiler/GHC/Tc/Types/Constraint.hs57
-rw-r--r--compiler/GHC/Tc/Types/Origin.hs5
-rw-r--r--compiler/GHC/Tc/Utils/Env.hs4
-rw-r--r--compiler/GHC/Tc/Utils/Instantiate.hs29
-rw-r--r--compiler/GHC/Tc/Utils/Monad.hs4
-rw-r--r--compiler/GHC/Tc/Utils/Unify.hs15
-rw-r--r--compiler/GHC/Tc/Validity.hs2
22 files changed, 915 insertions, 583 deletions
diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs
index 9e9adbb961..407cb6a21b 100644
--- a/compiler/GHC/Tc/Deriv.hs
+++ b/compiler/GHC/Tc/Deriv.hs
@@ -500,7 +500,7 @@ derivePred tc tys mb_lderiv_strat via_tvs deriv_pred =
-- We carefully set up uses of recoverM to minimize error message
-- cascades. See Note [Recovering from failures in deriving clauses].
recoverM (pure Nothing) $
- setSrcSpan (getLoc (hsSigType deriv_pred)) $ do
+ setSrcSpan (getLoc deriv_pred) $ do
traceTc "derivePred" $ vcat
[ text "tc" <+> ppr tc
, text "tys" <+> ppr tys
@@ -718,18 +718,15 @@ tcStandaloneDerivInstType
:: UserTypeCtxt -> LHsSigWcType GhcRn
-> TcM ([TyVar], DerivContext, Class, [Type])
tcStandaloneDerivInstType ctxt
- (HsWC { hswc_body = deriv_ty@(HsIB { hsib_ext = vars
- , hsib_body = deriv_ty_body })})
- | (tvs, theta, rho) <- splitLHsSigmaTyInvis deriv_ty_body
+ (HsWC { hswc_body = deriv_ty@(L loc (HsSig { sig_bndrs = outer_bndrs
+ , sig_body = deriv_ty_body }))})
+ | (theta, rho) <- splitLHsQualTy deriv_ty_body
, L _ [wc_pred] <- theta
, L wc_span (HsWildCardTy _) <- ignoreParens wc_pred
- = do dfun_ty <- tcHsClsInstType ctxt $
- HsIB { hsib_ext = vars
- , hsib_body
- = L (getLoc deriv_ty_body) $
- HsForAllTy { hst_tele = mkHsForAllInvisTele tvs
- , hst_xforall = noExtField
- , hst_body = rho }}
+ = do dfun_ty <- tcHsClsInstType ctxt $ L loc $
+ HsSig { sig_ext = noExtField
+ , sig_bndrs = outer_bndrs
+ , sig_body = rho }
let (tvs, _theta, cls, inst_tys) = tcSplitDFunTy dfun_ty
pure (tvs, InferContext (Just wc_span), cls, inst_tys)
| otherwise
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index 33c0765c69..a2ba8d1dbb 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -596,7 +596,9 @@ unliftedCompare lt_op eq_op a_expr b_expr lt eq gt
-- mean more tests (dynamically)
nlHsIf (ascribeBool $ genPrimOpApp a_expr eq_op b_expr) eq gt
where
- ascribeBool e = nlExprWithTySig e $ nlHsTyVar boolTyCon_RDR
+ ascribeBool e = noLoc $ ExprWithTySig noExtField e
+ $ mkHsWildCardBndrs $ noLoc $ mkHsImplicitSigType
+ $ nlHsTyVar boolTyCon_RDR
nlConWildPat :: DataCon -> LPat GhcPs
-- The pattern (K {})
@@ -1890,7 +1892,7 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
--
-- op :: forall c. a -> [T x] -> c -> Int
L loc $ ClassOpSig noExtField False [loc_meth_RDR]
- $ mkLHsSigType $ nlHsCoreTy to_ty
+ $ L loc $ mkHsImplicitSigType $ nlHsCoreTy to_ty
)
where
Pair from_ty to_ty = mkCoerceClassMethEqn cls inst_tvs inst_tys rhs_ty meth_id
@@ -1948,11 +1950,6 @@ nlHsAppType e s = noLoc (HsAppType noExtField e hs_ty)
where
hs_ty = mkHsWildCardBndrs $ parenthesizeHsType appPrec $ nlHsCoreTy s
-nlExprWithTySig :: LHsExpr GhcPs -> LHsType GhcPs -> LHsExpr GhcPs
-nlExprWithTySig e s = noLoc $ ExprWithTySig noExtField (parenthesizeHsExpr sigPrec e) hs_ty
- where
- hs_ty = mkLHsSigWcType s
-
nlHsCoreTy :: Type -> LHsType GhcPs
nlHsCoreTy = noLoc . XHsType . NHsCoreTy
@@ -2082,19 +2079,21 @@ genAuxBindSpecDup loc original_rdr_name dup_spec
genAuxBindSpecSig :: SrcSpan -> AuxBindSpec -> LHsSigWcType GhcPs
genAuxBindSpecSig loc spec = case spec of
DerivCon2Tag tycon _
- -> mkLHsSigWcType $ L loc $ XHsType $ NHsCoreTy $
+ -> mk_sig $ L loc $ XHsType $ NHsCoreTy $
mkSpecSigmaTy (tyConTyVars tycon) (tyConStupidTheta tycon) $
mkParentType tycon `mkVisFunTyMany` intPrimTy
DerivTag2Con tycon _
- -> mkLHsSigWcType $ L loc $
+ -> mk_sig $ L loc $
XHsType $ NHsCoreTy $ mkSpecForAllTys (tyConTyVars tycon) $
intTy `mkVisFunTyMany` mkParentType tycon
DerivMaxTag _ _
- -> mkLHsSigWcType (L loc (XHsType (NHsCoreTy intTy)))
+ -> mk_sig (L loc (XHsType (NHsCoreTy intTy)))
DerivDataDataType _ _ _
- -> mkLHsSigWcType (nlHsTyVar dataType_RDR)
+ -> mk_sig (nlHsTyVar dataType_RDR)
DerivDataConstr _ _ _
- -> mkLHsSigWcType (nlHsTyVar constr_RDR)
+ -> mk_sig (nlHsTyVar constr_RDR)
+ where
+ mk_sig = mkHsWildCardBndrs . L loc . mkHsImplicitSigType
type SeparateBagsDerivStuff =
-- DerivAuxBinds
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 8b50d5e719..37dc095f71 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -438,8 +438,13 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs
where
tcl_env = ic_env implic
insoluble = isInsolubleStatus status
- (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) tvs
- info' = tidySkolemInfo env1 info
+ (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) $
+ scopedSort tvs
+ -- scopedSort: the ic_skols may not be in dependency order
+ -- (see Note [Skolems in an implication] in GHC.Tc.Types.Constraint)
+ -- but tidying goes wrong on out-of-order constraints;
+ -- so we sort them here before tidying
+ info' = tidySkolemInfo env1 info
implic' = implic { ic_skols = tvs'
, ic_given = map (tidyEvVar env1) given
, ic_info = info' }
@@ -507,7 +512,7 @@ warnRedundantConstraints ctxt env info ev_vars
= any isImprovementPred (pred : transSuperClasses pred)
reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcTyVar] -> TcM ()
-reportBadTelescope ctxt env (ForAllSkol _ telescope) skols
+reportBadTelescope ctxt env (ForAllSkol telescope) skols
= do { msg <- mkErrorReport ctxt env (important doc)
; reportError msg }
where
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 97d997897f..e1077b883a 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -1659,7 +1659,7 @@ decideGeneralisationPlan dflags lbinds closed sig_fn
= [ null theta
| TcIdSig (PartialSig { psig_hs_ty = hs_ty })
<- mapMaybe sig_fn (collectHsBindListBinders lbinds)
- , let (_, L _ theta, _) = splitLHsSigmaTyInvis (hsSigWcType hs_ty) ]
+ , let (L _ theta, _) = splitLHsQualTy (hsSigWcType hs_ty) ]
has_partial_sigs = not (null partial_sig_mrs)
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 783e4b3773..524d97077d 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -632,7 +632,7 @@ tcExprWithSig expr hs_ty
; (expr', poly_ty) <- tcExprSig expr sig_info
; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) }
where
- loc = getLoc (hsSigWcType hs_ty)
+ loc = getLoc (dropWildCards hs_ty)
tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType)
tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 889923743c..685a1bc815 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -29,7 +29,12 @@ module GHC.Tc.Gen.HsType (
bindImplicitTKBndrs_Q_Tv, bindImplicitTKBndrs_Q_Skol,
bindExplicitTKBndrs_Tv, bindExplicitTKBndrs_Skol,
bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol,
- ContextKind(..),
+
+ bindOuterFamEqnTKBndrs, bindOuterFamEqnTKBndrs_Q_Tv,
+ tcOuterTKBndrs, scopedSortOuter,
+ bindOuterSigTKBndrs_Tv,
+ tcExplicitTKBndrs,
+ bindNamedWildCardBinders,
-- Type checking type and class decls, and instances thereof
bindTyClTyVars, tcFamTyPats,
@@ -42,8 +47,8 @@ module GHC.Tc.Gen.HsType (
-- No kind generalisation, no checkValidType
InitialKindStrategy(..),
SAKS_or_CUSK(..),
+ ContextKind(..),
kcDeclHeader,
- tcNamedWildCardBinders,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcInferLHsTypeKind, tcInferLHsType, tcInferLHsTypeUnsaturated,
@@ -335,13 +340,13 @@ funsSigCtxt :: [Located Name] -> UserTypeCtxt
funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
funsSigCtxt [] = panic "funSigCtxt"
-addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
+addSigCtxt :: Outputable hs_ty => UserTypeCtxt -> Located hs_ty -> TcM a -> TcM a
addSigCtxt ctxt hs_ty thing_inside
= setSrcSpan (getLoc hs_ty) $
addErrCtxt (pprSigCtxt ctxt hs_ty) $
thing_inside
-pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
+pprSigCtxt :: Outputable hs_ty => UserTypeCtxt -> Located hs_ty -> SDoc
-- (pprSigCtxt ctxt <extra> <type>)
-- prints In the type signature for 'f':
-- f :: <type>
@@ -361,9 +366,9 @@ tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
-- already checked this, so we can simply ignore it.
tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
-kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
+kcClassSigType :: [Located Name] -> LHsSigType GhcRn -> TcM ()
-- This is a special form of tcClassSigType that is used during the
--- kind-checking phase to infer the kind of class variables. Cf. tc_hs_sig_type.
+-- kind-checking phase to infer the kind of class variables. Cf. tc_lhs_sig_type.
-- Importantly, this does *not* kind-generalize. Consider
-- class SC f where
-- meth :: forall a (x :: f a). Proxy x -> ()
@@ -374,21 +379,18 @@ kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
-- end up promoting kappa to the top level (because kind-generalization is
-- normally done right before adding a binding to the context), and then we
-- can't set kappa := f a, because a is local.
-kcClassSigType skol_info names (HsIB { hsib_ext = sig_vars
- , hsib_body = hs_ty })
- = addSigCtxt (funsSigCtxt names) hs_ty $
- do { (tc_lvl, wanted, (spec_tkvs, _))
- <- pushLevelAndSolveEqualitiesX "kcClassSigType" $
- bindImplicitTKBndrs_Skol sig_vars $
+kcClassSigType names
+ sig_ty@(L _ (HsSig { sig_bndrs = hs_outer_bndrs, sig_body = hs_ty }))
+ = addSigCtxt (funsSigCtxt names) sig_ty $
+ do { _ <- bindOuterSigTKBndrs_Tv hs_outer_bndrs $
tcLHsType hs_ty liftedTypeKind
+ ; return () }
- ; emitResidualTvConstraint skol_info spec_tkvs tc_lvl wanted }
-
-tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
+tcClassSigType :: [Located Name] -> LHsSigType GhcRn -> TcM Type
-- Does not do validity checking
-tcClassSigType skol_info names sig_ty
- = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
- do { (implic, ty) <- tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
+tcClassSigType names sig_ty
+ = addSigCtxt sig_ctxt sig_ty $
+ do { (implic, ty) <- tc_lhs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
; emitImplication implic
; return ty }
-- Do not zonk-to-Type, nor perform a validity check
@@ -407,20 +409,24 @@ tcClassSigType skol_info names sig_ty
-- It should be that f has kind `k2 -> *`, but we never get a chance
-- to run the solver where the kind of f is touchable. This is
-- painfully delicate.
+ where
+ sig_ctxt = funsSigCtxt names
+ skol_info = SigTypeSkol sig_ctxt
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
-- Does validity checking
-- See Note [Recipe for checking a signature]
tcHsSigType ctxt sig_ty
- = addSigCtxt ctxt (hsSigType sig_ty) $
+ = addSigCtxt ctxt sig_ty $
do { traceTc "tcHsSigType {" (ppr sig_ty)
-- Generalise here: see Note [Kind generalisation]
- ; (implic, ty) <- tc_hs_sig_type skol_info sig_ty (expectedKindInCtxt ctxt)
+ ; (implic, ty) <- tc_lhs_sig_type skol_info sig_ty (expectedKindInCtxt ctxt)
- -- Spit out the implication (and perhaps fail fast)
+ -- Float out constraints, failing fast if not possible
-- See Note [Failure in local type signatures] in GHC.Tc.Solver
- ; emitFlatConstraints (mkImplicWC (unitBag implic))
+ ; traceTc "tcHsSigType 2" (ppr implic)
+ ; simplifyAndEmitFlatConstraints (mkImplicWC (unitBag implic))
; ty <- zonkTcType ty
; checkValidType ctxt ty
@@ -429,7 +435,7 @@ tcHsSigType ctxt sig_ty
where
skol_info = SigTypeSkol ctxt
-tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
+tc_lhs_sig_type :: SkolemInfo -> LHsSigType GhcRn
-> ContextKind -> TcM (Implication, TcType)
-- Kind-checks/desugars an 'LHsSigType',
-- solve equalities,
@@ -437,25 +443,28 @@ tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
-- This will never emit constraints, as it uses solveEqualities internally.
-- No validity checking or zonking
-- Returns also an implication for the unsolved constraints
-tc_hs_sig_type skol_info hs_sig_type ctxt_kind
- | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
- = do { (tc_lvl, wanted, (spec_tkvs, ty))
- <- pushLevelAndSolveEqualitiesX "tc_hs_sig_type" $
+tc_lhs_sig_type skol_info (L loc (HsSig { sig_bndrs = hs_outer_bndrs
+ , sig_body = hs_ty })) ctxt_kind
+ = setSrcSpan loc $
+ do { (tc_lvl, wanted, (outer_bndrs, ty))
+ <- pushLevelAndSolveEqualitiesX "tc_lhs_sig_type" $
-- See Note [Failure in local type signatures]
- bindImplicitTKBndrs_Skol sig_vars $
+ tcOuterTKBndrs skol_info hs_outer_bndrs $
do { kind <- newExpectedKind ctxt_kind
; tcLHsType hs_ty kind }
-- Any remaining variables (unsolved in the solveEqualities)
-- should be in the global tyvars, and therefore won't be quantified
- ; spec_tkvs <- zonkAndScopedSort spec_tkvs
- ; let ty1 = mkSpecForAllTys spec_tkvs ty
+ ; traceTc "tc_lhs_sig_type" (ppr hs_outer_bndrs $$ ppr outer_bndrs)
+ ; (outer_tv_bndrs :: [InvisTVBinder]) <- scopedSortOuter outer_bndrs
+
+ ; let ty1 = mkInvisForAllTys outer_tv_bndrs ty
; kvs <- kindGeneralizeSome wanted ty1
-- Build an implication for any as-yet-unsolved kind equalities
-- See Note [Skolem escape in type signatures]
- ; implic <- buildTvImplication skol_info (kvs ++ spec_tkvs) tc_lvl wanted
+ ; implic <- buildTvImplication skol_info kvs tc_lvl wanted
; return (implic, mkInfForAllTys kvs ty1) }
@@ -466,23 +475,24 @@ tcHsSigType is tricky. Consider (T11142)
This is ill-kinded becuase of a nested skolem-escape.
That will show up as an un-solvable constraint in the implication
-returned by buildTvImplication in tc_hs_sig_type. See Note [Skolem
+returned by buildTvImplication in tc_lhs_sig_type. See Note [Skolem
escape prevention] in GHC.Tc.Utils.TcType for why it is unsolvable
(the unification variable for b's kind is untouchable).
-Then, in GHC.Tc.Solver.emitFlatConstraints (called from tcHsSigType)
+Then, in GHC.Tc.Solver.simplifyAndEmitFlatConstraints (called from tcHsSigType)
we'll try to float out the constraint, be unable to do so, and fail.
See GHC.Tc.Solver Note [Failure in local type signatures] for more
detail on this.
-The separation between tcHsSigType and tc_hs_sig_type is because
+The separation between tcHsSigType and tc_lhs_sig_type is because
tcClassSigType wants to use the latter, but *not* fail fast, because
there are skolems from the class decl which are in scope; but it's fine
not to because tcClassDecl1 has a solveEqualities wrapped around all
the tcClassSigType calls.
-That's why tcHsSigType does emitFlatConstraints (which fails fast) but
-tcClassSigType just does emitImplication (which does not). Ugh.
+That's why tcHsSigType does simplifyAndEmitFlatConstraints (which
+fails fast) but tcClassSigType just does emitImplication (which does
+not). Ugh.
c.f. see also Note [Skolem escape and forall-types]. The difference
is that we don't need to simplify at a forall type, only at the
@@ -491,45 +501,46 @@ top level of a signature.
-- Does validity checking and zonking.
tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind)
-tcStandaloneKindSig (L _ kisig) = case kisig of
- StandaloneKindSig _ (L _ name) ksig ->
- let ctxt = StandaloneKindSigCtxt name in
- addSigCtxt ctxt (hsSigType ksig) $
- do { let mode = mkMode KindLevel
- ; kind <- tc_top_lhs_type mode ksig (expectedKindInCtxt ctxt)
+tcStandaloneKindSig (L _ (StandaloneKindSig _ (L _ name) ksig))
+ = addSigCtxt ctxt ksig $
+ do { kind <- tc_top_lhs_type KindLevel ctxt ksig
; checkValidType ctxt kind
; return (name, kind) }
+ where
+ ctxt = StandaloneKindSigCtxt name
+tcTopLHsType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
+tcTopLHsType ctxt lsig_ty
+ = tc_top_lhs_type TypeLevel ctxt lsig_ty
-tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
-tcTopLHsType hs_ty ctxt_kind
- = tc_top_lhs_type (mkMode TypeLevel) hs_ty ctxt_kind
-
-tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
--- tcTopLHsType is used for kind-checking top-level HsType where
+tc_top_lhs_type :: TypeOrKind -> UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
+-- tc_top_lhs_type is used for kind-checking top-level LHsSigTypes where
-- we want to fully solve /all/ equalities, and report errors
-- Does zonking, but not validity checking because it's used
-- for things (like deriving and instances) that aren't
-- ordinary types
-- Used for both types and kinds
-tc_top_lhs_type mode hs_sig_type ctxt_kind
- | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
- = do { traceTc "tcTopLHsType {" (ppr hs_ty)
- ; (tclvl, wanted, (spec_tkvs, ty))
- <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
- bindImplicitTKBndrs_Skol sig_vars $
- do { kind <- newExpectedKind ctxt_kind
- ; tc_lhs_type mode hs_ty kind }
-
- ; spec_tkvs <- zonkAndScopedSort spec_tkvs
- ; reportUnsolvedEqualities InstSkol spec_tkvs tclvl wanted
-
- ; let ty1 = mkSpecForAllTys spec_tkvs ty
- ; kvs <- kindGeneralizeAll ty1
+tc_top_lhs_type tyki ctxt (L loc sig_ty@(HsSig { sig_bndrs = hs_outer_bndrs
+ , sig_body = body }))
+ = setSrcSpan loc $
+ do { traceTc "tc_top_lhs_type {" (ppr sig_ty)
+ ; (tclvl, wanted, (outer_bndrs, ty))
+ <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
+ tcOuterTKBndrs skol_info hs_outer_bndrs $
+ do { kind <- newExpectedKind (expectedKindInCtxt ctxt)
+ ; tc_lhs_type (mkMode tyki) body kind }
+
+ ; outer_tv_bndrs <- scopedSortOuter outer_bndrs
+ ; let ty1 = mkInvisForAllTys outer_tv_bndrs ty
+
+ ; kvs <- kindGeneralizeAll ty1 -- "All" because it's a top-level type
+ ; reportUnsolvedEqualities skol_info kvs tclvl wanted
; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)
- ; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty])
- ; return final_ty}
+ ; traceTc "tc_top_lhs_type }" (vcat [ppr sig_ty, ppr final_ty])
+ ; return final_ty }
+ where
+ skol_info = SigTypeSkol ctxt
-----------------
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
@@ -542,7 +553,7 @@ tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
tcHsDeriv hs_ty
= do { ty <- checkNoErrs $ -- Avoid redundant error report
-- with "illegal deriving", below
- tcTopLHsType hs_ty AnyKind
+ tcTopLHsType DerivClauseCtxt hs_ty
; let (tvs, pred) = splitForAllTys ty
(kind_args, _) = splitFunTys (tcTypeKind pred)
; case getClassPredTys_maybe pred of
@@ -571,7 +582,7 @@ tcDerivStrategy mb_lds
tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy
tc_deriv_strategy NewtypeStrategy = boring_case NewtypeStrategy
tc_deriv_strategy (ViaStrategy ty) = do
- ty' <- checkNoErrs $ tcTopLHsType ty AnyKind
+ ty' <- checkNoErrs $ tcTopLHsType DerivClauseCtxt ty
let (via_tvs, via_pred) = splitForAllTys ty'
pure (ViaStrategy via_pred, via_tvs)
@@ -583,13 +594,13 @@ tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
-> TcM Type
-- Like tcHsSigType, but for a class instance declaration
tcHsClsInstType user_ctxt hs_inst_ty
- = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
+ = setSrcSpan (getLoc hs_inst_ty) $
do { -- Fail eagerly if tcTopLHsType fails. We are at top level so
-- these constraints will never be solved later. And failing
-- eagerly avoids follow-on errors when checkValidInstance
-- sees an unsolved coercion hole
inst_ty <- checkNoErrs $
- tcTopLHsType hs_inst_ty (TheKind constraintKind)
+ tcTopLHsType user_ctxt hs_inst_ty
; checkValidInstance user_ctxt hs_inst_ty inst_ty
; return inst_ty }
@@ -605,7 +616,7 @@ tcHsTypeApp wc_ty kind
solveEqualities "tcHsTypeApp" $
-- We are looking at a user-written type, very like a
-- signature so we want to solve its equalities right now
- tcNamedWildCardBinders sig_wcs $ \ _ ->
+ bindNamedWildCardBinders sig_wcs $ \ _ ->
tc_lhs_type mode hs_ty kind
-- We do not kind-generalize type applications: we just
@@ -713,7 +724,7 @@ tcInferLHsTypeKind :: LHsType GhcRn -> TcM (TcType, TcKind)
tcInferLHsTypeKind lhs_ty@(L loc hs_ty)
= addTypeCtxt lhs_ty $
setSrcSpan loc $ -- Cover the tcInstInvisibleTyBinders
- do { (res_ty, res_kind) <- tc_infer_hs_type (mkMode TypeLevel) hs_ty
+ do { (res_ty, res_kind) <- tc_infer_hs_type typeLevelMode hs_ty
; tcInstInvisibleTyBinders res_ty res_kind }
-- See Note [Do not always instantiate eagerly in types]
@@ -783,7 +794,7 @@ concern things that the renamer can't handle.
-}
tcMult :: HsArrow GhcRn -> TcM Mult
-tcMult hc = tc_mult (mkMode TypeLevel) hc
+tcMult hc = tc_mult typeLevelMode hc
-- | Info about the context in which we're checking a type. Currently,
-- differentiates only between types and kinds, but this will likely
@@ -795,11 +806,11 @@ tcMult hc = tc_mult (mkMode TypeLevel) hc
-- This data type is purely local, not exported from this module
data TcTyMode
= TcTyMode { mode_tyki :: TypeOrKind
+ , mode_holes :: HoleInfo }
- -- See Note [Levels for wildcards]
- -- Nothing <=> no wildcards expected
- , mode_holes :: Maybe (TcLevel, HoleMode)
- }
+-- See Note [Levels for wildcards]
+-- Nothing <=> no wildcards expected
+type HoleInfo = Maybe (TcLevel, HoleMode)
-- HoleMode says how to treat the occurrences
-- of anonymous wildcards; see tcAnonWildCardOcc
@@ -812,15 +823,17 @@ data HoleMode = HM_Sig -- Partial type signatures: f :: _ -> Int
mkMode :: TypeOrKind -> TcTyMode
mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing }
+typeLevelMode, kindLevelMode :: TcTyMode
+-- These modes expect no wildcards (holes) in the type
+kindLevelMode = mkMode KindLevel
+typeLevelMode = mkMode TypeLevel
+
mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode tyki hm
= do { lvl <- getTcLevel
; return (TcTyMode { mode_tyki = tyki
, mode_holes = Just (lvl,hm) }) }
-kindLevel :: TcTyMode -> TcTyMode
-kindLevel mode = mode { mode_tyki = KindLevel }
-
instance Outputable HoleMode where
ppr HM_Sig = text "HM_Sig"
ppr HM_FamPat = text "HM_FamPat"
@@ -997,7 +1010,7 @@ substitution to each NHsCoreTy and all is well:
------------------------------------------
tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType
tcLHsType hs_ty exp_kind
- = tc_lhs_type (mkMode TypeLevel) hs_ty exp_kind
+ = tc_lhs_type typeLevelMode hs_ty exp_kind
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
tc_lhs_type mode (L span ty) exp_kind
@@ -1049,32 +1062,16 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
= tc_fun_type mode (HsUnrestrictedArrow NormalSyntax) ty1 ty2 exp_kind
--------- Foralls
-tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
- = do { (tclvl, wanted, (tv_bndrs, ty'))
- <- pushLevelAndCaptureConstraints $
- -- No need to solve equalities here; we will do that later
- bindExplicitTKTele_Skol_M mode tele $
- -- The _M variant passes on the mode from the type, to
- -- any wildards in kind signatures on the forall'd variables
+tc_hs_type mode (HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
+ = do { (tv_bndrs, ty') <- tcTKTelescope mode tele $
+ tc_lhs_type mode ty exp_kind
+ -- Pass on the mode from the type, to any wildcards
+ -- in kind signatures on the forall'd variables
-- e.g. f :: _ -> Int -> forall (a :: _). blah
- tc_lhs_type mode ty exp_kind
-- Why exp_kind? See Note [Body kind of HsForAllTy]
-- Do not kind-generalise here! See Note [Kind generalisation]
- ; let skol_info = ForAllSkol (ppr forall) $ sep $ case tele of
- HsForAllVis { hsf_vis_bndrs = hs_tvs } ->
- map ppr hs_tvs
- HsForAllInvis { hsf_invis_bndrs = hs_tvs } ->
- map ppr hs_tvs
- skol_tvs = binderVars tv_bndrs
-
- ; implic <- buildTvImplication skol_info skol_tvs tclvl wanted
- ; emitImplication implic
- -- /Always/ emit this implication even if wanted is empty
- -- We need the implication so that we check for a bad telescope
- -- See Note [Skolem escape and forall-types]
-
; return (mkForAllTys tv_bndrs ty') }
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
@@ -1824,10 +1821,10 @@ tcHsMbContext Nothing = return []
tcHsMbContext (Just cxt) = tcHsContext cxt
tcHsContext :: LHsContext GhcRn -> TcM [PredType]
-tcHsContext cxt = tc_hs_context (mkMode TypeLevel) cxt
+tcHsContext cxt = tc_hs_context typeLevelMode cxt
tcLHsPredType :: LHsType GhcRn -> TcM PredType
-tcLHsPredType pred = tc_lhs_pred (mkMode TypeLevel) pred
+tcLHsPredType pred = tc_lhs_pred typeLevelMode pred
tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
@@ -2051,13 +2048,13 @@ addTypeCtxt (L _ ty) thing
* *
********************************************************************* -}
-tcNamedWildCardBinders :: [Name]
- -> ([(Name, TcTyVar)] -> TcM a)
- -> TcM a
+bindNamedWildCardBinders :: [Name]
+ -> ([(Name, TcTyVar)] -> TcM a)
+ -> TcM a
-- Bring into scope the /named/ wildcard binders. Remember that
-- plain wildcards _ are anonymous and dealt with by HsWildCardTy
-- Soe Note [The wildcard story for types] in GHC.Hs.Type
-tcNamedWildCardBinders wc_names thing_inside
+bindNamedWildCardBinders wc_names thing_inside
= do { wcs <- mapM newNamedWildTyVar wc_names
; let wc_prs = wc_names `zip` wcs
; tcExtendNameTyVarEnv wc_prs $
@@ -2351,7 +2348,7 @@ kcInferDeclHeader name flav
all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
-- NB: bindExplicitTKBndrs_Q_Tv does not clone;
-- ditto Implicit
- -- See Note [Non-cloning for tyvar binders]
+ -- See Note [Cloning for type variable binders]
tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
False -- not yet generalised
@@ -2897,6 +2894,7 @@ expectedKindInCtxt (GhciCtxt {}) = AnyKind
-- The types in a 'default' decl can have varying kinds
-- See Note [Extended defaults]" in GHC.Tc.Utils.Env
expectedKindInCtxt DefaultDeclCtxt = AnyKind
+expectedKindInCtxt DerivClauseCtxt = AnyKind
expectedKindInCtxt TypeAppCtxt = AnyKind
expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind
expectedKindInCtxt (InstDeclCtxt {}) = TheKind constraintKind
@@ -2910,228 +2908,411 @@ expectedKindInCtxt _ = OpenKind
* *
********************************************************************* -}
-{- Note [Non-cloning for tyvar binders]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-bindExplictTKBndrs_Q_Skol, bindExplictTKBndrs_Skol, do not clone;
-and nor do the Implicit versions. There is no need.
-
-bindExplictTKBndrs_Q_Tv does not clone; and similarly Implicit.
-We take advantage of this in kcInferDeclHeader:
- all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
-If we cloned, we'd need to take a bit more care here; not hard.
-
-The main payoff is that avoidng gratuitious cloning means that we can
-almost always take the fast path in swizzleTcTyConBndrs. "Almost
-always" means not the case of mutual recursion with polymorphic kinds.
-
-
-Note [Cloning for tyvar binders]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-bindExplicitTKBndrs_Tv does cloning, making up a Name with a fresh Unique,
-unlike bindExplicitTKBndrs_Q_Tv. (Nor do the Skol variants clone.)
-And similarly for bindImplicit...
-
-This for a narrow and tricky reason which, alas, I couldn't find a
-simpler way round. #16221 is the poster child:
-
- data SameKind :: k -> k -> *
- data T a = forall k2 (b :: k2). MkT (SameKind a b) !Int
-
-When kind-checking T, we give (a :: kappa1). Then:
-
-- In kcConDecl we make a TyVarTv unification variable kappa2 for k2
- (as described in Note [Kind-checking for GADTs], even though this
- example is an existential)
-- So we get (b :: kappa2) via bindExplicitTKBndrs_Tv
-- We end up unifying kappa1 := kappa2, because of the (SameKind a b)
-
-Now we generalise over kappa2. But if kappa2's Name is precisely k2
-(i.e. we did not clone) we'll end up giving T the utterlly final kind
- T :: forall k2. k2 -> *
-Nothing directly wrong with that but when we typecheck the data constructor
-we have k2 in scope; but then it's brought into scope /again/ when we find
-the forall k2. This is chaotic, and we end up giving it the type
- MkT :: forall k2 (a :: k2) k2 (b :: k2).
- SameKind @k2 a b -> Int -> T @{k2} a
-which is bogus -- because of the shadowing of k2, we can't
-apply T to the kind or a!
-
-And there no reason /not/ to clone the Name when making a unification
-variable. So that's what we do.
--}
-
---------------------------------------
--- Implicit binders
---------------------------------------
-
-bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv,
- bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv
- :: [Name] -> TcM a -> TcM ([TcTyVar], a)
-bindImplicitTKBndrs_Q_Skol = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedSkolemTyVar)
-bindImplicitTKBndrs_Q_Tv = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedTyVarTyVar)
-bindImplicitTKBndrs_Skol = bindImplicitTKBndrsX newFlexiKindedSkolemTyVar
-bindImplicitTKBndrs_Tv = bindImplicitTKBndrsX cloneFlexiKindedTyVarTyVar
- -- newFlexiKinded... see Note [Non-cloning for tyvar binders]
- -- cloneFlexiKindedTyVarTyVar: see Note [Cloning for tyvar binders]
-
-bindImplicitTKBndrsX
- :: (Name -> TcM TcTyVar) -- new_tv function
- -> [Name]
- -> TcM a
- -> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
- -- with the passed in [Name]
-bindImplicitTKBndrsX new_tv tv_names thing_inside
- = do { tkvs <- mapM new_tv tv_names
- ; traceTc "bindImplicitTKBndrs" (ppr tv_names $$ ppr tkvs)
- ; res <- tcExtendNameTyVarEnv (tv_names `zip` tkvs)
- thing_inside
- ; return (tkvs, res) }
-
-newImplicitTyVarQ :: (Name -> TcM TcTyVar) -> Name -> TcM TcTyVar
--- Behave like new_tv, except that if the tyvar is in scope, use it
-newImplicitTyVarQ new_tv name
- = do { mb_tv <- tcLookupLcl_maybe name
- ; case mb_tv of
- Just (ATyVar _ tv) -> return tv
- _ -> new_tv name }
-
-newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar
-newFlexiKindedTyVar new_tv name
- = do { kind <- newMetaKindVar
- ; new_tv name kind }
-
-newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
-newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
-
-newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
-newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
-
-cloneFlexiKindedTyVarTyVar :: Name -> TcM TyVar
-cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar
- -- See Note [Cloning for tyvar binders]
-
--------------------------------------
--- Explicit binders
+-- HsForAllTelescope
--------------------------------------
--- | Skolemise the 'HsTyVarBndr's in an 'LHsForAllTelescope.
-bindExplicitTKTele_Skol_M
- :: TcTyMode
- -> HsForAllTelescope GhcRn
- -> TcM a
- -> TcM ([TcTyVarBinder], a)
-bindExplicitTKTele_Skol_M mode tele thing_inside = case tele of
+tcTKTelescope :: TcTyMode
+ -> HsForAllTelescope GhcRn
+ -> TcM a
+ -> TcM ([TcTyVarBinder], a)
+tcTKTelescope mode tele thing_inside = case tele of
HsForAllVis { hsf_vis_bndrs = bndrs }
- -> do { (req_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside
+ -> do { (req_tv_bndrs, thing) <- tcExplicitTKBndrsX skol_mode bndrs thing_inside
-- req_tv_bndrs :: [VarBndr TyVar ()],
-- but we want [VarBndr TyVar ArgFlag]
; return (tyVarReqToBinders req_tv_bndrs, thing) }
+
HsForAllInvis { hsf_invis_bndrs = bndrs }
- -> do { (inv_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside
+ -> do { (inv_tv_bndrs, thing) <- tcExplicitTKBndrsX skol_mode bndrs thing_inside
-- inv_tv_bndrs :: [VarBndr TyVar Specificity],
-- but we want [VarBndr TyVar ArgFlag]
; return (tyVarSpecToBinders inv_tv_bndrs, thing) }
+ where
+ skol_mode = smVanilla { sm_clone = False, sm_holes = mode_holes mode }
+
+--------------------------------------
+-- HsOuterTyVarBndrs
+--------------------------------------
+
+bindOuterTKBndrsX :: OutputableBndrFlag flag
+ => SkolemMode
+ -> HsOuterTyVarBndrs flag GhcRn
+ -> TcM a
+ -> TcM (HsOuterTyVarBndrs flag GhcTc, a)
+bindOuterTKBndrsX skol_mode outer_bndrs thing_inside
+ = case outer_bndrs of
+ HsOuterImplicit{hso_ximplicit = imp_tvs} ->
+ do { (imp_tvs', thing) <- bindImplicitTKBndrsX skol_mode imp_tvs thing_inside
+ ; return ( HsOuterImplicit{hso_ximplicit = imp_tvs'}
+ , thing) }
+ HsOuterExplicit{hso_bndrs = exp_bndrs} ->
+ do { (exp_tvs', thing) <- bindExplicitTKBndrsX skol_mode exp_bndrs thing_inside
+ ; return ( HsOuterExplicit { hso_xexplicit = exp_tvs'
+ , hso_bndrs = exp_bndrs }
+ , thing) }
+
+getOuterTyVars :: HsOuterTyVarBndrs flag GhcTc -> [TcTyVar]
+-- The returned [TcTyVar] is not necessarily in dependency order
+-- at least for the HsOuterImplicit case
+getOuterTyVars (HsOuterImplicit { hso_ximplicit = tvs }) = tvs
+getOuterTyVars (HsOuterExplicit { hso_xexplicit = tvbs }) = binderVars tvbs
+
+---------------
+scopedSortOuter :: HsOuterTyVarBndrs Specificity GhcTc -> TcM [InvisTVBinder]
+-- Sort any /implicit/ binders into dependency order
+-- (zonking first so we can see the dependencies)
+-- /Explicit/ ones are already in the right order
+scopedSortOuter (HsOuterImplicit{hso_ximplicit = imp_tvs})
+ = do { imp_tvs <- zonkAndScopedSort imp_tvs
+ ; return [Bndr tv SpecifiedSpec | tv <- imp_tvs] }
+scopedSortOuter (HsOuterExplicit{hso_xexplicit = exp_tvs})
+ = -- No need to dependency-sort (or zonk) explicit quantifiers
+ return exp_tvs
+
+---------------
+bindOuterSigTKBndrs_Tv :: HsOuterSigTyVarBndrs GhcRn
+ -> TcM a -> TcM (HsOuterSigTyVarBndrs GhcTc, a)
+bindOuterSigTKBndrs_Tv
+ = bindOuterTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True })
+
+bindOuterSigTKBndrs_Tv_M :: TcTyMode
+ -> HsOuterSigTyVarBndrs GhcRn
+ -> TcM a -> TcM (HsOuterSigTyVarBndrs GhcTc, a)
+-- Do not push level; do not make implication constraint; use Tvs
+-- Two major clients of this "bind-only" path are:
+-- Note [Kind-checking for GADTs] in TyCl
+-- Note [Checking partial type signatures]
+bindOuterSigTKBndrs_Tv_M mode
+ = bindOuterTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True
+ , sm_holes = mode_holes mode })
+
+bindOuterFamEqnTKBndrs_Q_Tv :: HsOuterFamEqnTyVarBndrs GhcRn
+ -> TcM a
+ -> TcM ([TcTyVar], a)
+bindOuterFamEqnTKBndrs_Q_Tv hs_bndrs thing_inside
+ = liftFstM getOuterTyVars $
+ bindOuterTKBndrsX (smVanilla { sm_clone = False, sm_parent = True
+ , sm_tvtv = True })
+ hs_bndrs thing_inside
+ -- sm_clone=False: see Note [Cloning for type variable binders]
+
+bindOuterFamEqnTKBndrs :: HsOuterFamEqnTyVarBndrs GhcRn
+ -> TcM a
+ -> TcM ([TcTyVar], a)
+bindOuterFamEqnTKBndrs hs_bndrs thing_inside
+ = liftFstM getOuterTyVars $
+ bindOuterTKBndrsX (smVanilla { sm_clone = False, sm_parent = True })
+ hs_bndrs thing_inside
+ -- sm_clone=False: see Note [Cloning for type variable binders]
+
+---------------
+tcOuterTKBndrs :: OutputableBndrFlag flag
+ => SkolemInfo
+ -> HsOuterTyVarBndrs flag GhcRn
+ -> TcM a -> TcM (HsOuterTyVarBndrs flag GhcTc, a)
+tcOuterTKBndrs = tcOuterTKBndrsX (smVanilla { sm_clone = False })
+ -- Do not clone the outer binders
+ -- See Note [Cloning for type variable binder] under "must not"
+
+tcOuterTKBndrsX :: OutputableBndrFlag flag
+ => SkolemMode -> SkolemInfo
+ -> HsOuterTyVarBndrs flag GhcRn
+ -> TcM a -> TcM (HsOuterTyVarBndrs flag GhcTc, a)
+-- Push level, capture constraints, make implication
+tcOuterTKBndrsX skol_mode skol_info outer_bndrs thing_inside
+ = case outer_bndrs of
+ HsOuterImplicit{hso_ximplicit = imp_tvs} ->
+ do { (imp_tvs', thing) <- tcImplicitTKBndrsX skol_mode skol_info imp_tvs thing_inside
+ ; return ( HsOuterImplicit{hso_ximplicit = imp_tvs'}
+ , thing) }
+ HsOuterExplicit{hso_bndrs = exp_bndrs} ->
+ do { (exp_tvs', thing) <- tcExplicitTKBndrsX skol_mode exp_bndrs thing_inside
+ ; return ( HsOuterExplicit { hso_xexplicit = exp_tvs'
+ , hso_bndrs = exp_bndrs }
+ , thing) }
+--------------------------------------
+-- Explicit tyvar binders
+--------------------------------------
+
+tcExplicitTKBndrs :: OutputableBndrFlag flag
+ => [LHsTyVarBndr flag GhcRn]
+ -> TcM a
+ -> TcM ([VarBndr TyVar flag], a)
+tcExplicitTKBndrs = tcExplicitTKBndrsX (smVanilla { sm_clone = True })
+
+tcExplicitTKBndrsX :: OutputableBndrFlag flag
+ => SkolemMode
+ -> [LHsTyVarBndr flag GhcRn]
+ -> TcM a
+ -> TcM ([VarBndr TyVar flag], a)
+-- Push level, capture constraints,
+-- and emit an implication constraint with a ForAllSkol ic_info,
+-- so that it is subject to a telescope test.
+tcExplicitTKBndrsX skol_mode bndrs thing_inside
+ = do { (tclvl, wanted, (skol_tvs, res))
+ <- pushLevelAndCaptureConstraints $
+ bindExplicitTKBndrsX skol_mode bndrs $
+ thing_inside
+
+ ; let skol_info = ForAllSkol (fsep (map ppr bndrs))
+ -- Notice that we use ForAllSkol here, ignoring the enclosing
+ -- skol_info unlike tc_implicit_tk_bndrs, because the bad-telescope
+ -- test applies only to ForAllSkol
+ ; emitResidualTvConstraint skol_info (binderVars skol_tvs) tclvl wanted
+
+ ; return (skol_tvs, res) }
+
+----------------
+-- | Skolemise the 'HsTyVarBndr's in an 'HsForAllTelescope' with the supplied
+-- 'TcTyMode'.
bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
:: (OutputableBndrFlag flag)
=> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TyVar flag], a)
-bindExplicitTKBndrs_Skol_M, bindExplicitTKBndrs_Tv_M
- :: (OutputableBndrFlag flag)
- => TcTyMode
- -> [LHsTyVarBndr flag GhcRn]
- -> TcM a
- -> TcM ([VarBndr TyVar flag], a)
-
-bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) newSkolemTyVar)
-bindExplicitTKBndrs_Skol_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) newSkolemTyVar)
-bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) cloneTyVarTyVar)
-bindExplicitTKBndrs_Tv_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) cloneTyVarTyVar)
- -- newSkolemTyVar: see Note [Non-cloning for tyvar binders]
- -- cloneTyVarTyVar: see Note [Cloning for tyvar binders]
+bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (smVanilla { sm_clone = False })
+bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True })
+ -- sm_clone: see Note [Cloning for type variable binders]
bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv
:: ContextKind
-> [LHsTyVarBndr () GhcRn]
-> TcM a
-> TcM ([TcTyVar], a)
-
-bindExplicitTKBndrs_Q_Skol ctxt_kind = bindExplicitTKBndrsX_Q (tcHsQTyVarBndr ctxt_kind newSkolemTyVar)
-bindExplicitTKBndrs_Q_Tv ctxt_kind = bindExplicitTKBndrsX_Q (tcHsQTyVarBndr ctxt_kind newTyVarTyVar)
- -- See Note [Non-cloning for tyvar binders]
-
-bindExplicitTKBndrsX_Q
- :: (HsTyVarBndr () GhcRn -> TcM TcTyVar)
- -> [LHsTyVarBndr () GhcRn]
- -> TcM a
- -> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
- -- with the passed-in [LHsTyVarBndr]
-bindExplicitTKBndrsX_Q tc_tv hs_tvs thing_inside
- = do { (tv_bndrs,res) <- bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
- ; return (binderVars tv_bndrs,res) }
+-- These do not clone: see Note [Cloning for type variable binders]
+bindExplicitTKBndrs_Q_Skol ctxt_kind hs_bndrs thing_inside
+ = liftFstM binderVars $
+ bindExplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True
+ , sm_kind = ctxt_kind })
+ hs_bndrs thing_inside
+ -- sm_clone=False: see Note [Cloning for type variable binders]
+
+bindExplicitTKBndrs_Q_Tv ctxt_kind hs_bndrs thing_inside
+ = liftFstM binderVars $
+ bindExplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True
+ , sm_tvtv = True, sm_kind = ctxt_kind })
+ hs_bndrs thing_inside
+ -- sm_clone=False: see Note [Cloning for type variable binders]
bindExplicitTKBndrsX :: (OutputableBndrFlag flag)
- => (HsTyVarBndr flag GhcRn -> TcM TyVar)
+ => SkolemMode
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TyVar flag], a) -- Returned [TcTyVar] are in 1-1 correspondence
-- with the passed-in [LHsTyVarBndr]
-bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
- = do { traceTc "bindExplicTKBndrs" (ppr hs_tvs)
+bindExplicitTKBndrsX skol_mode@(SM { sm_parent = check_parent, sm_kind = ctxt_kind
+ , sm_holes = hole_info })
+ hs_tvs thing_inside
+ = do { traceTc "bindExplicitTKBndrs" (ppr hs_tvs)
; go hs_tvs }
where
+ tc_ki_mode = TcTyMode { mode_tyki = KindLevel, mode_holes = hole_info }
+ -- Inherit the HoleInfo from the context
+
go [] = do { res <- thing_inside
; return ([], res) }
go (L _ hs_tv : hs_tvs)
- = do { tv <- tc_tv hs_tv
+ = do { lcl_env <- getLclTypeEnv
+ ; tv <- tc_hs_bndr lcl_env hs_tv
-- Extend the environment as we go, in case a binder
-- is mentioned in the kind of a later binder
-- e.g. forall k (a::k). blah
-- NB: tv's Name may differ from hs_tv's
- -- See GHC.Tc.Utils.TcMType Note [Cloning for tyvar binders]
+ -- See Note [Cloning for type variable binders]
; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
go hs_tvs
; return (Bndr tv (hsTyVarBndrFlag hs_tv):tvs, res) }
------------------
-tcHsTyVarBndr :: TcTyMode -> (Name -> Kind -> TcM TyVar)
- -> HsTyVarBndr flag GhcRn -> TcM TcTyVar
-tcHsTyVarBndr _ new_tv (UserTyVar _ _ (L _ tv_nm))
- = do { kind <- newMetaKindVar
- ; new_tv tv_nm kind }
-tcHsTyVarBndr mode new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind)
- = do { kind <- tc_lhs_kind_sig mode (TyVarBndrKindCtxt tv_nm) lhs_kind
- ; new_tv tv_nm kind }
------------------
-tcHsQTyVarBndr :: ContextKind
- -> (Name -> Kind -> TcM TyVar)
- -> HsTyVarBndr () GhcRn -> TcM TcTyVar
--- Just like tcHsTyVarBndr, but also
--- - uses the in-scope TyVar from class, if it exists
--- - takes a ContextKind to use for the no-sig case
-tcHsQTyVarBndr ctxt_kind new_tv (UserTyVar _ _ (L _ tv_nm))
- = do { mb_tv <- tcLookupLcl_maybe tv_nm
- ; case mb_tv of
- Just (ATyVar _ tv) -> return tv
- _ -> do { kind <- newExpectedKind ctxt_kind
- ; new_tv tv_nm kind } }
-
-tcHsQTyVarBndr _ new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind)
- = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
- ; mb_tv <- tcLookupLcl_maybe tv_nm
- ; case mb_tv of
- Just (ATyVar _ tv)
- -> do { discardResult $ unifyKind (Just (ppr tv_nm))
- kind (tyVarKind tv)
- -- This unify rejects:
- -- class C (m :: * -> *) where
- -- type F (m :: *) = ...
- ; return tv }
-
- _ -> new_tv tv_nm kind }
+ tc_hs_bndr lcl_env (UserTyVar _ _ (L _ name))
+ | check_parent
+ , Just (ATyVar _ tv) <- lookupNameEnv lcl_env name
+ = return tv
+ | otherwise
+ = do { kind <- newExpectedKind ctxt_kind
+ ; newTyVarBndr skol_mode name kind }
+
+ tc_hs_bndr lcl_env (KindedTyVar _ _ (L _ name) lhs_kind)
+ | check_parent
+ , Just (ATyVar _ tv) <- lookupNameEnv lcl_env name
+ = do { kind <- tc_lhs_kind_sig tc_ki_mode (TyVarBndrKindCtxt name) lhs_kind
+ ; discardResult $
+ unifyKind (Just (ppr name)) kind (tyVarKind tv)
+ -- This unify rejects:
+ -- class C (m :: * -> *) where
+ -- type F (m :: *) = ...
+ ; return tv }
+
+ | otherwise
+ = do { kind <- tc_lhs_kind_sig tc_ki_mode (TyVarBndrKindCtxt name) lhs_kind
+ ; newTyVarBndr skol_mode name kind }
+
+newTyVarBndr :: SkolemMode -> Name -> Kind -> TcM TcTyVar
+newTyVarBndr (SM { sm_clone = clone, sm_tvtv = tvtv }) name kind
+ = do { name <- case clone of
+ True -> do { uniq <- newUnique
+ ; return (setNameUnique name uniq) }
+ False -> return name
+ ; details <- case tvtv of
+ True -> newMetaDetails TyVarTv
+ False -> do { lvl <- getTcLevel
+ ; return (SkolemTv lvl False) }
+ ; return (mkTcTyVar name kind details) }
+
+--------------------------------------
+-- Implicit tyvar binders
+--------------------------------------
+
+tcImplicitTKBndrsX :: SkolemMode -> SkolemInfo
+ -> [Name]
+ -> TcM a
+ -> TcM ([TcTyVar], a)
+-- The workhorse:
+-- push level, capture constraints,
+-- and emit an implication constraint with a ForAllSkol ic_info,
+-- so that it is subject to a telescope test.
+tcImplicitTKBndrsX skol_mode skol_info bndrs thing_inside
+ = do { (tclvl, wanted, (skol_tvs, res))
+ <- pushLevelAndCaptureConstraints $
+ bindImplicitTKBndrsX skol_mode bndrs $
+ thing_inside
+
+ ; emitResidualTvConstraint skol_info skol_tvs tclvl wanted
+
+ ; return (skol_tvs, res) }
+
+------------------
+bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv,
+ bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv
+ :: [Name] -> TcM a -> TcM ([TcTyVar], a)
+bindImplicitTKBndrs_Skol = bindImplicitTKBndrsX (smVanilla { sm_clone = True })
+bindImplicitTKBndrs_Tv = bindImplicitTKBndrsX (smVanilla { sm_clone = True, sm_tvtv = True })
+bindImplicitTKBndrs_Q_Skol = bindImplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True })
+bindImplicitTKBndrs_Q_Tv = bindImplicitTKBndrsX (smVanilla { sm_clone = False, sm_parent = True, sm_tvtv = True })
+
+bindImplicitTKBndrsX
+ :: SkolemMode
+ -> [Name]
+ -> TcM a
+ -> TcM ([TcTyVar], a) -- Returned [TcTyVar] are in 1-1 correspondence
+ -- with the passed in [Name]
+bindImplicitTKBndrsX skol_mode@(SM { sm_parent = check_parent, sm_kind = ctxt_kind })
+ tv_names thing_inside
+ = do { lcl_env <- getLclTypeEnv
+ ; tkvs <- mapM (new_tv lcl_env) tv_names
+ ; traceTc "bindImplicitTKBndrsX" (ppr tv_names $$ ppr tkvs)
+ ; res <- tcExtendNameTyVarEnv (tv_names `zip` tkvs)
+ thing_inside
+ ; return (tkvs, res) }
+ where
+ new_tv lcl_env name
+ | check_parent
+ , Just (ATyVar _ tv) <- lookupNameEnv lcl_env name
+ = return tv
+ | otherwise
+ = do { kind <- newExpectedKind ctxt_kind
+ ; newTyVarBndr skol_mode name kind }
+
+--------------------------------------
+-- SkolemMode
+--------------------------------------
+
+-- | 'SkolemMode' decribes how to typecheck an explicit ('HsTyVarBndr') or
+-- implicit ('Name') binder in a type. It is just a record of flags
+-- that describe what sort of 'TcTyVar' to create.
+data SkolemMode
+ = SM { sm_parent :: Bool -- True <=> check the in-scope parent type variable
+ -- Used only for asssociated types
+
+ , sm_clone :: Bool -- True <=> fresh unique
+ -- See Note [Cloning for type variable binders]
+
+ , sm_tvtv :: Bool -- True <=> use a TyVarTv, rather than SkolemTv
+ -- Why? See Note [Inferring kinds for type declarations]
+ -- in GHC.Tc.TyCl, and (in this module)
+ -- Note [Checking partial type signatures]
+
+ , sm_kind :: ContextKind -- Use this for the kind of any new binders
+
+ , sm_holes :: HoleInfo -- What to do for wildcards in the kind
+ }
+
+smVanilla :: SkolemMode
+smVanilla = SM { sm_clone = panic "sm_clone" -- We always override this
+ , sm_parent = False
+ , sm_tvtv = False
+ , sm_kind = AnyKind
+ , sm_holes = Nothing }
+
+{- Note [Cloning for type variable binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Sometimes we must clone the Name of a type variable binder (written in
+the source program); and sometimes we must not. This is controlled by
+the sm_clone field of SkolemMode.
+
+In some cases it doesn't matter whether or not we clone. Perhaps
+it'd be better to use MustClone/MayClone/MustNotClone.
+
+When we /must not/ clone
+* In the binders of a type signature (tcOuterTKBndrs)
+ f :: forall a{27}. blah
+ f = rhs
+ Then 'a' scopes over 'rhs'. When we kind-check the signature (tcHsSigType),
+ we must get the type (forall a{27}. blah) for the Id f, because
+ we bring that type variable into scope when we typecheck 'rhs'.
+
+* In the binders of a data family instance (bindOuterFamEqnTKBndrs)
+ data instance
+ forall p q. D (p,q) = D1 p | D2 q
+ We kind-check the LHS in tcDataFamInstHeader, and then separately
+ (in tcDataFamInstDecl) bring p,q into scope before looking at the
+ the constructor decls.
+
+* bindExplicitTKBndrs_Q_Tv/bindImplicitTKBndrs_Q_Tv do not clone
+ We take advantage of this in kcInferDeclHeader:
+ all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
+ If we cloned, we'd need to take a bit more care here; not hard.
+
+* bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Skol, do not clone.
+ There is no need, I think.
+
+ The payoff here is that avoiding gratuitous cloning means that we can
+ almost always take the fast path in swizzleTcTyConBndrs.
+
+When we /must/ clone.
+* bindOuterSigTKBndrs_Tv, bindExplicitTKBndrs_Tv do cloning
+
+ This for a narrow and tricky reason which, alas, I couldn't find a
+ simpler way round. #16221 is the poster child:
+
+ data SameKind :: k -> k -> *
+ data T a = forall k2 (b :: k2). MkT (SameKind a b) !Int
+
+ When kind-checking T, we give (a :: kappa1). Then:
+
+ - In kcConDecl we make a TyVarTv unification variable kappa2 for k2
+ (as described in Note [Kind-checking for GADTs], even though this
+ example is an existential)
+ - So we get (b :: kappa2) via bindExplicitTKBndrs_Tv
+ - We end up unifying kappa1 := kappa2, because of the (SameKind a b)
+
+ Now we generalise over kappa2. But if kappa2's Name is precisely k2
+ (i.e. we did not clone) we'll end up giving T the utterly final kind
+ T :: forall k2. k2 -> *
+ Nothing directly wrong with that but when we typecheck the data constructor
+ we have k2 in scope; but then it's brought into scope /again/ when we find
+ the forall k2. This is chaotic, and we end up giving it the type
+ MkT :: forall k2 (a :: k2) k2 (b :: k2).
+ SameKind @k2 a b -> Int -> T @{k2} a
+ which is bogus -- because of the shadowing of k2, we can't
+ apply T to the kind or a!
+
+ And there no reason /not/ to clone the Name when making a unification
+ variable. So that's what we do.
+-}
--------------------------------------
-- Binding type/class variables in the
@@ -3161,8 +3342,8 @@ bindTyClTyVars tycon_name thing_inside
zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar]
zonkAndScopedSort spec_tkvs
- = do { spec_tkvs <- mapM zonkAndSkolemise spec_tkvs
- -- Use zonkAndSkolemise because a skol_tv might be a TyVarTv
+ = do { spec_tkvs <- mapM zonkTcTyVarToTyVar spec_tkvs
+ -- Zonk the kinds, to we can do the dependency analayis
-- Do a stable topological sort, following
-- Note [Ordering of implicit variables] in GHC.Rename.HsType
@@ -3563,18 +3744,16 @@ tcHsPartialSigType
, TcType ) -- Tau part
-- See Note [Checking partial type signatures]
tcHsPartialSigType ctxt sig_ty
- | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
- , HsIB { hsib_ext = implicit_hs_tvs
- , hsib_body = hs_ty } <- ib_ty
- , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTyInvis hs_ty
- = addSigCtxt ctxt hs_ty $
+ | HsWC { hswc_ext = sig_wcs, hswc_body = sig_ty } <- sig_ty
+ , L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = body_ty}) <- sig_ty
+ , (L _ hs_ctxt, hs_tau) <- splitLHsQualTy body_ty
+ = addSigCtxt ctxt sig_ty $
do { mode <- mkHoleMode TypeLevel HM_Sig
- ; (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau)))
- <- solveEqualities "tcHsPartialSigType" $
+ ; (outer_bndrs, (wcs, wcx, theta, tau))
+ <- solveEqualities "tcHsPartialSigType" $
-- See Note [Failure in local type signatures]
- tcNamedWildCardBinders sig_wcs $ \ wcs ->
- bindImplicitTKBndrs_Tv implicit_hs_tvs $
- bindExplicitTKBndrs_Tv_M mode explicit_hs_tvs $
+ bindNamedWildCardBinders sig_wcs $ \ wcs ->
+ bindOuterSigTKBndrs_Tv_M mode hs_outer_bndrs $
do { -- Instantiate the type-class context; but if there
-- is an extra-constraints wildcard, just discard it here
(theta, wcx) <- tcPartialContext mode hs_ctxt
@@ -3585,11 +3764,12 @@ tcHsPartialSigType ctxt sig_ty
; return (wcs, wcx, theta, tau) }
- ; let implicit_tvbndrs = map (mkTyVarBinder SpecifiedSpec) implicit_tvs
+ ; traceTc "tcHsPartialSigType 2" empty
+ ; outer_tv_bndrs <- scopedSortOuter outer_bndrs
+ ; traceTc "tcHsPartialSigType 3" empty
-- No kind-generalization here:
- ; kindGeneralizeNone (mkInvisForAllTys implicit_tvbndrs $
- mkInvisForAllTys explicit_tvbndrs $
+ ; kindGeneralizeNone (mkInvisForAllTys outer_tv_bndrs $
mkPhiTy theta $
tau)
@@ -3601,16 +3781,17 @@ tcHsPartialSigType ctxt sig_ty
-- Zonk, so that any nested foralls can "see" their occurrences
-- See Note [Checking partial type signatures], and in particular
-- Note [Levels for wildcards]
- ; implicit_tvbndrs <- mapM zonkInvisTVBinder implicit_tvbndrs
- ; explicit_tvbndrs <- mapM zonkInvisTVBinder explicit_tvbndrs
- ; theta <- mapM zonkTcType theta
- ; tau <- zonkTcType tau
+ ; outer_tv_bndrs <- mapM zonkInvisTVBinder outer_tv_bndrs
+ ; theta <- mapM zonkTcType theta
+ ; tau <- zonkTcType tau
-- We return a proper (Name,InvisTVBinder) environment, to be sure that
-- we bring the right name into scope in the function body.
-- Test case: partial-sigs/should_compile/LocalDefinitionBug
- ; let tv_prs = (implicit_hs_tvs `zip` implicit_tvbndrs)
- ++ (hsLTyVarNames explicit_hs_tvs `zip` explicit_tvbndrs)
+ ; let outer_bndr_names :: [Name]
+ outer_bndr_names = hsOuterTyVarNames hs_outer_bndrs
+ tv_prs :: [(Name,InvisTVBinder)]
+ tv_prs = outer_bndr_names `zip` outer_tv_bndrs
-- NB: checkValidType on the final inferred type will be
-- done later by checkInferredPolyId. We can't do it
@@ -3656,7 +3837,7 @@ we do the following
They are typechecked as a recursive group, with monomorphic types,
so 'a' and 'b' will get unified together. Very like kind inference
for mutually recursive data types (sans CUSKs or SAKS); see
- Note [Cloning for tyvar binders] in GHC.Tc.Gen.HsType
+ Note [Cloning for type variable binders]
* In GHC.Tc.Gen.Sig.tcUserSigType we return a PartialSig, which (unlike
the companion CompleteSig) contains the original, as-yet-unchecked
@@ -3784,7 +3965,7 @@ tcHsPatSigType ctxt
solveEqualities "tcHsPatSigType" $
-- See Note [Failure in local type signatures]
-- and c.f #16033
- tcNamedWildCardBinders sig_wcs $ \ wcs ->
+ bindNamedWildCardBinders sig_wcs $ \ wcs ->
tcExtendNameTyVarEnv sig_tkv_prs $
do { ek <- newOpenTypeKind
; sig_ty <- tc_lhs_type mode hs_ty ek
@@ -3890,7 +4071,7 @@ It does sort checking and desugaring at the same time, in one single pass.
tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tcLHsKindSig ctxt hs_kind
- = tc_lhs_kind_sig (mkMode KindLevel) ctxt hs_kind
+ = tc_lhs_kind_sig kindLevelMode ctxt hs_kind
tc_lhs_kind_sig :: TcTyMode -> UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tc_lhs_kind_sig mode ctxt hs_kind
@@ -3927,7 +4108,11 @@ promotionErr name err
NoDataKindsTC -> text "perhaps you intended to use DataKinds"
NoDataKindsDC -> text "perhaps you intended to use DataKinds"
PatSynPE -> text "pattern synonyms cannot be promoted"
- _ -> text "it is defined and used in the same recursive group"
+ RecDataConPE -> same_rec_group_msg
+ ClassPE -> same_rec_group_msg
+ TyConPE -> same_rec_group_msg
+
+ same_rec_group_msg = text "it is defined and used in the same recursive group"
{-
************************************************************************
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index dba5bf5874..a1004e07c6 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -838,6 +838,15 @@ between alternatives.
RIP GADT refinement: refinements have been replaced by the use of explicit
equality constraints that are used in conjunction with implication constraints
to express the local scope of GADT refinements.
+
+Note [Freshen existentials]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is essential that these existentials are freshened.
+Otherwise, if we have something like
+ case (a :: Ex, b :: Ex) of (MkEx ..., MkEx ...) -> ...
+we'll give both unpacked existential variables the
+same name, leading to shadowing.
+
-}
-- Running example:
@@ -888,6 +897,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv ex_tvs
-- Get location from monad, not from ex_tvs
+ -- This freshens: See Note [Freshen existentials]
; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
-- pat_ty' is type of the actual constructor application
@@ -974,6 +984,8 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
; let all_arg_tys = ty : prov_theta ++ (map scaledThing arg_tys)
; checkExistentials ex_tvs all_arg_tys penv
; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
+ -- This freshens: Note [Freshen existentials]
+
; let ty' = substTy tenv ty
arg_tys' = substScaledTys tenv arg_tys
pat_mult = scaledMult pat_ty
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 170930c2ff..64be6780a3 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -32,6 +32,7 @@ import GHC.Tc.Gen.HsType
import GHC.Tc.Types
import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.Zonk
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.TcMType
@@ -104,21 +105,8 @@ especially on value bindings. Here's an overview.
unification variables is correct because we are in tcMonoBinds.
-Note [Scoped tyvars]
-~~~~~~~~~~~~~~~~~~~~
-The -XScopedTypeVariables flag brings lexically-scoped type variables
-into scope for any explicitly forall-quantified type variables:
- f :: forall a. a -> a
- f x = e
-Then 'a' is in scope inside 'e'.
-
-However, we do *not* support this
- - For pattern bindings e.g
- f :: forall a. a->a
- (f,g) = e
-
Note [Binding scoped type variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The type variables *brought into lexical scope* by a type signature
may be a subset of the *quantified type variables* of the signatures,
for two reasons:
@@ -264,13 +252,17 @@ completeSigFromId ctxt id
, sig_loc = getSrcSpan id }
isCompleteHsSig :: LHsSigWcType GhcRn -> Bool
--- ^ If there are no wildcards, return a LHsSigType
-isCompleteHsSig (HsWC { hswc_ext = wcs
- , hswc_body = HsIB { hsib_body = hs_ty } })
- = null wcs && no_anon_wc hs_ty
+-- ^ If there are no wildcards, return a LHsSigWcType
+isCompleteHsSig (HsWC { hswc_ext = wcs, hswc_body = hs_sig_ty })
+ = null wcs && no_anon_wc_sig_ty hs_sig_ty
+
+no_anon_wc_sig_ty :: LHsSigType GhcRn -> Bool
+no_anon_wc_sig_ty (L _ (HsSig{sig_bndrs = outer_bndrs, sig_body = body}))
+ = all no_anon_wc_tvb (hsOuterExplicitBndrs outer_bndrs)
+ && no_anon_wc_ty body
-no_anon_wc :: LHsType GhcRn -> Bool
-no_anon_wc lty = go lty
+no_anon_wc_ty :: LHsType GhcRn -> Bool
+no_anon_wc_ty lty = go lty
where
go (L _ ty) = case ty of
HsWildCardTy _ -> False
@@ -305,11 +297,13 @@ no_anon_wc lty = go lty
no_anon_wc_tele :: HsForAllTelescope GhcRn -> Bool
no_anon_wc_tele tele = case tele of
- HsForAllVis { hsf_vis_bndrs = ltvs } -> all (go . unLoc) ltvs
- HsForAllInvis { hsf_invis_bndrs = ltvs } -> all (go . unLoc) ltvs
- where
- go (UserTyVar _ _ _) = True
- go (KindedTyVar _ _ _ ki) = no_anon_wc ki
+ HsForAllVis { hsf_vis_bndrs = ltvs } -> all no_anon_wc_tvb ltvs
+ HsForAllInvis { hsf_invis_bndrs = ltvs } -> all no_anon_wc_tvb ltvs
+
+no_anon_wc_tvb :: LHsTyVarBndr flag GhcRn -> Bool
+no_anon_wc_tvb (L _ tvb) = case tvb of
+ UserTyVar _ _ _ -> True
+ KindedTyVar _ _ _ ki -> no_anon_wc_ty ki
{- Note [Fail eagerly on bad signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -378,17 +372,17 @@ completely solving them.
tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
-- See Note [Pattern synonym signatures]
-- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
-tcPatSynSig name sig_ty
- | HsIB { hsib_ext = implicit_hs_tvs
- , hsib_body = hs_ty } <- sig_ty
- , (univ_hs_tvbndrs, hs_req, hs_ty1) <- splitLHsSigmaTyInvis hs_ty
- , (ex_hs_tvbndrs, hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1
- = do { traceTc "tcPatSynSig 1" (ppr sig_ty)
- ; (tclvl, wanted, (implicit_tvs, (univ_tvbndrs, (ex_tvbndrs, (req, prov, body_ty)))))
- <- pushLevelAndSolveEqualitiesX "tcPatSynSig" $
- bindImplicitTKBndrs_Skol implicit_hs_tvs $
- bindExplicitTKBndrs_Skol univ_hs_tvbndrs $
- bindExplicitTKBndrs_Skol ex_hs_tvbndrs $
+tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty}))
+ | (hs_req, hs_ty1) <- splitLHsQualTy hs_ty
+ , (ex_hs_tvbndrs, hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1
+ = do { traceTc "tcPatSynSig 1" (ppr sig_ty)
+
+ ; let skol_info = DataConSkol name
+ ; (tclvl, wanted, (outer_bndrs, (ex_bndrs, (req, prov, body_ty))))
+ <- pushLevelAndSolveEqualitiesX "tcPatSynSig" $
+ -- See Note [solveEqualities in tcPatSynSig]
+ tcOuterTKBndrs skol_info hs_outer_bndrs $
+ tcExplicitTKBndrs ex_hs_tvbndrs $
do { req <- tcHsContext hs_req
; prov <- tcHsContext hs_prov
; body_ty <- tcHsOpenType hs_body_ty
@@ -396,32 +390,37 @@ tcPatSynSig name sig_ty
-- e.g. pattern Zero <- 0# (#12094)
; return (req, prov, body_ty) }
+ ; let implicit_tvs :: [TcTyVar]
+ univ_bndrs :: [TcInvisTVBinder]
+ (implicit_tvs, univ_bndrs) = case outer_bndrs of
+ HsOuterImplicit{hso_ximplicit = implicit_tvs} -> (implicit_tvs, [])
+ HsOuterExplicit{hso_xexplicit = univ_bndrs} -> ([], univ_bndrs)
+
; implicit_tvs <- zonkAndScopedSort implicit_tvs
- ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvbndrs
- req ex_tvbndrs prov body_ty
+ ; let implicit_bndrs = mkTyVarBinders SpecifiedSpec implicit_tvs
-- Kind generalisation
- ; kvs <- kindGeneralizeAll ungen_patsyn_ty
+ ; let ungen_patsyn_ty = build_patsyn_type implicit_bndrs univ_bndrs
+ req ex_bndrs prov body_ty
; traceTc "tcPatSynSig" (ppr ungen_patsyn_ty)
-
- ; let skol_tvs = kvs ++ implicit_tvs ++ binderVars (univ_tvbndrs ++ ex_tvbndrs)
- skol_info = DataConSkol name
- ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
+ ; kvs <- kindGeneralizeAll ungen_patsyn_ty
+ ; reportUnsolvedEqualities skol_info kvs tclvl wanted
-- See Note [Report unsolved equalities in tcPatSynSig]
-- These are /signatures/ so we zonk to squeeze out any kind
-- unification variables. Do this after kindGeneralizeAll which may
-- default kind variables to *.
- ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
- ; univ_tvbndrs <- mapM zonkTyCoVarKindBinder univ_tvbndrs
- ; ex_tvbndrs <- mapM zonkTyCoVarKindBinder ex_tvbndrs
- ; req <- zonkTcTypes req
- ; prov <- zonkTcTypes prov
- ; body_ty <- zonkTcType body_ty
+ ; (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
-- Now do validity checking
; checkValidType ctxt $
- build_patsyn_type kvs implicit_tvs univ_tvbndrs req ex_tvbndrs prov body_ty
+ build_patsyn_type implicit_bndrs univ_bndrs req ex_bndrs prov body_ty
-- arguments become the types of binders. We thus cannot allow
-- levity polymorphism here
@@ -429,27 +428,25 @@ tcPatSynSig name sig_ty
; mapM_ (checkForLevPoly empty . scaledThing) arg_tys
; traceTc "tcTySig }" $
- vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs
- , text "kvs" <+> ppr_tvs kvs
- , text "univ_tvs" <+> ppr_tvs (binderVars univ_tvbndrs)
+ vcat [ text "kvs" <+> ppr_tvs (binderVars kv_bndrs)
+ , text "implicit_tvs" <+> ppr_tvs (binderVars implicit_bndrs)
+ , text "univ_tvs" <+> ppr_tvs (binderVars univ_bndrs)
, text "req" <+> ppr req
- , text "ex_tvs" <+> ppr_tvs (binderVars ex_tvbndrs)
+ , text "ex_tvs" <+> ppr_tvs (binderVars ex_bndrs)
, text "prov" <+> ppr prov
, text "body_ty" <+> ppr body_ty ]
; return (TPSI { patsig_name = name
- , patsig_implicit_bndrs = mkTyVarBinders InferredSpec kvs ++
- mkTyVarBinders SpecifiedSpec implicit_tvs
- , patsig_univ_bndrs = univ_tvbndrs
+ , patsig_implicit_bndrs = kv_bndrs ++ implicit_bndrs
+ , patsig_univ_bndrs = univ_bndrs
, patsig_req = req
- , patsig_ex_bndrs = ex_tvbndrs
+ , patsig_ex_bndrs = ex_bndrs
, patsig_prov = prov
, patsig_body_ty = body_ty }) }
where
ctxt = PatSynCtxt name
- build_patsyn_type kvs imp univ_bndrs req ex_bndrs prov body
- = mkInfForAllTys kvs $
- mkSpecForAllTys imp $
+ build_patsyn_type implicit_bndrs univ_bndrs req ex_bndrs prov body
+ = mkInvisForAllTys implicit_bndrs $
mkInvisForAllTys univ_bndrs $
mkPhiTy req $
mkInvisForAllTys ex_bndrs $
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index 115c64f341..754059571b 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -2470,14 +2470,14 @@ getGhciStepIO = do
let ghciM = nlHsAppTy (nlHsTyVar ghciTy) (nlHsTyVar a_tv)
ioM = nlHsAppTy (nlHsTyVar ioTyConName) (nlHsTyVar a_tv)
- step_ty = noLoc $ HsForAllTy
- { hst_tele = mkHsForAllInvisTele
- [noLoc $ UserTyVar noExtField SpecifiedSpec (noLoc a_tv)]
- , hst_xforall = noExtField
- , hst_body = nlHsFunTy ghciM ioM }
+ step_ty :: LHsSigType GhcRn
+ step_ty = noLoc $ HsSig
+ { sig_bndrs = HsOuterImplicit{hso_ximplicit = [a_tv]}
+ , sig_ext = noExtField
+ , sig_body = nlHsFunTy ghciM ioM }
stepTy :: LHsSigWcType GhcRn
- stepTy = mkEmptyWildCardBndrs (mkEmptyImplicitBndrs step_ty)
+ stepTy = mkEmptyWildCardBndrs step_ty
return (noLoc $ ExprWithTySig noExtField (nlHsVar ghciStepIoMName) stepTy)
@@ -2610,7 +2610,7 @@ tcRnType hsc_env flexi normalise rdr_type
; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
; (_tclvl, wanted, (ty, kind))
<- pushLevelAndSolveEqualitiesX "tcRnType" $
- tcNamedWildCardBinders wcs $ \ wcs' ->
+ bindNamedWildCardBinders wcs $ \ wcs' ->
do { mapM_ emitNamedTypeHole wcs'
; tcInferLHsTypeUnsaturated rn_type }
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index bf7e9b239e..dc23ca54e6 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -18,7 +18,7 @@ module GHC.Tc.Solver(
simplifyTopWanteds,
- promoteTyVarSet, emitFlatConstraints,
+ promoteTyVarSet, simplifyAndEmitFlatConstraints,
-- For Rules we need these
solveWanteds, solveWantedsAndDrop,
@@ -200,24 +200,29 @@ solveEqualities :: String -> TcM a -> TcM a
solveEqualities callsite thing_inside
= do { traceTc "solveEqualities {" (text "Called from" <+> text callsite)
; (res, wanted) <- captureConstraints thing_inside
- ; residual_wanted <- runTcSEqualities (solveWantedsAndDrop wanted)
- ; emitFlatConstraints residual_wanted
- -- emitFlatConstraints fails outright unless the only unsolved
- -- constraints are soluble-looking equalities that can float out
- ; traceTc "solveEqualities }" (text "Residual: " <+> ppr residual_wanted)
+ ; simplifyAndEmitFlatConstraints wanted
+ -- simplifyAndEmitFlatConstraints fails outright unless
+ -- the only unsolved constraints are soluble-looking
+ -- equalities that can float out
+ ; traceTc "solveEqualities }" empty
; return res }
-emitFlatConstraints :: WantedConstraints -> TcM ()
+simplifyAndEmitFlatConstraints :: WantedConstraints -> TcM ()
-- See Note [Failure in local type signatures]
-emitFlatConstraints wanted
- = do { wanted <- TcM.zonkWC wanted
+simplifyAndEmitFlatConstraints wanted
+ = do { -- Solve and zonk to esablish the
+ -- preconditions for floatKindEqualities
+ wanted <- runTcSEqualities (solveWanteds wanted)
+ ; wanted <- TcM.zonkWC wanted
+
+ ; traceTc "emitFlatConstraints {" (ppr wanted)
; case floatKindEqualities wanted of
- Nothing -> do { traceTc "emitFlatConstraints: failing" (ppr wanted)
+ Nothing -> do { traceTc "emitFlatConstraints } failing" (ppr wanted)
; emitConstraints wanted -- So they get reported!
; failM }
Just (simples, holes)
- -> do { _ <- TcM.promoteTyVarSet (tyCoVarsOfCts simples)
- ; traceTc "emitFlatConstraints:" $
+ -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples)
+ ; traceTc "emitFlatConstraints }" $
vcat [ text "simples:" <+> ppr simples
, text "holes: " <+> ppr holes ]
; emitHoles holes -- Holes don't need promotion
@@ -228,6 +233,12 @@ floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag Hole)
-- Return Nothing if any constraints can't be floated (captured
-- by skolems), or if there is an insoluble constraint, or
-- IC_Telescope telescope error
+-- Precondition 1: we have tried to solve the 'wanteds', both so that
+-- the ic_status field is set, and because solving can make constraints
+-- more floatable.
+-- Precondition 2: the 'wanteds' are zonked, since floatKindEqualities
+-- is not monadic
+-- See Note [floatKindEqualities vs approximateWC]
floatKindEqualities wc = float_wc emptyVarSet wc
where
float_wc :: TcTyCoVarSet -> WantedConstraints -> Maybe (Bag Ct, Bag Hole)
@@ -328,7 +339,7 @@ So here's the plan (see tcHsSigType):
* buildTvImplication: build an implication for the residual, unsolved
constraint
-* emitFlatConstraints: try to float out every unsolved equalities
+* simplifyAndEmitFlatConstraints: try to float out every unsolved equality
inside that implication, in the hope that it constrains only global
type variables, not the locally-quantified ones.
@@ -364,6 +375,16 @@ All this is done:
reporting errors, we avoid that happening.
See also #18062, #11506
+
+Note [floatKindEqualities vs approximateWC]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+floatKindEqualities and approximateWC are strikingly similar to each
+other, but
+
+* floatKindEqualites tries to float /all/ equalities, and fails if
+ it can't, or if any implication is insoluble.
+* approximateWC just floats out any constraints
+ (not just equalities) that can float; it never fails.
-}
@@ -1928,7 +1949,7 @@ checkBadTelescope :: Implication -> TcS Bool
-- See Note [Checking telescopes] in GHC.Tc.Types.Constraint
checkBadTelescope (Implic { ic_info = info
, ic_skols = skols })
- | ForAllSkol {} <- info
+ | checkTelescopeSkol info
= do{ skols <- mapM TcS.zonkTyCoVarKind skols
; return (go emptyVarSet (reverse skols))}
@@ -2237,6 +2258,7 @@ defaultTyVarTcS the_tv
approximateWC :: Bool -> WantedConstraints -> Cts
-- Postcondition: Wanted or Derived Cts
-- See Note [ApproximateWC]
+-- See Note [floatKindEqualities vs approximateWC]
approximateWC float_past_equalities wc
= float_wc emptyVarSet wc
where
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 924996edfd..5bd83982f1 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -2145,7 +2145,7 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 rhs
| otherwise -- For some reason (occurs check, or forall) we can't unify
-- We must not use it for further rewriting!
- = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr rhs)
+ = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr rhs $$ ppr mtvu)
; new_ev <- rewriteEqEvidence ev swapped lhs rhs rewrite_co1 rewrite_co2
; let status | isInsolubleOccursCheck eq_rel tv1 rhs
= InsolubleCIS
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 3983113554..38fc88407c 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -38,6 +38,8 @@ import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX
, reportUnsolvedEqualities )
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Env
+import GHC.Tc.Utils.Unify( emitResidualTvConstraint )
+import GHC.Tc.Types.Constraint( emptyWC )
import GHC.Tc.Validity
import GHC.Tc.Utils.Zonk
import GHC.Tc.TyCl.Utils
@@ -755,7 +757,9 @@ swizzleTcTyConBndrs :: [(TcTyCon, ScopedPairs, TcKind)]
swizzleTcTyConBndrs tc_infos
| all no_swizzle swizzle_prs
-- This fast path happens almost all the time
- -- See Note [Non-cloning for tyvar binders] in GHC.Tc.Gen.HsType
+ -- See Note [Cloning for type variable binders] in GHC.Tc.Gen.HsType
+ -- "Almost all the time" means not the case of mutual recursion with
+ -- polymorphic kinds.
= do { traceTc "Skipping swizzleTcTyConBndrs for" (ppr (map fstOf3 tc_infos))
; return tc_infos }
@@ -1560,11 +1564,9 @@ kcTyClDecl (ClassDecl { tcdLName = L _ name
do { _ <- tcHsContext ctxt
; mapM_ (wrapLocM_ kc_sig) sigs }
where
- kc_sig (ClassOpSig _ _ nms op_ty) = kcClassSigType skol_info nms op_ty
+ kc_sig (ClassOpSig _ _ nms op_ty) = kcClassSigType nms op_ty
kc_sig _ = return ()
- skol_info = TyConSkol ClassFlavour name
-
kcTyClDecl (FamDecl _ (FamilyDecl { fdInfo = fd_info })) fam_tc
-- closed type families look at their equations, but other families don't
-- do anything here
@@ -1636,8 +1638,8 @@ kcConDecl new_or_data res_kind (ConDeclH98
}
kcConDecl new_or_data res_kind (ConDeclGADT
- { con_names = names, con_qvars = explicit_tkv_nms, con_mb_cxt = cxt
- , con_g_args = args, con_res_ty = res_ty, con_g_ext = implicit_tkv_nms })
+ { con_names = names, con_bndrs = L _ outer_bndrs, con_mb_cxt = cxt
+ , con_g_args = args, con_res_ty = res_ty })
= -- Even though the GADT-style data constructor's type is closed,
-- we must still kind-check the type, because that may influence
-- the inferred kind of the /type/ constructor. Example:
@@ -1646,9 +1648,8 @@ kcConDecl new_or_data res_kind (ConDeclGADT
-- If we don't look at MkT we won't get the correct kind
-- for the type constructor T
addErrCtxt (dataConCtxtName names) $
- discardResult $
- bindImplicitTKBndrs_Tv implicit_tkv_nms $
- bindExplicitTKBndrs_Tv explicit_tkv_nms $
+ discardResult $
+ bindOuterSigTKBndrs_Tv outer_bndrs $
-- Why "_Tv"? See Note [Kind-checking for GADTs]
do { _ <- tcHsMbContext cxt
; kcConGADTArgs new_or_data res_kind args
@@ -2437,11 +2438,10 @@ tcDefaultAssocDecl _ (d1:_:_)
tcDefaultAssocDecl fam_tc
[L loc (TyFamInstDecl { tfid_eqn =
- HsIB { hsib_ext = imp_vars
- , hsib_body = FamEqn { feqn_tycon = L _ tc_name
- , feqn_bndrs = mb_expl_bndrs
+ FamEqn { feqn_tycon = L _ tc_name
+ , feqn_bndrs = outer_bndrs
, feqn_pats = hs_pats
- , feqn_rhs = hs_rhs_ty }}})]
+ , feqn_rhs = hs_rhs_ty }})]
= -- See Note [Type-checking default assoc decls]
setSrcSpan loc $
tcAddFamInstCtxt (text "default type instance") tc_name $
@@ -2465,8 +2465,7 @@ tcDefaultAssocDecl fam_tc
-- type default LHS can mention *different* type variables than the
-- enclosing class. So it's treated more as a freestanding beast.
; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc NotAssociated
- imp_vars (mb_expl_bndrs `orElse` [])
- hs_pats hs_rhs_ty
+ outer_bndrs hs_pats hs_rhs_ty
; let fam_tvs = tyConTyVars fam_tc
; traceTc "tcDefaultAssocDecl 2" (vcat
@@ -2845,17 +2844,15 @@ kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
-- Used for the equations of a closed type family only
-- Not used for data/type instances
kcTyFamInstEqn tc_fam_tc
- (L loc (HsIB { hsib_ext = imp_vars
- , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
- , feqn_bndrs = mb_expl_bndrs
- , feqn_pats = hs_pats
- , feqn_rhs = hs_rhs_ty }}))
+ (L loc (FamEqn { feqn_tycon = L _ eqn_tc_name
+ , feqn_bndrs = outer_bndrs
+ , feqn_pats = hs_pats
+ , feqn_rhs = hs_rhs_ty }))
= setSrcSpan loc $
do { traceTc "kcTyFamInstEqn" (vcat
[ text "tc_name =" <+> ppr eqn_tc_name
, text "fam_tc =" <+> ppr tc_fam_tc <+> dcolon <+> ppr (tyConKind tc_fam_tc)
- , text "hsib_vars =" <+> ppr imp_vars
- , text "feqn_bndrs =" <+> ppr mb_expl_bndrs
+ , text "feqn_bndrs =" <+> ppr outer_bndrs
, text "feqn_pats =" <+> ppr hs_pats ])
-- this check reports an arity error instead of a kind error; easier for user
; let vis_pats = numVisibleArgs hs_pats
@@ -2871,8 +2868,7 @@ kcTyFamInstEqn tc_fam_tc
wrongNumberOfParmsErr vis_arity
; discardResult $
- bindImplicitTKBndrs_Q_Tv imp_vars $
- bindExplicitTKBndrs_Q_Tv AnyKind (mb_expl_bndrs `orElse` []) $
+ bindOuterFamEqnTKBndrs_Q_Tv outer_bndrs $
do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats
; tcCheckLHsType hs_rhs_ty (TheKind res_kind) }
-- Why "_Tv" here? Consider (#14066
@@ -2892,13 +2888,12 @@ tcTyFamInstEqn :: TcTyCon -> AssocInstInfo -> LTyFamInstEqn GhcRn
-- (typechecked here) have TyFamInstEqns
tcTyFamInstEqn fam_tc mb_clsinfo
- (L loc (HsIB { hsib_ext = imp_vars
- , hsib_body = FamEqn { feqn_bndrs = mb_expl_bndrs
- , feqn_pats = hs_pats
- , feqn_rhs = hs_rhs_ty }}))
+ (L loc (FamEqn { feqn_bndrs = outer_bndrs
+ , feqn_pats = hs_pats
+ , feqn_rhs = hs_rhs_ty }))
= setSrcSpan loc $
do { traceTc "tcTyFamInstEqn" $
- vcat [ ppr fam_tc <+> ppr hs_pats
+ vcat [ ppr loc, ppr fam_tc <+> ppr hs_pats
, text "fam tc bndrs" <+> pprTyVars (tyConTyVars fam_tc)
, case mb_clsinfo of
NotAssociated {} -> empty
@@ -2914,24 +2909,15 @@ tcTyFamInstEqn fam_tc mb_clsinfo
; checkTc (vis_pats == vis_arity) $
wrongNumberOfParmsErr vis_arity
; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc mb_clsinfo
- imp_vars (mb_expl_bndrs `orElse` [])
- hs_pats hs_rhs_ty
+ outer_bndrs hs_pats hs_rhs_ty
-- Don't print results they may be knot-tied
-- (tcFamInstEqnGuts zonks to Type)
; return (mkCoAxBranch qtvs [] [] pats rhs_ty
(map (const Nominal) qtvs)
loc) }
-{-
-Kind check type patterns and kind annotate the embedded type variables.
- type instance F [a] = rhs
-
- * Here we check that a type instance matches its kind signature, but we do
- not check whether there is a pattern for each type index; the latter
- check is only required for type synonym instances.
-
-Note [Instantiating a family tycon]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Instantiating a family tycon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's possible that kind-checking the result of a family tycon applied to
its patterns will instantiate the tycon further. For example, we might
have
@@ -2960,19 +2946,30 @@ We want to quantify over all the free vars of the LHS including
such as Proxy
* wildcards such as '_' above
-So, the simple thing is
- - Gather candidates from the LHS
- - Include any user-specified forall'd variables, so that we get an
- error from Validity.checkFamPatBinders if a forall'd variable is
- not bound on the LHS
- - Quantify over them
+The wildcards are particularly awkward: they may need to be quantified
+ - before the explicit variables k,a,b
+ - after them
+ - or even interleaved with them
+ c.f. Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType
+
+So, we use bindOuterFamEqnTKBndrs (which does not create an implication for
+the telescope), and generalise over /all/ the variables in the LHS,
+without treating the explicitly-quanfitifed ones specially. Wrinkles:
+
+ - When generalising, include the explicit user-specified forall'd
+ variables, so that we get an error from Validity.checkFamPatBinders
+ if a forall'd variable is not bound on the LHS
-Note that, unlike a type signature like
- f :: forall (a::k). blah
-we do /not/ care about the Inferred/Specified designation
-or order for the final quantified tyvars. Type-family
-instances are not invoked directly in Haskell source code,
-so visible type application etc plays no role.
+ - We still want to complain about a bad telescope among the user-specified
+ variables. So in checkFamTelescope we emit an implication constraint
+ quantifying only over them, purely so that we get a good telescope error.
+
+ - Note that, unlike a type signature like
+ f :: forall (a::k). blah
+ we do /not/ care about the Inferred/Specified designation or order for
+ the final quantified tyvars. Type-family instances are not invoked
+ directly in Haskell source code, so visible type application etc plays
+ no role.
See also Note [Re-quantify type variables in rules] in
GHC.Tc.Gen.Rule, which explains a /very/ similar design when
@@ -2982,12 +2979,12 @@ generalising over the type of a rewrite rule.
--------------------------
tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo
- -> [Name] -> [LHsTyVarBndr () GhcRn] -- Implicit and explicit binder
+ -> HsOuterFamEqnTyVarBndrs GhcRn -- Implicit and explicit binders
-> HsTyPats GhcRn -- Patterns
-> LHsType GhcRn -- RHS
-> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs)
-- Used only for type families, not data families
-tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
+tcTyFamInstEqnGuts fam_tc mb_clsinfo outer_hs_bndrs hs_pats hs_rhs_ty
= do { traceTc "tcTyFamInstEqnGuts {" (ppr fam_tc)
-- By now, for type families (but not data families) we should
@@ -2995,10 +2992,9 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
-- This code is closely related to the code
-- in GHC.Tc.Gen.HsType.kcCheckDeclHeader_cusk
- ; (tclvl, wanted, (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty))))
+ ; (tclvl, wanted, (outer_tvs, (lhs_ty, rhs_ty)))
<- pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $
- bindImplicitTKBndrs_Q_Skol imp_vars $
- bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
+ bindOuterFamEqnTKBndrs outer_hs_bndrs $
do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats
-- Ensure that the instance is consistent with its
-- parent class (#16008)
@@ -3013,9 +3009,10 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
-- check there too!
-- See Note [Generalising in tcTyFamInstEqnGuts]
- ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys (imp_tvs ++ exp_tvs))
+ ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys outer_tvs)
; qtvs <- quantifyTyVars dvs
; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
+ ; checkFamTelescope tclvl outer_hs_bndrs outer_tvs
; traceTc "tcTyFamInstEqnGuts 2" $
vcat [ ppr fam_tc
@@ -3033,6 +3030,22 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
; traceTc "tcTyFamInstEqnGuts }" (ppr fam_tc <+> pprTyVars qtvs)
; return (qtvs, pats, rhs_ty) }
+
+checkFamTelescope :: TcLevel -> HsOuterFamEqnTyVarBndrs GhcRn
+ -> [TcTyVar] -> TcM ()
+-- Emit a constraint (forall a b c. <empty>), so that
+-- we will do telescope-checking on a,b,c
+-- See Note [Generalising in tcTyFamInstEqnGuts]
+checkFamTelescope tclvl hs_outer_bndrs outer_tvs
+ | HsOuterExplicit { hso_bndrs = bndrs } <- hs_outer_bndrs
+ , (b_first : _) <- bndrs
+ , let b_last = last bndrs
+ skol_info = ForAllSkol (fsep (map ppr bndrs))
+ = setSrcSpan (combineSrcSpans (getLoc b_first) (getLoc b_last)) $
+ emitResidualTvConstraint skol_info outer_tvs tclvl emptyWC
+ | otherwise
+ = return ()
+
-----------------
unravelFamInstPats :: TcType -> [TcType]
-- Decompose fam_app to get the argument patterns
@@ -3218,8 +3231,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
; (tclvl, wanted, (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts)))
- <- pushLevelAndSolveEqualitiesX "tcConDecl:H98" $
- bindExplicitTKBndrs_Skol explicit_tkv_nms $
+ <- pushLevelAndSolveEqualitiesX "tcConDecl:H98" $
+ tcExplicitTKBndrs explicit_tkv_nms $
do { ctxt <- tcHsMbContext hs_ctxt
; let exp_kind = getArgExpKind new_or_data res_kind
; btys <- tcConH98Args exp_kind hs_args
@@ -3248,7 +3261,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
; kvs <- kindGeneralizeAll fake_ty
- ; let skol_tvs = kvs ++ tmpl_tvs ++ binderVars exp_tvbndrs
+ ; let skol_tvs = kvs ++ tmpl_tvs
; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
-- Zonk to Types
@@ -3289,19 +3302,17 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
-- NB: don't use res_kind here, as it's ill-scoped. Instead,
-- we get the res_kind by typechecking the result type.
- (ConDeclGADT { con_g_ext = implicit_tkv_nms
- , con_names = names
- , con_qvars = explicit_tkv_nms
+ (ConDeclGADT { con_names = names
+ , con_bndrs = L _ outer_hs_bndrs
, con_mb_cxt = cxt, con_g_args = hs_args
, con_res_ty = hs_res_ty })
= addErrCtxt (dataConCtxtName names) $
do { traceTc "tcConDecl 1 gadt" (ppr names)
; let (L _ name : _) = names
- ; (tclvl, wanted, (imp_tvs, (exp_tvbndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts))))
+ ; (tclvl, wanted, (outer_bndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
<- pushLevelAndSolveEqualitiesX "tcConDecl:GADT" $
- bindImplicitTKBndrs_Skol implicit_tkv_nms $
- bindExplicitTKBndrs_Skol explicit_tkv_nms $
+ tcOuterTKBndrs skol_info outer_hs_bndrs $
do { ctxt <- tcHsMbContext cxt
; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty
-- See Note [GADT return kinds]
@@ -3314,19 +3325,17 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
; field_lbls <- lookupConstructorFields name
; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
}
- ; imp_tvs <- zonkAndScopedSort imp_tvs
- ; let con_ty = mkSpecForAllTys imp_tvs $
- mkInvisForAllTys exp_tvbndrs $
- mkPhiTy ctxt $
- mkVisFunTys arg_tys $
- res_ty
- ; kvs <- kindGeneralizeAll con_ty
- ; let tvbndrs = mkTyVarBinders InferredSpec kvs
- ++ mkTyVarBinders SpecifiedSpec imp_tvs
- ++ exp_tvbndrs
+ ; outer_tv_bndrs <- scopedSortOuter outer_bndrs
+
+ ; tkvs <- kindGeneralizeAll (mkInvisForAllTys outer_tv_bndrs $
+ mkPhiTy ctxt $
+ mkVisFunTys arg_tys $
+ res_ty)
+ ; traceTc "tcConDecl:GADT" (ppr names $$ ppr res_ty $$ ppr tkvs)
+ ; reportUnsolvedEqualities skol_info tkvs tclvl wanted
- ; reportUnsolvedEqualities skol_info (binderVars tvbndrs) tclvl wanted
+ ; let tvbndrs = mkTyVarBinders InferredSpec tkvs ++ outer_tv_bndrs
-- Zonk to Types
; (ze, tvbndrs) <- zonkTyVarBinders tvbndrs
@@ -4825,8 +4834,7 @@ tcAddTyFamInstCtxt decl
= tcAddFamInstCtxt (text "type instance") (tyFamInstDeclName decl)
tcMkDataFamInstCtxt :: DataFamInstDecl GhcRn -> SDoc
-tcMkDataFamInstCtxt decl@(DataFamInstDecl { dfid_eqn =
- HsIB { hsib_body = eqn }})
+tcMkDataFamInstCtxt decl@(DataFamInstDecl { dfid_eqn = eqn })
= tcMkFamInstCtxt (pprDataFamInstFlavour decl <+> text "instance")
(unLoc (feqn_tycon eqn))
diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs
index 92be85fa06..8e637a1a32 100644
--- a/compiler/GHC/Tc/TyCl/Class.hs
+++ b/compiler/GHC/Tc/TyCl/Class.hs
@@ -157,16 +157,14 @@ tcClassSigs clas sigs def_methods
dm_bind_names :: [Name] -- These ones have a value binding in the class decl
dm_bind_names = [op | L _ (FunBind {fun_id = L _ op}) <- bagToList def_methods]
- skol_info = TyConSkol ClassFlavour clas
-
tc_sig :: NameEnv (SrcSpan, Type) -> ([Located Name], LHsSigType GhcRn)
-> TcM [TcMethInfo]
tc_sig gen_dm_env (op_names, op_hs_ty)
= do { traceTc "ClsSig 1" (ppr op_names)
- ; op_ty <- tcClassSigType skol_info op_names op_hs_ty
+ ; op_ty <- tcClassSigType op_names op_hs_ty
-- Class tyvars already in scope
- ; traceTc "ClsSig 2" (ppr op_names)
+ ; traceTc "ClsSig 2" (ppr op_names $$ ppr op_ty)
; return [ (op_name, op_ty, f op_name) | L _ op_name <- op_names ] }
where
f nm | Just lty <- lookupNameEnv gen_dm_env nm = Just (GenericDM lty)
@@ -174,7 +172,7 @@ tcClassSigs clas sigs def_methods
| otherwise = Nothing
tc_gen_sig (op_names, gen_hs_ty)
- = do { gen_op_ty <- tcClassSigType skol_info op_names gen_hs_ty
+ = do { gen_op_ty <- tcClassSigType op_names gen_hs_ty
; return [ (op_name, (loc, gen_op_ty)) | L loc op_name <- op_names ] }
{-
@@ -290,7 +288,7 @@ tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn
; let local_dm_id = mkLocalId local_dm_name Many local_dm_ty
local_dm_sig = CompleteSig { sig_bndr = local_dm_id
, sig_ctxt = ctxt
- , sig_loc = getLoc (hsSigType hs_ty) }
+ , sig_loc = getLoc hs_ty }
; (ev_binds, (tc_bind, _))
<- checkConstraints skol_info tyvars [this_dict] $
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index cc47d1e348..2c52a89248 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -531,7 +531,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
-- Finally, construct the Core representation of the instance.
-- (This no longer includes the associated types.)
- ; dfun_name <- newDFunName clas inst_tys (getLoc (hsSigType hs_ty))
+ ; dfun_name <- newDFunName clas inst_tys (getLoc hs_ty)
-- Dfun location is that of instance *header*
; ispec <- newClsInst (fmap unLoc overlap_mode) dfun_name
@@ -559,7 +559,6 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds
defined_ats = mkNameSet (map (tyFamInstDeclName . unLoc) ats)
`unionNameSet`
mkNameSet (map (unLoc . feqn_tycon
- . hsib_body
. dfid_eqn
. unLoc) adts)
@@ -583,7 +582,7 @@ tcTyFamInstDecl :: AssocInstInfo
tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
= setSrcSpan loc $
tcAddTyFamInstCtxt decl $
- do { let fam_lname = feqn_tycon (hsib_body eqn)
+ do { let fam_lname = feqn_tycon eqn
; fam_tc <- tcLookupLocatedTyCon fam_lname
; tcFamInstDeclChecks mb_clsinfo fam_tc
@@ -592,10 +591,11 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
-- (1) do the work of verifying the synonym group
+ -- For some reason we don't have a location for the equation
+ -- itself, so we make do with the location of family name
; co_ax_branch <- tcTyFamInstEqn fam_tc mb_clsinfo
(L (getLoc fam_lname) eqn)
-
-- (2) check for validity
; checkConsistentFamInst mb_clsinfo fam_tc co_ax_branch
; checkValidCoAxBranch fam_tc co_ax_branch
@@ -665,9 +665,8 @@ tcDataFamInstDecl ::
-> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
-- "newtype instance" and "data instance"
tcDataFamInstDecl mb_clsinfo tv_skol_env
- (L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext = imp_vars
- , hsib_body =
- FamEqn { feqn_bndrs = mb_bndrs
+ (L loc decl@(DataFamInstDecl { dfid_eqn =
+ FamEqn { feqn_bndrs = outer_bndrs
, feqn_pats = hs_pats
, feqn_tycon = lfam_name@(L _ fam_name)
, feqn_fixity = fixity
@@ -676,7 +675,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
, dd_ctxt = hs_ctxt
, dd_cons = hs_cons
, dd_kindSig = m_ksig
- , dd_derivs = derivs } }}}))
+ , dd_derivs = derivs } }}))
= setSrcSpan loc $
tcAddDataFamInstCtxt decl $
do { fam_tc <- tcLookupLocatedTyCon lfam_name
@@ -689,7 +688,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env
-- Do /not/ check that the number of patterns = tyConArity fam_tc
-- See [Arity of data families] in GHC.Core.FamInstEnv
; (qtvs, pats, res_kind, stupid_theta)
- <- tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs
+ <- tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs
fixity hs_ctxt hs_pats m_ksig hs_cons
new_or_data
@@ -856,7 +855,7 @@ TyVarEnv will simply be empty, and there is nothing to worry about.
-----------------------
tcDataFamInstHeader
- :: AssocInstInfo -> TyCon -> [Name] -> Maybe [LHsTyVarBndr () GhcRn]
+ :: AssocInstInfo -> TyCon -> HsOuterFamEqnTyVarBndrs GhcRn
-> LexicalFixity -> LHsContext GhcRn
-> HsTyPats GhcRn -> Maybe (LHsKind GhcRn) -> [LConDecl GhcRn]
-> NewOrData
@@ -865,13 +864,12 @@ tcDataFamInstHeader
-- the data constructors themselves
-- e.g. data instance D [a] :: * -> * where ...
-- Here the "header" is the bit before the "where"
-tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
+tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
hs_ctxt hs_pats m_ksig hs_cons new_or_data
= do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
- ; (tclvl, wanted, (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind))))
+ ; (tclvl, wanted, (scoped_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
<- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
- bindImplicitTKBndrs_Q_Skol imp_vars $
- bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
+ bindOuterFamEqnTKBndrs outer_bndrs $
do { stupid_theta <- tcHsContext hs_ctxt
; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
; (lhs_applied_ty, lhs_applied_kind)
@@ -909,7 +907,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
-- check there too!
-- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
- ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys (imp_tvs ++ exp_tvs))
+ ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
; qtvs <- quantifyTyVars dvs
; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
@@ -937,9 +935,8 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
; return (qtvs, pats, master_res_kind, stupid_theta) }
where
- fam_name = tyConName fam_tc
- data_ctxt = DataKindCtxt fam_name
- exp_bndrs = mb_bndrs `orElse` []
+ fam_name = tyConName fam_tc
+ data_ctxt = DataKindCtxt fam_name
-- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, wrinkle (2).
tc_kind_sig Nothing
@@ -952,8 +949,8 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
-- See Note [Result kind signature for a data family instance]
tc_kind_sig (Just hs_kind)
= do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
- ; let (tvs, inner_kind) = tcSplitForAllTys sig_kind
; lvl <- getTcLevel
+ ; let (tvs, inner_kind) = tcSplitForAllTys sig_kind
; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
-- Perhaps surprisingly, we don't need the skolemised tvs themselves
; return (substTy subst inner_kind) }
@@ -1802,7 +1799,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
-- There is a signature in the instance
-- See Note [Instance method signatures]
= do { (sig_ty, hs_wrap)
- <- setSrcSpan (getLoc (hsSigType hs_sig_ty)) $
+ <- setSrcSpan (getLoc hs_sig_ty) $
do { inst_sigs <- xoptM LangExt.InstanceSigs
; checkTc inst_sigs (misplacedInstSig sel_name hs_sig_ty)
; sig_ty <- tcHsSigType (FunSigCtxt sel_name False) hs_sig_ty
@@ -1823,7 +1820,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
inner_meth_id = mkLocalId inner_meth_name Many sig_ty
inner_meth_sig = CompleteSig { sig_bndr = inner_meth_id
, sig_ctxt = ctxt
- , sig_loc = getLoc (hsSigType hs_sig_ty) }
+ , sig_loc = getLoc hs_sig_ty }
; (tc_bind, [inner_id]) <- tcPolyCheck no_prag_fn inner_meth_sig meth_bind
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 014a5027a4..3f5b10f343 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -24,6 +24,7 @@ import GHC.Hs
import GHC.Tc.Gen.Pat
import GHC.Core.Multiplicity
import GHC.Core.Type ( tidyTyCoVarBinders, tidyTypes, tidyType )
+import GHC.Core.TyCo.Subst( extendTvSubstWithClone )
import GHC.Tc.Utils.Monad
import GHC.Tc.Gen.Sig( emptyPragEnv, completeSigFromId )
import GHC.Tc.Utils.Env
@@ -61,7 +62,7 @@ import GHC.Utils.Misc
import GHC.Utils.Error
import Data.Maybe( mapMaybe )
import Control.Monad ( zipWithM )
-import Data.List( partition )
+import Data.List( partition, mapAccumL )
#include "HsVersions.h"
@@ -345,24 +346,24 @@ tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
, psb_def = lpat, psb_dir = dir }
TPSI{ patsig_implicit_bndrs = implicit_bndrs
- , patsig_univ_bndrs = explicit_univ_bndrs, patsig_prov = prov_theta
- , patsig_ex_bndrs = explicit_ex_bndrs, patsig_req = req_theta
+ , patsig_univ_bndrs = explicit_univ_bndrs, patsig_req = req_theta
+ , patsig_ex_bndrs = explicit_ex_bndrs, patsig_prov = prov_theta
, patsig_body_ty = sig_body_ty }
= addPatSynCtxt lname $
- do { let decl_arity = length arg_names
- (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
-
- ; traceTc "tcCheckPatSynDecl" $
+ do { traceTc "tcCheckPatSynDecl" $
vcat [ ppr implicit_bndrs, ppr explicit_univ_bndrs, ppr req_theta
, ppr explicit_ex_bndrs, ppr prov_theta, ppr sig_body_ty ]
+ ; let decl_arity = length arg_names
+ (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
+
; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
Right stuff -> return stuff
Left missing -> wrongNumberOfParmsErr name decl_arity missing
-- Complain about: pattern P :: () => forall x. x -> P x
-- The existential 'x' should not appear in the result type
- -- Can't check this until we know P's arity
+ -- Can't check this until we know P's arity (decl_arity above)
; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) $ binderVars explicit_ex_bndrs
; checkTc (null bad_tvs) $
hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
@@ -379,36 +380,55 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
univ_tvs = binderVars univ_bndrs
ex_tvs = binderVars ex_bndrs
+ -- Skolemise the quantified type variables. This is necessary
+ -- in order to check the actual pattern type against the
+ -- expected type. Even though the tyvars in the type are
+ -- already skolems, this step changes their TcLevels,
+ -- avoiding level-check errors when unifying.
+ ; (skol_subst0, skol_univ_bndrs) <- skolemiseTvBndrsX emptyTCvSubst univ_bndrs
+ ; (skol_subst, skol_ex_bndrs) <- skolemiseTvBndrsX skol_subst0 ex_bndrs
+ ; let skol_univ_tvs = binderVars skol_univ_bndrs
+ skol_ex_tvs = binderVars skol_ex_bndrs
+ skol_req_theta = substTheta skol_subst0 req_theta
+ skol_prov_theta = substTheta skol_subst prov_theta
+ skol_arg_tys = substTys skol_subst (map scaledThing arg_tys)
+ skol_pat_ty = substTy skol_subst pat_ty
+
+ univ_tv_prs = [ (getName orig_univ_tv, skol_univ_tv)
+ | (orig_univ_tv, skol_univ_tv) <- univ_tvs `zip` skol_univ_tvs ]
+
-- Right! Let's check the pattern against the signature
-- See Note [Checking against a pattern signature]
- ; req_dicts <- newEvVars req_theta
+ ; req_dicts <- newEvVars skol_req_theta
; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
pushLevelAndCaptureConstraints $
- tcExtendTyVarEnv univ_tvs $
- tcCheckPat PatSyn lpat (unrestricted pat_ty) $
- do { let in_scope = mkInScopeSet (mkVarSet univ_tvs)
+ tcExtendNameTyVarEnv univ_tv_prs $
+ tcCheckPat PatSyn lpat (unrestricted skol_pat_ty) $
+ do { let in_scope = mkInScopeSet (mkVarSet skol_univ_tvs)
empty_subst = mkEmptyTCvSubst in_scope
- ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
+ ; (inst_subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst skol_ex_tvs
-- newMetaTyVarX: see the "Existential type variables"
-- part of Note [Checking against a pattern signature]
; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
- ; let prov_theta' = substTheta subst prov_theta
+ ; let prov_theta' = substTheta inst_subst skol_prov_theta
-- Add univ_tvs to the in_scope set to
-- satisfy the substitution invariant. There's no need to
-- add 'ex_tvs' as they are already in the domain of the
-- substitution.
-- See also Note [The substitution invariant] in GHC.Core.TyCo.Subst.
; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
- ; args' <- zipWithM (tc_arg subst) arg_names (map scaledThing arg_tys)
+ ; args' <- zipWithM (tc_arg inst_subst) arg_names
+ skol_arg_tys
; return (ex_tvs', prov_dicts, args') }
; let skol_info = SigSkol (PatSynCtxt name) pat_ty []
-- The type here is a bit bogus, but we do not print
-- the type for PatSynCtxt, so it doesn't matter
-- See Note [Skolem info for pattern synonyms] in "GHC.Tc.Types.Origin"
- ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
+ ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_univ_tvs
+ req_dicts wanted
-- Solve the constraints now, because we are about to make a PatSyn,
-- which should not contain unification variables and the like (#10997)
@@ -419,11 +439,12 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
-- when that should be impossible
; traceTc "tcCheckPatSynDecl }" $ ppr name
+
; tc_patsyn_finish lname dir is_infix lpat'
- (univ_bndrs, req_theta, ev_binds, req_dicts)
- (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
- (args', map scaledThing arg_tys)
- pat_ty rec_fields }
+ (skol_univ_bndrs, skol_req_theta, ev_binds, req_dicts)
+ (skol_ex_bndrs, mkTyVarTys ex_tvs', skol_prov_theta, prov_dicts)
+ (args', skol_arg_tys)
+ skol_pat_ty rec_fields }
where
tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTc)
-- Look up the variable actually bound by lpat
@@ -440,13 +461,50 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
do { arg_id <- tcLookupId arg_name
; wrap <- tcSubTypeSigma GenSigCtxt
(idType arg_id)
- (substTyUnchecked subst arg_ty)
+ (substTy subst arg_ty)
-- Why do we need tcSubType here?
-- See Note [Pattern synonyms and higher rank types]
; return (mkLHsWrap wrap $ nlHsVar arg_id) }
-{- [Pattern synonyms and higher rank types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+skolemiseTvBndrsX :: TCvSubst -> [VarBndr TyVar flag]
+ -> TcM (TCvSubst, [VarBndr TcTyVar flag])
+-- Make new TcTyVars, all skolems with levels, but do not clone
+-- The level is one level deeper than the current level
+-- See Note [Skolemising when checking a pattern synonym]
+skolemiseTvBndrsX orig_subst tvs
+ = do { tc_lvl <- getTcLevel
+ ; let pushed_lvl = pushTcLevel tc_lvl
+ details = SkolemTv pushed_lvl False
+
+ mk_skol_tv_x :: TCvSubst -> VarBndr TyVar flag
+ -> (TCvSubst, VarBndr TcTyVar flag)
+ mk_skol_tv_x subst (Bndr tv flag)
+ = (subst', Bndr new_tv flag)
+ where
+ new_kind = substTyUnchecked subst (tyVarKind tv)
+ new_tv = mkTcTyVar (tyVarName tv) new_kind details
+ subst' = extendTvSubstWithClone subst tv new_tv
+
+ ; return (mapAccumL mk_skol_tv_x orig_subst tvs) }
+
+{- Note [Skolemising when checking a pattern synonym]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ pattern P1 :: forall a. a -> Maybe a
+ pattern P1 x <- Just x where
+ P1 x = Just (x :: a)
+
+The scoped type variable 'a' scopes over the builder RHS, Just (x::a).
+But the builder RHS is typechecked much later in tcPatSynBuilderBind,
+and gets its scoped type variables from the type of the builder_id.
+The easiest way to achieve this is not to clone when skolemising.
+
+Hence a special-purpose skolemiseTvBndrX here, similar to
+GHC.Tc.Utils.Instantiate.tcInstSkolTyVarsX except that the latter
+does cloning.
+
+[Pattern synonyms and higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data T = MkT (forall a. a->a)
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 71f628aa3a..308569ace0 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -35,7 +35,7 @@ module GHC.Tc.Types.Constraint (
isDroppableCt, insolubleImplic,
arisesFromGivens,
- Implication(..), implicationPrototype,
+ Implication(..), implicationPrototype, checkTelescopeSkol,
ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
bumpSubGoalDepth, subGoalDepthExceeded,
@@ -1176,8 +1176,8 @@ data ImplicStatus
| IC_Insoluble -- At least one insoluble constraint in the tree
- | IC_BadTelescope -- solved, but the skolems in the telescope are out of
- -- dependency order
+ | IC_BadTelescope -- Solved, but the skolems in the telescope are out of
+ -- dependency order. See Note [Checking telescopes]
| IC_Unsolved -- Neither of the above; might go either way
@@ -1207,6 +1207,11 @@ instance Outputable ImplicStatus where
ppr (IC_Solved { ics_dead = dead })
= text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead))
+checkTelescopeSkol :: SkolemInfo -> Bool
+-- See Note [Checking telescopes]
+checkTelescopeSkol (ForAllSkol {}) = True
+checkTelescopeSkol _ = False
+
{- Note [Checking telescopes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When kind-checking a /user-written/ type, we might have a "bad telescope"
@@ -1241,7 +1246,7 @@ all at once, creating one implication constraint for the lot:
that binds existentials, where the type of the data constructor is
known to be valid (it in tcConPat), no need for the check.
- So the check is done if and only if ic_info is ForAllSkol
+ So the check is done /if and only if/ ic_info is ForAllSkol.
* If ic_info is (ForAllSkol dt dvs), the dvs::SDoc displays the
original, user-written type variables.
@@ -1251,6 +1256,18 @@ all at once, creating one implication constraint for the lot:
constraint solver a chance to make that bad-telescope test! Hence
the extra guard in emitResidualTvConstraint; see #16247
+* Don't mix up inferred and explicit variables in the same implication
+ constraint. E.g.
+ foo :: forall a kx (b :: kx). SameKind a b
+ We want an implication
+ Implic { ic_skol = [(a::kx), kx, (b::kx)], ... }
+ but GHC will attempt to quantify over kx, since it is free in (a::kx),
+ and it's hopelessly confusing to report an error about quantified
+ variables kx (a::kx) kx (b::kx).
+ Instead, the outer quantification over kx should be in a separate
+ implication. TL;DR: an explicit forall should generate an implication
+ quantified only over those explicitly quantified variables.
+
Note [Needed evidence variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Th ic_need_evs field holds the free vars of ic_binds, and all the
@@ -1277,14 +1294,30 @@ worrying that 'b' might clash.
Note [Skolems in an implication]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The skolems in an implication are not there to perform a skolem escape
-check. That happens because all the environment variables are in the
-untouchables, and therefore cannot be unified with anything at all,
-let alone the skolems.
-
-Instead, ic_skols is used only when considering floating a constraint
-outside the implication in GHC.Tc.Solver.floatEqualities or
-GHC.Tc.Solver.approximateImplications
+The skolems in an implication are used:
+
+* When considering floating a constraint outside the implication in
+ GHC.Tc.Solver.floatEqualities or GHC.Tc.Solver.approximateImplications
+ For this, we can treat ic_skols as a set.
+
+* When checking that a /user-specified/ forall (ic_info = ForAllSkol tvs)
+ has its variables in the correct order; see Note [Checking telescopes].
+ Only for these implications does ic_skols need to be a list.
+
+Nota bene: Although ic_skols is a list, it is not necessarily
+in dependency order:
+- In the ic_info=ForAllSkol case, the user might have written them
+ in the wrong order
+- In the case of a type signature like
+ f :: [a] -> [b]
+ the renamer gathers the implicit "outer" forall'd variables {a,b}, but
+ does not know what order to put them in. The type checker can sort them
+ into dependency order, but only after solving all the kind constraints;
+ and to do that it's convenient to create the Implication!
+
+So we accept that ic_skols may be out of order. Think of it as a set or
+(in the case of ic_info=ForAllSkol, a list in user-specified, and possibly
+wrong, order.
Note [Insoluble constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index d836b8d947..b47d4319dd 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -184,7 +184,6 @@ data SkolemInfo
-- hence, we have less info
| ForAllSkol -- Bound by a user-written "forall".
- SDoc -- Shows the entire forall type
SDoc -- Shows just the binders, used when reporting a bad telescope
-- See Note [Checking telescopes] in GHC.Tc.Types.Constraint
@@ -244,7 +243,7 @@ pprSkolInfo :: SkolemInfo -> SDoc
-- Complete the sentence "is a rigid type variable bound by..."
pprSkolInfo (SigSkol cx ty _) = pprSigSkolInfo cx ty
pprSkolInfo (SigTypeSkol cx) = pprUserTypeCtxt cx
-pprSkolInfo (ForAllSkol pt _) = quotes pt
+pprSkolInfo (ForAllSkol tvs) = text "an explicit forall" <+> tvs
pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural ips <+> text "for"
<+> pprWithCommas ppr ips
pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred)
@@ -304,7 +303,7 @@ For pattern synonym SkolemInfo we have
but the type 'ty' is not very helpful. The full pattern-synonym type
has the provided and required pieces, which it is inconvenient to
record and display here. So we simply don't display the type at all,
-contenting outselves with just the name of the pattern synonym, which
+contenting ourselves with just the name of the pattern synonym, which
is fine. We could do more, but it doesn't seem worth it.
Note [SigSkol SkolemInfo]
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index 61d0cdcd47..199fb57cc6 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -734,8 +734,8 @@ tcAddDataFamConPlaceholders inst_decls thing_inside
= concatMap (get_fi_cons . unLoc) fids
get_fi_cons :: DataFamInstDecl GhcRn -> [Name]
- get_fi_cons (DataFamInstDecl { dfid_eqn = HsIB { hsib_body =
- FamEqn { feqn_rhs = HsDataDefn { dd_cons = cons } }}})
+ get_fi_cons (DataFamInstDecl { dfid_eqn =
+ FamEqn { feqn_rhs = HsDataDefn { dd_cons = cons } }})
= map unLoc $ concatMap (getConNames . unLoc) cons
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index 6940d161d6..c2140f7deb 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -491,7 +491,7 @@ tcInstTypeBndrs id
tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type signature with skolem constants.
--- We could give them fresh names, but no need to do so
+-- This freshens the names, but no need to do so
tcSkolDFunType dfun
= do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
; return (map snd tv_prs, theta, tau) }
@@ -523,13 +523,18 @@ tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- See Note [Skolemising type variables]
+-- This version freshens the names and creates "super skolems";
+-- see comments around superSkolemTv.
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- See Note [Skolemising type variables]
+-- This version freshens the names and creates "super skolems";
+-- see comments around superSkolemTv.
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
-tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar]
+tcInstSkolTyVarsPushLevel :: Bool -- True <=> make "super skolem"
+ -> TCvSubst -> [TyVar]
-> TcM (TCvSubst, [TcTyVar])
-- Skolemise one level deeper, hence pushTcLevel
-- See Note [Skolemising type variables]
@@ -598,10 +603,22 @@ a) Level allocation. We generally skolemise /before/ calling
b) The [TyVar] should be ordered (kind vars first)
See Note [Kind substitution when instantiating]
-c) It's a complete freshening operation: the skolems have a fresh
- unique, and a location from the monad
-
-d) The resulting skolems are
+c) Clone the variable to give a fresh unique. This is essential.
+ Consider (tc160)
+ type Foo x = forall a. a -> x
+ And typecheck the expression
+ (e :: Foo (Foo ())
+ We will skolemise the signature, but after expanding synonyms it
+ looks like
+ forall a. a -> forall a. a -> x
+ We don't want to make two big-lambdas with the same unique!
+
+d) We retain locations. Because the location of the variable is the correct
+ location to report in errors (e.g. in the signature). We don't want the
+ location to change to the body of the function, which does *not* explicitly
+ bind the variable.
+
+e) The resulting skolems are
non-overlappable for tcInstSkolTyVars,
but overlappable for tcInstSuperSkolTyVars
See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index a040cca093..de3c4aeb01 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -1845,8 +1845,8 @@ It's distressingly delicate though:
the visible type application fails in the monad (throws an exception).
We must not discard the out-of-scope error.
- Also GHC.Tc.Solver.emitFlatConstraints may fail having emitted some
- constraints with skolem-escape problems.
+ Also GHC.Tc.Solver.simplifyAndEmitFlatConstraints may fail having
+ emitted some constraints with skolem-escape problems.
* If we discard too /few/ constraints, we may get the misleading
class constraints mentioned above. But we may /also/ end up taking
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index d704bcbf8f..4b0a5f8fdd 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -927,13 +927,18 @@ checkTvConstraints skol_info skol_tvs thing_inside
emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint skol_info skol_tvs tclvl wanted
- | isEmptyWC wanted
- = return ()
-
- | otherwise
- = do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
+ | not (isEmptyWC wanted) ||
+ checkTelescopeSkol skol_info
+ = -- checkTelescopeSkol: in this case, /always/ emit this implication
+ -- even if 'wanted' is empty. We need the implication so that we check
+ -- for a bad telescope. See Note [Skolem escape and forall-types] in
+ -- GHC.Tc.Gen.HsType
+ do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
; emitImplication implic }
+ | otherwise -- Empty 'wanted', emit nothing
+ = return ()
+
buildTvImplication :: SkolemInfo -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication skol_info skol_tvs tclvl wanted
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 5f08249e38..68ef82785d 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -2855,7 +2855,7 @@ at all in the kind -- after all, it is Specified so it must have
occurred. (It /used/ to be possible; see tests T13983 and T7873. But
with the advent of the forall-or-nothing rule for kind variables,
those strange cases went away. See Note [forall-or-nothing rule] in
-GHC.Rename.HsType.)
+GHC.Hs.Type.)
But one might worry about
type v k = *
View Lorry Controller Status