summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2020-07-16 14:35:42 +0100
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-09-24 13:16:32 -0400
commit9fa26aa16f9eee0b56b5d9e65c16367d7b789996 (patch)
treea7b27876018129d93bdb3e91f7b1762e30e37f5b /compiler/GHC/Tc
parent97cff9190d346c3b51c32c88fd145fcf1e6678f1 (diff)
downloadhaskell-9fa26aa16f9eee0b56b5d9e65c16367d7b789996.tar.gz
Improve kind generalisation, error messages
This patch does two things: * It refactors GHC.Tc.Errors a bit. In debugging Quick Look I was forced to look in detail at error messages, and ended up doing a bit of refactoring, esp in mkTyVarEqErr'. It's still quite a mess, but a bit better, I think. * It makes a significant improvement to the kind checking of type and class declarations. Specifically, we now ensure that if kind checking fails with an unsolved constraint, all the skolems are in scope. That wasn't the case before, which led to some obscure error messages; and occasional failures with "no skolem info" (eg #16245). Both of these, and the main Quick Look patch itself, affect a /lot/ of error messages, as you can see from the number of files changed. I've checked them all; I think they are as good or better than before. Smaller things * I documented the various instances of VarBndr better. See Note [The VarBndr tyep and its uses] in GHC.Types.Var * Renamed GHC.Tc.Solver.simpl_top to simplifyTopWanteds * A bit of refactoring in bindExplicitTKTele, to avoid the footwork with Either. Simpler now. * Move promoteTyVar from GHC.Tc.Solver to GHC.Tc.Utils.TcMType Fixes #16245 (comment 211369), memorialised as typecheck/polykinds/T16245a Also fixes the three bugs in #18640
Diffstat (limited to 'compiler/GHC/Tc')
-rw-r--r--compiler/GHC/Tc/Errors.hs72
-rw-r--r--compiler/GHC/Tc/Errors/Hole.hs4
-rw-r--r--compiler/GHC/Tc/Gen/Default.hs2
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs382
-rw-r--r--compiler/GHC/Tc/Gen/Sig.hs89
-rw-r--r--compiler/GHC/Tc/Gen/Splice.hs14
-rw-r--r--compiler/GHC/Tc/Module.hs17
-rw-r--r--compiler/GHC/Tc/Solver.hs224
-rw-r--r--compiler/GHC/Tc/TyCl.hs203
-rw-r--r--compiler/GHC/Tc/TyCl/Instance.hs27
-rw-r--r--compiler/GHC/Tc/Types/Constraint.hs18
-rw-r--r--compiler/GHC/Tc/Types/Evidence.hs4
-rw-r--r--compiler/GHC/Tc/Utils/Monad.hs31
-rw-r--r--compiler/GHC/Tc/Utils/TcMType.hs114
14 files changed, 673 insertions, 528 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index d597c95b72..93c047ca32 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -69,7 +69,7 @@ import GHC.Utils.FV ( fvVarList, unionFV )
import Control.Monad ( when )
import Data.Foldable ( toList )
-import Data.List ( partition, mapAccumL, nub, sortBy, unfoldr )
+import Data.List ( partition, mapAccumL, sortBy, unfoldr )
import {-# SOURCE #-} GHC.Tc.Errors.Hole ( findValidHoleFits )
@@ -215,7 +215,13 @@ report_unsolved type_errors expr_holes
-- If we are deferring we are going to need /all/ evidence around,
-- including the evidence produced by unflattening (zonkWC)
; let tidy_env = tidyFreeTyCoVars emptyTidyEnv free_tvs
- free_tvs = tyCoVarsOfWCList wanted
+ free_tvs = filterOut isCoVar $
+ tyCoVarsOfWCList wanted
+ -- tyCoVarsOfWC returns free coercion *holes*, even though
+ -- they are "bound" by other wanted constraints. They in
+ -- turn may mention variables bound further in, which makes
+ -- no sense. Really we should not return those holes at all;
+ -- for now we just filter them out.
; traceTc "reportUnsolved (after zonking):" $
vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
@@ -832,7 +838,11 @@ eq_lhs_type ct1 ct2
_ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
cmp_loc :: Ct -> Ct -> Ordering
-cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
+cmp_loc ct1 ct2 = get ct1 `compare` get ct2
+ where
+ get ct = realSrcSpanStart (ctLocSpan (ctLoc ct))
+ -- Reduce duplication by reporting only one error from each
+ -- /starting/ location even if the end location differs
reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter
reportGroup mk_err ctxt cts =
@@ -1451,14 +1461,15 @@ mkTyVarEqErr dflags ctxt report ct tv1 ty2
; mkTyVarEqErr' dflags ctxt report ct tv1 ty2 }
mkTyVarEqErr' dflags ctxt report ct tv1 ty2
- | isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar; we would have
- -- swapped in Solver.Canonical.canEqTyVarHomo
+ | isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar; we would have
+ -- swapped in Solver.Canonical.canEqTyVarHomo
|| isTyVarTyVar tv1 && not (isTyVarTy ty2)
|| ctEqRel ct == ReprEq
-- The cases below don't really apply to ReprEq (except occurs check)
= mkErrorMsgFromCt ctxt ct $ mconcat
[ headline_msg
, extraTyVarEqInfo ctxt tv1 ty2
+ , suggestAddSig ctxt ty1 ty2
, report
]
@@ -1594,17 +1605,6 @@ mkEqInfoMsg ct ty1 ty2
<+> text "is a non-injective type family"
| otherwise = empty
-isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool
--- See Note [Reporting occurs-check errors]
-isUserSkolem ctxt tv
- = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt)
- where
- is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info })
- = tv `elem` sks && is_user_skol_info skol_info
-
- is_user_skol_info (InferSkol {}) = False
- is_user_skol_info _ = True
-
misMatchOrCND :: Bool -> ReportErrCtxt -> Ct
-> TcType -> TcType -> Report
-- If oriented then ty1 is actual, ty2 is expected
@@ -1724,21 +1724,29 @@ extraTyVarInfo ctxt tv
suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> Report
-- See Note [Suggest adding a type signature]
-suggestAddSig ctxt ty1 ty2
- | null inferred_bndrs
+suggestAddSig ctxt ty1 _ty2
+ | null inferred_bndrs -- No let-bound inferred binders in context
= mempty
| [bndr] <- inferred_bndrs
= important $ text "Possible fix: add a type signature for" <+> quotes (ppr bndr)
| otherwise
= important $ text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs)
where
- inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
- get_inf ty | Just tv <- tcGetTyVar_maybe ty
- , isSkolemTyVar tv
- , ((InferSkol prs, _) : _) <- getSkolemInfo (cec_encl ctxt) [tv]
- = map fst prs
- | otherwise
- = []
+ inferred_bndrs = case tcGetTyVar_maybe ty1 of
+ Just tv | isSkolemTyVar tv -> find (cec_encl ctxt) False tv
+ _ -> []
+
+ -- 'find' returns the binders of an InferSkol for 'tv',
+ -- provided there is an intervening implication with
+ -- ic_no_eqs = False (i.e. a GADT match)
+ find [] _ _ = []
+ find (implic:implics) seen_eqs tv
+ | tv `elem` ic_skols implic
+ , InferSkol prs <- ic_info implic
+ , seen_eqs
+ = map fst prs
+ | otherwise
+ = find implics (seen_eqs || not (ic_no_eqs implic)) tv
--------------------
misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report
@@ -2183,9 +2191,8 @@ sameOccExtra ty1 ty2
mod = nameModule nm
loc = nameSrcSpan nm
-{-
-Note [Suggest adding a type signature]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Suggest adding a type signature]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The OutsideIn algorithm rejects GADT programs that don't have a principal
type, and indeed some that do. Example:
data T a where
@@ -2199,6 +2206,15 @@ untouchable type variable. So suggestAddSig sees if the offending
type variable is bound by an *inferred* signature, and suggests
adding a declared signature instead.
+More specifically, we suggest adding a type sig if we have p ~ ty, and
+p is a skolem bound by an InferSkol. Those skolems were created from
+unification variables in simplifyInfer. Why didn't we unify? It must
+have been because of an intervening GADT or existential, making it
+untouchable. Either way, a type signature would help. For GADTs, it
+might make it typeable; for existentials the attempt to write a
+signature will fail -- or at least will produce a better error message
+next time
+
This initially came up in #8968, concerning pattern synonyms.
Note [Disambiguating (X ~ X) errors]
diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs
index 06a75e2a1f..3ff2312903 100644
--- a/compiler/GHC/Tc/Errors/Hole.hs
+++ b/compiler/GHC/Tc/Errors/Hole.hs
@@ -44,7 +44,7 @@ import Data.List ( partition, sort, sortOn, nubBy )
import Data.Graph ( graphFromEdges, topSort )
-import GHC.Tc.Solver ( simpl_top, runTcSDeriveds )
+import GHC.Tc.Solver ( simplifyTopWanteds, runTcSDeriveds )
import GHC.Tc.Utils.Unify ( tcSubTypeSigma )
import GHC.HsToCore.Docs ( extractDocs )
@@ -957,7 +957,7 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
w_rel_cts = addSimples wanted cloned_relevants
final_wc = foldr (setWCAndBinds fresh_binds) w_rel_cts outermost_first
; traceTc "final_wc is: " $ ppr final_wc
- ; rem <- runTcSDeriveds $ simpl_top final_wc
+ ; rem <- runTcSDeriveds $ simplifyTopWanteds final_wc
-- We don't want any insoluble or simple constraints left, but
-- solved implications are ok (and necessary for e.g. undefined)
; traceTc "rems was:" $ ppr rem
diff --git a/compiler/GHC/Tc/Gen/Default.hs b/compiler/GHC/Tc/Gen/Default.hs
index 1bd06ddc63..d37f26df40 100644
--- a/compiler/GHC/Tc/Gen/Default.hs
+++ b/compiler/GHC/Tc/Gen/Default.hs
@@ -71,7 +71,7 @@ tcDefaults decls@(L locn (DefaultDecl _ _) : _)
tc_default_ty :: [Class] -> LHsType GhcRn -> TcM Type
tc_default_ty deflt_clss hs_ty
- = do { ty <- solveEqualities $
+ = do { ty <- solveEqualities "tc_default_ty" $
tcInferLHsType hs_ty
; ty <- zonkTcTypeToType ty -- establish Type invariants
; checkValidType DefaultDeclCtxt ty
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 550d859c81..9c778a1b4b 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -49,8 +49,6 @@ module GHC.Tc.Gen.HsType (
tcInferLHsTypeKind, tcInferLHsType, tcInferLHsTypeUnsaturated,
tcCheckLHsType,
tcHsMbContext, tcHsContext, tcLHsPredType,
- failIfEmitsConstraints,
- solveEqualities, -- useful re-export
kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
@@ -87,7 +85,6 @@ import GHC.Tc.Solver
import GHC.Tc.Utils.Zonk
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
-import GHC.Tc.Errors ( reportAllUnsolved )
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBindersN, tcInstInvisibleTyBinder )
import GHC.Core.Type
@@ -187,43 +184,122 @@ these variables.
Note [Recipe for checking a signature]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Checking a user-written signature requires several steps:
+Kind-checking a user-written signature requires several steps:
- 1. Generate constraints.
- 2. Solve constraints.
- 3. Promote tyvars and/or kind-generalize.
- 4. Zonk.
- 5. Check validity.
+ 0. Bump the TcLevel
+ 1. Bind any lexically-scoped type variables.
+ 2. Generate constraints.
+ 3. Solve constraints.
+ 4. Sort any implicitly-bound variables into dependency order
+ 5. Promote tyvars and/or kind-generalize.
+ 6. Zonk.
+ 7. Check validity.
-There may be some surprises in here:
+Very similar steps also apply when kind-checking a type or class
+declaration.
-Step 2 is necessary for two reasons: most signatures also bring
-implicitly quantified variables into scope, and solving is necessary
-to get these in the right order (see Note [Keeping implicitly
-quantified variables in order]). Additionally, solving is necessary in
-order to kind-generalize correctly: otherwise, we do not know which
-metavariables are left unsolved.
+The general pattern looks something like this. (But NB every
+specific instance varies in one way or another!)
-Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to
-kindGeneralize{All,Some,None}. Here, we have to deal with the fact that
-metatyvars generated in the type may have a bumped TcLevel, because explicit
-foralls raise the TcLevel. To avoid these variables from ever being visible in
-the surrounding context, we must obey the following dictum:
+ do { (tclvl, wanted, (spec_tkvs, ty))
+ <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
+ bindImplicitTKBndrs_Skol sig_vars $
+ <kind-check the type>
+
+ ; spec_tkvs <- zonkAndScopedSort spec_tkvs
+
+ ; reportUnsolvedEqualities skol_info spec_tkvs tclvl wanted
+
+ ; let ty1 = mkSpecForAllTys spec_tkvs ty
+ ; kvs <- kindGeneralizeAll ty1
+
+ ; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)
+
+ ; checkValidType final_ty
+
+This pattern is repeated many times in GHC.Tc.Gen.HsType,
+GHC.Tc.Gen.Sig, and GHC.Tc.TyCl, with variations. In more detail:
+
+* pushLevelAndSolveEqualitiesX (Step 0, step 3) bumps the TcLevel,
+ calls the thing inside to generate constraints, solves those
+ constraints as much as possible, returning the residual unsolved
+ constraints in 'wanted'.
+
+* bindImplicitTKBndrs_Skol (Step 1) binds the user-specified type
+ variables E.g. when kind-checking f :: forall a. F a -> a we must
+ bring 'a' into scope before kind-checking (F a -> a)
+
+* zonkAndScopedSort (Step 4) puts those user-specified variables in
+ the dependency order. (For "implicit" variables the order is no
+ user-specified. E.g. forall (a::k1) (b::k2). blah k1 and k2 are
+ implicitly brought into scope.
+
+* reportUnsolvedEqualities (Step 3 continued) reports any unsolved
+ equalities, carefully wrapping them in an implication that binds the
+ skolems. We can't do that in pushLevelAndSolveEqualitiesX because
+ that function doesn't have access to the skolems.
+
+* kindGeneralize (Step 5). See Note [Kind generalisation]
+
+* The final zonkTcTypeToType must happen after promoting/generalizing,
+ because promoting and generalizing fill in metavariables.
+
+
+Doing Step 3 (constraint solving) eagerly (rather than building an
+implication constraint and solving later) is necessary for several
+reasons:
+
+* Exactly as for Solver.simplifyInfer: when generalising, we solve all
+ the constraints we can so that we don't have to quantify over them
+ or, since we don't quantify over constraints in kinds, float them
+ and inhibit generalisation.
+
+* Most signatures also bring implicitly quantified variables into
+ scope, and solving is necessary to get these in the right order
+ (Step 4) see Note [Keeping implicitly quantified variables in
+ order]).
+
+Note [Kind generalisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Step 5 of Note [Recipe for checking a signature], namely
+kind-generalisation, is done by
+ kindGeneraliseAll
+ kindGeneraliseSome
+ kindGeneraliseNone
+
+Here, we have to deal with the fact that metatyvars generated in the
+type will have a bumped TcLevel, because explicit foralls raise the
+TcLevel. To avoid these variables from ever being visible in the
+surrounding context, we must obey the following dictum:
Every metavariable in a type must either be
(A) generalized, or
(B) promoted, or See Note [Promotion in signatures]
- (C) a cause to error See Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType
+ (C) a cause to error See Note [Naughty quantification candidates]
+ in GHC.Tc.Utils.TcMType
+
+There are three steps (look at kindGeneraliseSome):
+
+1. candidateQTyVarsOfType finds the free variables of the type or kind,
+ to generalise
+
+2. filterConstrainedCandidates filters out candidates that appear
+ in the unsolved 'wanteds', and promotes the ones that get filtered out
+ thereby.
+
+3. quantifyTyVars quantifies the remaining type variables
The kindGeneralize functions do not require pre-zonking; they zonk as they
go.
-If you are actually doing kind-generalization, you need to bump the level
-before generating constraints, as we will only generalize variables with
-a TcLevel higher than the ambient one.
+kindGeneraliseAll specialises for the case where step (2) is vacuous.
+kindGeneraliseNone specialises for the case where we do no quantification,
+but we must still promote.
-After promoting/generalizing, we need to zonk again because both
-promoting and generalizing fill in metavariables.
+If you are actually doing kind-generalization, you need to bump the
+level before generating constraints, as we will only generalize
+variables with a TcLevel higher than the ambient one.
+Hence the "pushLevel" in pushLevelAndSolveEqualities.
Note [Promotion in signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -301,10 +377,9 @@ kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
kcClassSigType skol_info names (HsIB { hsib_ext = sig_vars
, hsib_body = hs_ty })
= addSigCtxt (funsSigCtxt names) hs_ty $
- do { (tc_lvl, (wanted, (spec_tkvs, _)))
- <- pushTcLevelM $
- solveLocalEqualitiesX "kcClassSigType" $
- bindImplicitTKBndrs_Skol sig_vars $
+ do { (tc_lvl, wanted, (spec_tkvs, _))
+ <- pushLevelAndSolveEqualitiesX "kcClassSigType" $
+ bindImplicitTKBndrs_Skol sig_vars $
tcLHsType hs_ty liftedTypeKind
; emitResidualTvConstraint skol_info spec_tkvs tc_lvl wanted }
@@ -364,27 +439,19 @@ tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
-- 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)))
- <- pushTcLevelM $
- solveLocalEqualitiesX "tc_hs_sig_type" $
+ = do { (tc_lvl, wanted, (spec_tkvs, ty))
+ <- pushLevelAndSolveEqualitiesX "tc_hs_sig_type" $
-- See Note [Failure in local type signatures]
bindImplicitTKBndrs_Skol sig_vars $
do { kind <- newExpectedKind ctxt_kind
; tcLHsType hs_ty kind }
- -- Any remaining variables (unsolved in the solveLocalEqualities)
+ -- 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
- -- This bit is very much like decideMonoTyVars in GHC.Tc.Solver,
- -- but constraints are so much simpler in kinds, it is much
- -- easier here. (In particular, we never quantify over a
- -- constraint in a type.)
- ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
- ; let should_gen = not . (`elemVarSet` constrained)
-
- ; kvs <- kindGeneralizeSome should_gen ty1
+ ; kvs <- kindGeneralizeSome wanted ty1
-- Build an implication for any as-yet-unsolved kind equalities
-- See Note [Skolem escape in type signatures]
@@ -448,16 +515,18 @@ tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
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)
- ; (spec_tkvs, ty)
- <- pushTcLevelM_ $
- solveEqualities $
- bindImplicitTKBndrs_Skol sig_vars $
+ ; (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 -- "All" because it's a top-level type
+ ; kvs <- kindGeneralizeAll ty1
+
; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)
; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty])
; return final_ty}
@@ -533,7 +602,7 @@ tcHsTypeApp wc_ty kind
= do { mode <- mkHoleMode TypeLevel HM_VTA
-- HM_VTA: See Note [Wildcards in visible type application]
; ty <- addTypeCtxt hs_ty $
- solveLocalEqualities "tcHsTypeApp" $
+ 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 $ \ _ ->
@@ -985,8 +1054,9 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) 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 $
- bindExplicitTKTele_Skol_M mode tele $
+ <- 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
-- e.g. f :: _ -> Int -> forall (a :: _). blah
@@ -1000,22 +1070,15 @@ tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
map ppr hs_tvs
HsForAllInvis { hsf_invis_bndrs = hs_tvs } ->
map ppr hs_tvs
- tv_bndrs' = construct_bndrs tv_bndrs
- skol_tvs = binderVars tv_bndrs'
+ 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') }
- where
- construct_bndrs :: Either [TcReqTVBinder] [TcInvisTVBinder]
- -> [TcTyVarBinder]
- construct_bndrs (Left req_tv_bndrs) =
- map (mkTyVarBinder Required . binderVar) req_tv_bndrs
- construct_bndrs (Right inv_tv_bndrs) =
- map tyVarSpecToBinder inv_tv_bndrs
+ ; return (mkForAllTys tv_bndrs ty') }
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
| null (unLoc ctxt)
@@ -2194,11 +2257,10 @@ kcCheckDeclHeader_cusk name flav
-- CUSK case
-- See note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
= addTyConFlavCtxt name flav $
- do { (scoped_kvs, (tc_tvs, res_kind))
- <- pushTcLevelM_ $
- solveEqualities $
- bindImplicitTKBndrs_Q_Skol kv_ns $
- bindExplicitTKBndrs_Q_Skol ctxt_kind hs_tvs $
+ do { (tclvl, wanted, (scoped_kvs, (tc_tvs, res_kind)))
+ <- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_cusk" $
+ bindImplicitTKBndrs_Q_Skol kv_ns $
+ bindExplicitTKBndrs_Q_Skol ctxt_kind hs_tvs $
newExpectedKind =<< kc_res_ki
-- Now, because we're in a CUSK,
@@ -2234,6 +2296,10 @@ kcCheckDeclHeader_cusk name flav
tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs
True -- it is generalised
flav
+
+ ; reportUnsolvedEqualities skol_info (binderVars final_tc_binders)
+ tclvl wanted
+
-- If the ordering from
-- Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl
-- doesn't work, we catch it here, before an error cascade
@@ -2256,6 +2322,7 @@ kcCheckDeclHeader_cusk name flav
; return tycon }
where
+ skol_info = TyConSkol flav name
ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
| otherwise = AnyKind
@@ -2358,11 +2425,10 @@ kcCheckDeclHeader_sig kisig name flav
-- and to [(Name, TcTyVar)] for tcTyConScopedTyVars
; (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders
- ; (implicit_tvs, (invis_binders, r_ki))
- <- pushTcLevelM_ $
- solveEqualities $ -- #16687
- bindImplicitTKBndrs_Tv implicit_nms $
- tcExtendNameTyVarEnv explicit_tv_prs $
+ ; (tclvl, wanted, (implicit_tvs, (invis_binders, r_ki)))
+ <- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_sig" $ -- #16687
+ bindImplicitTKBndrs_Tv implicit_nms $
+ tcExtendNameTyVarEnv explicit_tv_prs $
do { -- Check that inline kind annotations on binders are valid.
-- For example:
--
@@ -2416,7 +2482,11 @@ kcCheckDeclHeader_sig kisig name flav
; let tcbs = vis_tcbs ++ invis_tcbs
implicit_tv_prs = implicit_nms `zip` implicit_tvs
all_tv_prs = implicit_tv_prs ++ explicit_tv_prs
- tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav
+ tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav
+ skol_info = TyConSkol flav name
+
+ -- Check that there are no unsolved equalities
+ ; reportUnsolvedEqualities skol_info (binderVars tcbs) tclvl wanted
; traceTc "kcCheckDeclHeader_sig done:" $ vcat
[ text "tyConName = " <+> ppr (tyConName tc)
@@ -2506,7 +2576,7 @@ kcCheckDeclHeader_sig kisig name flav
KindedTyVar _ _ v v_hs_ki -> do
v_ki <- tcLHsKindSig (TyVarBndrKindCtxt (unLoc v)) v_hs_ki
discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
- unifyKind (Just (HsTyVar noExtField NotPromoted v))
+ unifyKind (Just (ppr v))
(tyBinderType tb)
v_ki
@@ -2960,19 +3030,22 @@ cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar
--------------------------------------
-- | Skolemise the 'HsTyVarBndr's in an 'LHsForAllTelescope.
--- Returns 'Left' for visible @forall@s and 'Right' for invisible @forall@s.
bindExplicitTKTele_Skol_M
:: TcTyMode
-> HsForAllTelescope GhcRn
-> TcM a
- -> TcM (Either [TcReqTVBinder] [TcInvisTVBinder], a)
+ -> TcM ([TcTyVarBinder], a)
bindExplicitTKTele_Skol_M mode tele thing_inside = case tele of
- HsForAllVis { hsf_vis_bndrs = bndrs } -> do
- (req_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside
- pure (Left req_tv_bndrs, thing)
- HsForAllInvis { hsf_invis_bndrs = bndrs } -> do
- (inv_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside
- pure (Right inv_tv_bndrs, thing)
+ HsForAllVis { hsf_vis_bndrs = bndrs }
+ -> do { (req_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M 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
+ -- inv_tv_bndrs :: [VarBndr TyVar Specificity],
+ -- but we want [VarBndr TyVar ArgFlag]
+ ; return (tyVarSpecToBinders inv_tv_bndrs, thing) }
bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
:: (OutputableBndrFlag flag)
@@ -3012,10 +3085,10 @@ bindExplicitTKBndrsX_Q
-- 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) }
+ ; return (binderVars tv_bndrs,res) }
bindExplicitTKBndrsX :: (OutputableBndrFlag flag)
- => (HsTyVarBndr flag GhcRn -> TcM TcTyVar)
+ => (HsTyVarBndr flag GhcRn -> TcM TyVar)
-> [LHsTyVarBndr flag GhcRn]
-> TcM a
-> TcM ([VarBndr TyVar flag], a) -- Returned [TcTyVar] are in 1-1 correspondence
@@ -3035,7 +3108,7 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
-- See GHC.Tc.Utils.TcMType Note [Cloning for tyvar binders]
; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $
go hs_tvs
- ; return ((Bndr tv (hsTyVarBndrFlag hs_tv)):tvs, res) }
+ ; return (Bndr tv (hsTyVarBndrFlag hs_tv):tvs, res) }
-----------------
tcHsTyVarBndr :: TcTyMode -> (Name -> Kind -> TcM TyVar)
@@ -3066,7 +3139,7 @@ tcHsQTyVarBndr _ new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind)
; mb_tv <- tcLookupLcl_maybe tv_nm
; case mb_tv of
Just (ATyVar _ tv)
- -> do { discardResult $ unifyKind (Just hs_tv)
+ -> do { discardResult $ unifyKind (Just (ppr tv_nm))
kind (tyVarKind tv)
-- This unify rejects:
-- class C (m :: * -> *) where
@@ -3074,9 +3147,6 @@ tcHsQTyVarBndr _ new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind)
; return tv }
_ -> new_tv tv_nm kind }
- where
- hs_tv = HsTyVar noExtField NotPromoted (noLoc tv_nm)
- -- Used for error messages only
--------------------------------------
-- Binding type/class variables in the
@@ -3116,56 +3186,63 @@ zonkAndScopedSort spec_tkvs
-- | Generalize some of the free variables in the given type.
-- All such variables should be *kind* variables; any type variables
-- should be explicitly quantified (with a `forall`) before now.
--- The supplied predicate says which free variables to quantify.
--- But in all cases,
--- generalize only those variables whose TcLevel is strictly greater
--- than the ambient level. This "strictly greater than" means that
--- you likely need to push the level before creating whatever type
--- gets passed here. Any variable whose level is greater than the
--- ambient level but is not selected to be generalized will be
--- promoted. (See [Promoting unification variables] in "GHC.Tc.Solver"
--- and Note [Recipe for checking a signature].)
--- The resulting KindVar are the variables to
--- quantify over, in the correct, well-scoped order. They should
--- generally be Inferred, not Specified, but that's really up to
--- the caller of this function.
-kindGeneralizeSome :: (TcTyVar -> Bool)
+--
+-- The WantedConstraints are un-solved kind constraints. Generally
+-- they'll be reported as errors later, but meanwhile we refrain
+-- from quantifying over any variable free in these unsolved
+-- constraints. See Note [Failure in local type signatures].
+--
+-- But in all cases, generalize only those variables whose TcLevel is
+-- strictly greater than the ambient level. This "strictly greater
+-- than" means that you likely need to push the level before creating
+-- whatever type gets passed here.
+--
+-- Any variable whose level is greater than the ambient level but is
+-- not selected to be generalized will be promoted. (See [Promoting
+-- unification variables] in "GHC.Tc.Solver" and Note [Recipe for
+-- checking a signature].)
+--
+-- The resulting KindVar are the variables to quantify over, in the
+-- correct, well-scoped order. They should generally be Inferred, not
+-- Specified, but that's really up to the caller of this function.
+kindGeneralizeSome :: WantedConstraints
-> TcType -- ^ needn't be zonked
-> TcM [KindVar]
-kindGeneralizeSome should_gen kind_or_type
- = do { traceTc "kindGeneralizeSome {" (ppr kind_or_type)
-
- -- use the "Kind" variant here, as any types we see
+kindGeneralizeSome wanted kind_or_type
+ = do { -- Use the "Kind" variant here, as any types we see
-- here will already have all type variables quantified;
-- thus, every free variable is really a kv, never a tv.
; dvs <- candidateQTyVarsOfKind kind_or_type
-
- -- So 'dvs' are the variables free in kind_or_type, with a level greater
- -- than the ambient level, hence candidates for quantification
- -- Next: filter out the ones we don't want to generalize (specified by should_gen)
- -- and promote them instead
-
- ; let (to_promote, dvs') = partitionCandidates dvs (not . should_gen)
-
+ ; dvs <- filterConstrainedCandidates wanted dvs
+ ; quantifyTyVars dvs }
+
+filterConstrainedCandidates
+ :: WantedConstraints -- Don't quantify over variables free in these
+ -- Not necessarily fully zonked
+ -> CandidatesQTvs -- Candidates for quantification
+ -> TcM CandidatesQTvs
+-- filterConstrainedCandidates removes any candidates that are free in
+-- 'wanted'; instead, it promotes them. This bit is very much like
+-- decideMonoTyVars in GHC.Tc.Solver, but constraints are so much
+-- simpler in kinds, it is much easier here. (In particular, we never
+-- quantify over a constraint in a type.)
+filterConstrainedCandidates wanted dvs
+ | isEmptyWC wanted -- Fast path for a common case
+ = return dvs
+ | otherwise
+ = do { wc_tvs <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted)
+ ; let (to_promote, dvs') = partitionCandidates dvs (`elemVarSet` wc_tvs)
; _ <- promoteTyVarSet to_promote
- ; qkvs <- quantifyTyVars dvs'
-
- ; traceTc "kindGeneralizeSome }" $
- vcat [ text "Kind or type:" <+> ppr kind_or_type
- , text "dvs:" <+> ppr dvs
- , text "dvs':" <+> ppr dvs'
- , text "to_promote:" <+> ppr to_promote
- , text "qkvs:" <+> pprTyVars qkvs ]
-
- ; return qkvs }
-
--- | Specialized version of 'kindGeneralizeSome', but where all variables
--- can be generalized. Use this variant when you can be sure that no more
--- constraints on the type's metavariables will arise or be solved.
-kindGeneralizeAll :: TcType -- needn't be zonked
- -> TcM [KindVar]
-kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty
- ; kindGeneralizeSome (const True) ty }
+ ; return dvs' }
+
+-- |- Specialised verison of 'kindGeneralizeSome', but with empty
+-- WantedConstraints, so no filtering is needed
+-- i.e. kindGeneraliseAll = kindGeneralizeSome emptyWC
+kindGeneralizeAll :: TcType -> TcM [KindVar]
+kindGeneralizeAll kind_or_type
+ = do { traceTc "kindGeneralizeAll" (ppr kind_or_type)
+ ; dvs <- candidateQTyVarsOfKind kind_or_type
+ ; quantifyTyVars dvs }
-- | Specialized version of 'kindGeneralizeSome', but where no variables
-- can be generalized, but perhaps some may neeed to be promoted.
@@ -3177,11 +3254,11 @@ kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty
-- Note [Promotion in signatures].
kindGeneralizeNone :: TcType -- needn't be zonked
-> TcM ()
-kindGeneralizeNone ty
- = do { traceTc "kindGeneralizeNone" empty
- ; kvs <- kindGeneralizeSome (const False) ty
- ; MASSERT( null kvs )
- }
+kindGeneralizeNone kind_or_type
+ = do { traceTc "kindGeneralizeNone" (ppr kind_or_type)
+ ; dvs <- candidateQTyVarsOfKind kind_or_type
+ ; _ <- promoteTyVarSet (candidateKindVars dvs)
+ ; return () }
{- Note [Levels and generalisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3508,10 +3585,10 @@ tcHsPartialSigType ctxt sig_ty
= addSigCtxt ctxt hs_ty $
do { mode <- mkHoleMode TypeLevel HM_Sig
; (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau)))
- <- solveLocalEqualities "tcHsPartialSigType" $
+ <- solveEqualities "tcHsPartialSigType" $
-- See Note [Failure in local type signatures]
- tcNamedWildCardBinders sig_wcs $ \ wcs ->
- bindImplicitTKBndrs_Tv implicit_hs_tvs $
+ tcNamedWildCardBinders sig_wcs $ \ wcs ->
+ bindImplicitTKBndrs_Tv implicit_hs_tvs $
bindExplicitTKBndrs_Tv_M mode explicit_hs_tvs $
do { -- Instantiate the type-class context; but if there
-- is an extra-constraints wildcard, just discard it here
@@ -3718,11 +3795,11 @@ tcHsPatSigType ctxt
do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
; mode <- mkHoleMode TypeLevel HM_Sig
; (wcs, sig_ty)
- <- addTypeCtxt hs_ty $
- solveLocalEqualities "tcHsPatSigType" $
+ <- addTypeCtxt hs_ty $
+ solveEqualities "tcHsPatSigType" $
-- See Note [Failure in local type signatures]
-- and c.f #16033
- tcNamedWildCardBinders sig_wcs $ \ wcs ->
+ tcNamedWildCardBinders sig_wcs $ \ wcs ->
tcExtendNameTyVarEnv sig_tkv_prs $
do { ek <- newOpenTypeKind
; sig_ty <- tc_lhs_type mode hs_ty ek
@@ -3768,7 +3845,7 @@ Here
It must be a skolem so that it retains its identity, and
GHC.Tc.Errors.getSkolemInfo can thereby find the binding site for the skolem.
- * The type signature pattern (f :: b -> c) makes freshs meta-tyvars
+ * The type signature pattern (f :: b -> c) makes fresh meta-tyvars
beta and gamma (TauTvs), and binds "b" :-> beta, "c" :-> gamma in the
environment
@@ -3796,7 +3873,7 @@ For RULE binders, though, things are a bit different (yuk).
RULE "foo" forall (x::a) (y::[a]). f x y = ...
Here this really is the binding site of the type variable so we'd like
to use a skolem, so that we get a complaint if we unify two of them
-together. Hence the new_tv function in tcHsPatSigType.
+together. Hence the new_implicit_tv function in tcHsPatSigType.
************************************************************************
@@ -3835,7 +3912,7 @@ tc_lhs_kind_sig mode ctxt hs_kind
-- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
-- Result is zonked
= do { kind <- addErrCtxt (text "In the kind" <+> quotes (ppr hs_kind)) $
- solveLocalEqualities "tcLHsKindSig" $
+ solveEqualities "tcLHsKindSig" $
tc_lhs_type mode hs_kind liftedTypeKind
; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
-- No generalization:
@@ -3876,19 +3953,6 @@ promotionErr name err
-}
--- | If the inner action emits constraints, report them as errors and fail;
--- otherwise, propagates the return value. Useful as a wrapper around
--- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be
--- another chance to solve constraints
-failIfEmitsConstraints :: TcM a -> TcM a
-failIfEmitsConstraints thing_inside
- = checkNoErrs $ -- We say that we fail if there are constraints!
- -- c.f same checkNoErrs in solveEqualities
- do { (res, lie) <- captureConstraints thing_inside
- ; reportAllUnsolved lie
- ; return res
- }
-
-- | Make an appropriate message for an error in a function argument.
-- Used for both expressions and types.
funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index 6226bbc65e..170930c2ff 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -14,7 +14,7 @@ module GHC.Tc.Gen.Sig(
TcSigFun,
isPartialSig, hasCompleteSig, tcIdSigName, tcSigInfoName,
- completeSigPolyId_maybe,
+ completeSigPolyId_maybe, isCompleteHsSig,
tcTySigs, tcUserTypeSig, completeSigFromId,
tcInstSig,
@@ -30,6 +30,7 @@ import GHC.Prelude
import GHC.Hs
import GHC.Tc.Gen.HsType
import GHC.Tc.Types
+import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType
@@ -360,23 +361,18 @@ Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
* After we kind-check the pieces and convert to Types, we do kind generalisation.
-Note [solveEqualities in tcPatSynSig]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Report unsolved equalities in tcPatSynSig]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's important that we solve /all/ the equalities in a pattern
synonym signature, because we are going to zonk the signature to
a Type (not a TcType), in GHC.Tc.TyCl.PatSyn.tc_patsyn_finish, and that
fails if there are un-filled-in coercion variables mentioned
in the type (#15694).
-The best thing is simply to use solveEqualities to solve all the
-equalites, rather than leaving them in the ambient constraints
-to be solved later. Pattern synonyms are top-level, so there's
-no problem with completely solving them.
-
-(NB: this solveEqualities wraps newImplicitTKBndrs, which itself
-does a solveLocalEqualities; so solveEqualities isn't going to
-make any further progress; it'll just report any unsolved ones,
-and fail, as it should.)
+So we solve all the equalities we can, and report any unsolved ones,
+rather than leaving them in the ambient constraints to be solved
+later. Pattern synonyms are top-level, so there's no problem with
+completely solving them.
-}
tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
@@ -388,12 +384,11 @@ tcPatSynSig name 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)
- ; (implicit_tvs, (univ_tvbndrs, (ex_tvbndrs, (req, prov, body_ty))))
- <- pushTcLevelM_ $
- solveEqualities $ -- See Note [solveEqualities in tcPatSynSig]
- bindImplicitTKBndrs_Skol implicit_hs_tvs $
- bindExplicitTKBndrs_Skol univ_hs_tvbndrs $
- bindExplicitTKBndrs_Skol ex_hs_tvbndrs $
+ ; (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 $
do { req <- tcHsContext hs_req
; prov <- tcHsContext hs_prov
; body_ty <- tcHsOpenType hs_body_ty
@@ -401,6 +396,7 @@ tcPatSynSig name sig_ty
-- e.g. pattern Zero <- 0# (#12094)
; return (req, prov, body_ty) }
+ ; implicit_tvs <- zonkAndScopedSort implicit_tvs
; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvbndrs
req ex_tvbndrs prov body_ty
@@ -408,61 +404,46 @@ tcPatSynSig name sig_ty
; kvs <- kindGeneralizeAll ungen_patsyn_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
+ -- See Note [Report unsolved equalities in tcPatSynSig]
+
-- These are /signatures/ so we zonk to squeeze out any kind
- -- unification variables. Do this after kindGeneralize which may
+ -- unification variables. Do this after kindGeneralizeAll which may
-- default kind variables to *.
- ; implicit_tvs <- zonkAndScopedSort implicit_tvs
+ ; 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
- -- Skolems have TcLevels too, though they're used only for debugging.
- -- If you don't do this, the debugging checks fail in GHC.Tc.TyCl.PatSyn.
- -- Test case: patsyn/should_compile/T13441
-{-
- ; tclvl <- getTcLevel
- ; let env0 = mkEmptyTCvSubst $ mkInScopeSet $ mkVarSet kvs
- (env1, implicit_tvs') = promoteSkolemsX tclvl env0 implicit_tvs
- (env2, univ_tvs') = promoteSkolemsX tclvl env1 univ_tvs
- (env3, ex_tvs') = promoteSkolemsX tclvl env2 ex_tvs
- req' = substTys env3 req
- prov' = substTys env3 prov
- body_ty' = substTy env3 body_ty
--}
- ; let implicit_tvs' = implicit_tvs
- univ_tvbndrs' = univ_tvbndrs
- ex_tvbndrs' = ex_tvbndrs
- req' = req
- prov' = prov
- body_ty' = 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 kvs implicit_tvs univ_tvbndrs req ex_tvbndrs prov body_ty
-- arguments become the types of binders. We thus cannot allow
-- levity polymorphism here
- ; let (arg_tys, _) = tcSplitFunTys body_ty'
+ ; let (arg_tys, _) = tcSplitFunTys body_ty
; mapM_ (checkForLevPoly empty . scaledThing) arg_tys
; traceTc "tcTySig }" $
- vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs'
+ vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs
, text "kvs" <+> ppr_tvs kvs
- , text "univ_tvs" <+> ppr_tvs (binderVars univ_tvbndrs')
- , text "req" <+> ppr req'
- , text "ex_tvs" <+> ppr_tvs (binderVars ex_tvbndrs')
- , text "prov" <+> ppr prov'
- , text "body_ty" <+> ppr body_ty' ]
+ , text "univ_tvs" <+> ppr_tvs (binderVars univ_tvbndrs)
+ , text "req" <+> ppr req
+ , text "ex_tvs" <+> ppr_tvs (binderVars ex_tvbndrs)
+ , 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_req = req'
- , patsig_ex_bndrs = ex_tvbndrs'
- , patsig_prov = prov'
- , patsig_body_ty = body_ty' }) }
+ mkTyVarBinders SpecifiedSpec implicit_tvs
+ , patsig_univ_bndrs = univ_tvbndrs
+ , patsig_req = req
+ , patsig_ex_bndrs = ex_tvbndrs
+ , patsig_prov = prov
+ , patsig_body_ty = body_ty }) }
where
ctxt = PatSynCtxt name
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index c18ce5f3cf..5871eb99ea 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -1435,11 +1435,17 @@ reifyInstances th_nm th_tys
rnImplicitBndrs Nothing tv_rdrs $ \ tv_names ->
do { (rn_ty, fvs) <- rnLHsType doc rdr_ty
; return ((tv_names, rn_ty), fvs) }
- ; (_tvs, ty)
- <- pushTcLevelM_ $
- solveEqualities $ -- Avoid error cascade if there are unsolved
- bindImplicitTKBndrs_Skol tv_names $
+
+ ; (tclvl, wanted, (tvs, ty))
+ <- pushLevelAndSolveEqualitiesX "reifyInstances" $
+ bindImplicitTKBndrs_Skol tv_names $
tcInferLHsType rn_ty
+
+ ; tvs <- zonkAndScopedSort tvs
+
+ -- Avoid error cascade if there are unsolved
+ ; reportUnsolvedEqualities ReifySkol tvs tclvl wanted
+
; ty <- zonkTcTypeToType ty
-- Substitute out the meta type variables
-- In particular, the type might have kind
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index f29378122c..784625f3a2 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -2589,18 +2589,18 @@ tcRnType hsc_env flexi normalise rdr_type
-- It can have any rank or kind
-- First bring into scope any wildcards
; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
- ; (ty, kind) <- pushTcLevelM_ $
- -- must push level to satisfy level precondition of
- -- kindGeneralize, below
- solveEqualities $
- tcNamedWildCardBinders wcs $ \ wcs' ->
- do { mapM_ emitNamedTypeHole wcs'
- ; tcInferLHsTypeUnsaturated rn_type }
+ ; (_tclvl, wanted, (ty, kind))
+ <- pushLevelAndSolveEqualitiesX "tcRnType" $
+ tcNamedWildCardBinders wcs $ \ wcs' ->
+ do { mapM_ emitNamedTypeHole wcs'
+ ; tcInferLHsTypeUnsaturated rn_type }
+
+ ; checkNoErrs (reportAllUnsolved wanted)
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
; kvs <- kindGeneralizeAll kind
- ; e <- mkEmptyZonkEnv flexi
+ ; e <- mkEmptyZonkEnv flexi
; ty <- zonkTcTypeToTypeX e ty
-- Do validity checking on type
@@ -2615,6 +2615,7 @@ tcRnType hsc_env flexi normalise rdr_type
; return (ty', mkInfForAllTys kvs (tcTypeKind ty')) }
+
{- Note [TcRnExprMode]
~~~~~~~~~~~~~~~~~~~~~~
How should we infer a type when a user asks for the type of an expression e
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index ad0ea2ed3c..2aa1189bcf 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -7,14 +7,16 @@ module GHC.Tc.Solver(
simplifyDefault,
simplifyTop, simplifyTopImplic,
simplifyInteractive,
- solveEqualities, solveLocalEqualities, solveLocalEqualitiesX,
+ solveEqualities,
+ pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX,
+ reportUnsolvedEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
tcNormalise,
captureTopConstraints,
- simpl_top,
+ simplifyTopWanteds,
promoteTyVarSet, emitFlatConstraints,
@@ -42,8 +44,9 @@ import GHC.Tc.Types.Evidence
import GHC.Tc.Solver.Interact
import GHC.Tc.Solver.Canonical ( makeSuperClasses, solveCallStack )
import GHC.Tc.Solver.Flatten ( flattenType )
-import GHC.Tc.Utils.TcMType as TcM
-import GHC.Tc.Utils.Monad as TcM
+import GHC.Tc.Utils.Unify ( buildTvImplication )
+import GHC.Tc.Utils.TcMType as TcM
+import GHC.Tc.Utils.Monad as TcM
import GHC.Tc.Solver.Monad as TcS
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
@@ -56,7 +59,6 @@ import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Types.Var
import GHC.Types.Var.Set
-import GHC.Types.Unique.Set
import GHC.Types.Basic ( IntWithInf, intGtLimit )
import GHC.Utils.Error ( emptyMessages )
import qualified GHC.LanguageExtensions as LangExt
@@ -85,7 +87,7 @@ captureTopConstraints :: TcM a -> TcM (a, WantedConstraints)
--
-- Importantly, if captureTopConstraints propagates an exception, it
-- reports any insoluble constraints first, lest they be lost
--- altogether. This is important, because solveLocalEqualities (maybe
+-- altogether. This is important, because solveEqualities (maybe
-- other things too) throws an exception without adding any error
-- messages; it just puts the unsolved constraints back into the
-- monad. See GHC.Tc.Utils.Monad Note [Constraints and errors]
@@ -129,7 +131,7 @@ simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
simplifyTop wanteds
= do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
; ((final_wc, unsafe_ol), binds1) <- runTcS $
- do { final_wc <- simpl_top wanteds
+ do { final_wc <- simplifyTopWanteds wanteds
; unsafe_ol <- getSafeOverlapFailures
; return (final_wc, unsafe_ol) }
; traceTc "End simplifyTop }" empty
@@ -155,16 +157,54 @@ simplifyTop wanteds
; return (evBindMapBinds binds1 `unionBags` binds2) }
+pushLevelAndSolveEqualities :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
+-- Push level, and solve all resulting equalities
+-- If there are any unsolved equalities, report them
+-- and fail (in the monad)
+--
+-- Panics if we solve any non-equality constraints. (In runTCSEqualities
+-- we use an error thunk for the evidence bindings.)
+pushLevelAndSolveEqualities skol_info skol_tvs thing_inside
+ = do { (tclvl, wanted, res) <- pushLevelAndSolveEqualitiesX
+ "pushLevelAndSolveEqualities" thing_inside
+ ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
+ ; return res }
+
+pushLevelAndSolveEqualitiesX :: String -> TcM a
+ -> TcM (TcLevel, WantedConstraints, a)
+-- Push the level, gather equality constraints, and then solve them.
+-- Returns any remaining unsolved equalities.
+-- Does not report errors.
+--
+-- Panics if we solve any non-equality constraints. (In runTCSEqualities
+-- we use an error thunk for the evidence bindings.)
+pushLevelAndSolveEqualitiesX callsite thing_inside
+ = do { traceTc "pushLevelAndSolveEqualitiesX {" (text "Called from" <+> text callsite)
+ ; (tclvl, (wanted, res))
+ <- pushTcLevelM $
+ do { (res, wanted) <- captureConstraints thing_inside
+ ; wanted <- runTcSEqualities (simplifyTopWanteds wanted)
+ ; return (wanted,res) }
+ ; traceTc "pushLevelAndSolveEqualities }" (vcat [ text "Residual:" <+> ppr wanted
+ , text "Level:" <+> ppr tclvl ])
+ ; return (tclvl, wanted, res) }
-- | Type-check a thing that emits only equality constraints, solving any
--- constraints we can and re-emitting constraints that we can't. The thing_inside
--- should generally bump the TcLevel to make sure that this run of the solver
--- doesn't affect anything lying around.
-solveLocalEqualities :: String -> TcM a -> TcM a
--- Note [Failure in local type signatures]
-solveLocalEqualities callsite thing_inside
- = do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside
- ; emitFlatConstraints wanted
+-- constraints we can and re-emitting constraints that we can't.
+-- Use this variant only when we'll get another crack at it later
+-- See Note [Failure in local type signatures]
+--
+-- Panics if we solve any non-equality constraints. (In runTCSEqualities
+-- we use an error thunk for the evidence bindings.)
+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)
; return res }
emitFlatConstraints :: WantedConstraints -> TcM ()
@@ -176,7 +216,7 @@ emitFlatConstraints wanted
; emitConstraints wanted -- So they get reported!
; failM }
Just (simples, holes)
- -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples)
+ -> do { _ <- TcM.promoteTyVarSet (tyCoVarsOfCts simples)
; traceTc "emitFlatConstraints:" $
vcat [ text "simples:" <+> ppr simples
, text "holes: " <+> ppr holes ]
@@ -226,10 +266,21 @@ floatKindEqualities wc = float_wc emptyVarSet wc
{- Note [Failure in local type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When kind checking a type signature, we like to fail fast if we can't
-solve all the kind equality constraints: see Note [Fail fast on kind
-errors]. But what about /local/ type signatures, mentioning in-scope
-type variables for which there might be given equalities. Here's
-an example (T15076b):
+solve all the kind equality constraints, for two reasons:
+
+ * A kind-bogus type signature may cause a cascade of knock-on
+ errors if we let it pass
+
+ * More seriously, we don't have a convenient term-level place to add
+ deferred bindings for unsolved kind-equality constraints. In
+ earlier GHCs this led to un-filled-in coercion holes, which caused
+ GHC to crash with "fvProv falls into a hole" See #11563, #11520,
+ #11516, #11399
+
+But what about /local/ type signatures, mentioning in-scope type
+variables for which there might be 'given' equalities? For these we
+might not be able to solve all the equalities locally. Here's an
+example (T15076b):
class (a ~ b) => C a b
data SameKind :: k -> k -> Type where { SK :: SameKind a b }
@@ -238,7 +289,7 @@ an example (T15076b):
C a b => Proxy a -> Proxy b -> ()
bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y)
-Consider the type singature on 'undefined'. It's ill-kinded unless
+Consider the type signature on 'undefined'. It's ill-kinded unless
a~b. But the superclass of (C a b) means that indeed (a~b). So all
should be well. BUT it's hard to see that when kind-checking the signature
for undefined. We want to emit a residual (a~b) constraint, to solve
@@ -264,13 +315,15 @@ hoping to solve it later, we might end up filling in the holes
co1 and co2 with coercions involving 'a' and 'b' -- but by now
we've instantiated the type. Chaos!
-Moreover, the unsolved constraints might be skolem-escpae things, and
+Moreover, the unsolved constraints might be skolem-escape things, and
if we proceed with f bound to a nonsensical type, we get a cascade of
follow-up errors. For example polykinds/T12593, T15577, and many others.
-So here's the plan:
+So here's the plan (see tcHsSigType):
-* solveLocalEqualitiesX: try to solve the constraints (solveLocalEqualitiesX)
+* pushLevelAndSolveEqualitiesX: try to solve the constraints
+
+* kindGeneraliseSome: do kind generalisation
* buildTvImplication: build an implication for the residual, unsolved
constraint
@@ -292,54 +345,49 @@ So here's the plan:
All this is done:
-* in solveLocalEqualities, where there is no kind-generalisation
- to complicate matters.
-
-* in GHC.Tc.Gen.HsType.tcHsSigType, where quantification intervenes.
-
-See also #18062, #11506
--}
-
-solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a)
-solveLocalEqualitiesX callsite thing_inside
- = do { traceTc "solveLocalEqualitiesX {" (vcat [ text "Called from" <+> text callsite ])
+* In GHC.Tc.Gen.HsType.tcHsSigType, as above
- ; (result, wanted) <- captureConstraints thing_inside
+* solveEqualities. Use this when there no kind-generalisation
+ step to complicate matters; then we don't need to push levels,
+ and can solve the equalities immediately without needing to
+ wrap it in an implication constraint. (You'll generally see
+ a kindGeneraliseNone nearby.)
- ; traceTc "solveLocalEqualities: running solver" (ppr wanted)
- ; residual_wanted <- runTcSEqualities (solveWanteds wanted)
+* In GHC.Tc.TyCl and GHC.Tc.TyCl.Instance; see calls to
+ pushLevelAndSolveEqualitiesX, followed by quantification, and
+ then reportUnsolvedEqualities.
- ; traceTc "solveLocalEqualitiesX end }" $
- text "residual_wanted =" <+> ppr residual_wanted
+ NB: we call reportUnsolvedEqualities before zonkTcTypeToType
+ because the latter does not expect to see any un-filled-in
+ coercions, which will happen if we have unsolved equalities.
+ By calling reportUnsolvedEqualities first, which fails after
+ reporting errors, we avoid that happening.
- ; return (residual_wanted, result) }
-
--- | Type-check a thing that emits only equality constraints, then
--- solve those constraints. Fails outright if there is trouble.
--- Use this if you're not going to get another crack at solving
--- (because, e.g., you're checking a datatype declaration)
-solveEqualities :: TcM a -> TcM a
-solveEqualities thing_inside
- = checkNoErrs $ -- See Note [Fail fast on kind errors]
- do { lvl <- TcM.getTcLevel
- ; traceTc "solveEqualities {" (text "level =" <+> ppr lvl)
+See also #18062, #11506
+-}
- ; (result, wanted) <- captureConstraints thing_inside
- ; traceTc "solveEqualities: running solver" $ text "wanted = " <+> ppr wanted
- ; final_wc <- runTcSEqualities $ simpl_top wanted
- -- NB: Use simpl_top here so that we potentially default RuntimeRep
- -- vars to LiftedRep. This is needed to avoid #14991.
+reportUnsolvedEqualities :: SkolemInfo -> [TcTyVar] -> TcLevel
+ -> WantedConstraints -> TcM ()
+-- Reports all unsolved wanteds provided; fails in the monad if there are any.
+--
+-- The provided SkolemInfo and [TcTyVar] arguments are used in an implication to
+-- provide skolem info for any errors.
+--
+reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
+ | isEmptyWC wanted
+ = return ()
+ | otherwise
+ = checkNoErrs $ -- Fail
+ do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
+ ; reportAllUnsolved (mkImplicWC (unitBag implic)) }
- ; traceTc "End solveEqualities }" empty
- ; reportAllUnsolved final_wc
- ; return result }
-- | Simplify top-level constraints, but without reporting any unsolved
-- constraints nor unsafe overlapping.
-simpl_top :: WantedConstraints -> TcS WantedConstraints
+simplifyTopWanteds :: WantedConstraints -> TcS WantedConstraints
-- See Note [Top-level Defaulting Plan]
-simpl_top wanteds
+simplifyTopWanteds wanteds
= do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
-- This is where the main work happens
; dflags <- getDynFlags
@@ -424,29 +472,8 @@ defaultCallStacks wanteds
= return (Just ct)
-{- Note [Fail fast on kind errors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-solveEqualities is used to solve kind equalities when kind-checking
-user-written types. If solving fails we should fail outright, rather
-than just accumulate an error message, for two reasons:
-
- * A kind-bogus type signature may cause a cascade of knock-on
- errors if we let it pass
-
- * More seriously, we don't have a convenient term-level place to add
- deferred bindings for unsolved kind-equality constraints, so we
- don't build evidence bindings (by usine reportAllUnsolved). That
- means that we'll be left with a type that has coercion holes
- in it, something like
- <type> |> co-hole
- where co-hole is not filled in. Eeek! That un-filled-in
- hole actually causes GHC to crash with "fvProv falls into a hole"
- See #11563, #11520, #11516, #11399
-
-So it's important to use 'checkNoErrs' here!
-
-Note [When to do type-class defaulting]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [When to do type-class defaulting]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
was false, on the grounds that defaulting can't help solve insoluble
constraints. But if we *don't* do defaulting we may report a whole
@@ -592,7 +619,7 @@ How is this implemented? It's complicated! So we'll step through it all:
`InertCans`.
4) `GHC.Tc.Solver.simplifyTop`:
- * Call simpl_top, the top-level function for driving the simplifier for
+ * Call simplifyTopWanteds, the top-level function for driving the simplifier for
constraint resolution.
* Once finished, call `getSafeOverlapFailures` to retrieve the
@@ -629,7 +656,7 @@ How is this implemented? It's complicated! So we'll step through it all:
Note [No defaulting in the ambiguity check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When simplifying constraints for the ambiguity check, we use
-solveWantedsAndDrop, not simpl_top, so that we do no defaulting.
+solveWantedsAndDrop, not simplifyTopWanteds, so that we do no defaulting.
#11947 was an example:
f :: Num a => Int -> Int
This is ambiguous of course, but we don't want to default the
@@ -970,7 +997,7 @@ mkResidualConstraints rhs_tclvl ev_binds_var
; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
- ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple)
+ ; _ <- TcM.promoteTyVarSet (tyCoVarsOfCts outer_simple)
; let inner_wanted = wanteds { wc_simple = inner_simple }
; implics <- if isEmptyWC inner_wanted
@@ -2174,29 +2201,6 @@ we'll get more Givens (a unification is like adding a Given) to
allow the implication to make progress.
-}
-promoteTyVar :: TcTyVar -> TcM Bool
--- When we float a constraint out of an implication we must restore
--- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType
--- Return True <=> we did some promotion
--- Also returns either the original tyvar (no promotion) or the new one
--- See Note [Promoting unification variables]
-promoteTyVar tv
- = do { tclvl <- TcM.getTcLevel
- ; if (isFloatedTouchableMetaTyVar tclvl tv)
- then do { cloned_tv <- TcM.cloneMetaTyVar tv
- ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
- ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv)
- ; return True }
- else return False }
-
--- Returns whether or not *any* tyvar is defaulted
-promoteTyVarSet :: TcTyVarSet -> TcM Bool
-promoteTyVarSet tvs
- = do { bools <- mapM promoteTyVar (nonDetEltsUniqSet tvs)
- -- Non-determinism is OK because order of promotion doesn't matter
-
- ; return (or bools) }
-
promoteTyVarTcS :: TcTyVar -> TcS ()
-- When we float a constraint out of an implication we must restore
-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 2cefd67c7f..9cd0b2a66c 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -30,6 +30,8 @@ import GHC.Prelude
import GHC.Hs
import GHC.Driver.Types
import GHC.Tc.TyCl.Build
+import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX
+ , reportUnsolvedEqualities )
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Env
import GHC.Tc.Validity
@@ -38,7 +40,6 @@ import GHC.Tc.TyCl.Utils
import GHC.Tc.TyCl.Class
import {-# SOURCE #-} GHC.Tc.TyCl.Instance( tcInstDecls1 )
import GHC.Tc.Deriv (DerivInfo(..))
-import GHC.Tc.Utils.Unify ( checkTvConstraints )
import GHC.Tc.Gen.HsType
import GHC.Tc.Instance.Class( AssocInstInfo(..) )
import GHC.Tc.Utils.TcMType
@@ -644,13 +645,18 @@ kcTyClGroup kisig_env decls
| otherwise = Left d
- ; checked_tcs <- checkInitialKinds kinded_decls
+ ; checked_tcs <- checkNoErrs $
+ checkInitialKinds kinded_decls
+ -- checkNoErrs because we are about to extend
+ -- the envt with these tycons, and we get
+ -- knock-on errors if we have tycons with
+ -- malformed kinds
+
; inferred_tcs
- <- tcExtendKindEnvWithTyCons checked_tcs $
- pushTcLevelM_ $ -- We are going to kind-generalise, so
- -- unification variables in here must
- -- be one level in
- solveEqualities $
+ <- tcExtendKindEnvWithTyCons checked_tcs $
+ pushLevelAndSolveEqualities UnkSkol [] $
+ -- We are going to kind-generalise, so unification
+ -- variables in here must be one level in
do { -- Step 1: Bind kind variables for all decls
mono_tcs <- inferInitialKinds kindless_decls
@@ -2300,10 +2306,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
roles = roles_info tycon_name -- for TyCon and Class
; (ctxt, fds, sig_stuff, at_stuff)
- <- pushTcLevelM_ $
- solveEqualities $
- checkTvConstraints skol_info (binderVars binders) $
- -- The checkTvConstraints is needed bring into scope the
+ <- pushLevelAndSolveEqualities skol_info (binderVars binders) $
+ -- The (binderVars binders) is needed bring into scope the
-- skolems bound by the class decl header (#17841)
do { ctxt <- tcHsContext hs_ctxt
; fds <- mapM (addLocM tc_fundep) fundeps
@@ -2311,7 +2315,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
; at_stuff <- tcClassATs class_name clas ats at_defs
; return (ctxt, fds, sig_stuff, at_stuff) }
- -- The solveEqualities will report errors for any
+
+ -- The pushLevelAndSolveEqualities will report errors for any
-- unsolved equalities, so these zonks should not encounter
-- any unfilled coercion variables unless there is such an error
-- The zonk also squeeze out the TcTyCons, and converts
@@ -2703,13 +2708,13 @@ tcTySynRhs roles_info tc_name hs_ty
= bindTyClTyVars tc_name $ \ _ binders res_kind ->
do { env <- getLclEnv
; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
- ; rhs_ty <- pushTcLevelM_ $
- solveEqualities $
+ ; rhs_ty <- pushLevelAndSolveEqualities skol_info (binderVars binders) $
tcCheckLHsType hs_ty (TheKind res_kind)
; rhs_ty <- zonkTcTypeToType rhs_ty
; let roles = roles_info tc_name
- tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
- ; return tycon }
+ ; return (buildSynTyCon tc_name binders res_kind roles rhs_ty) }
+ where
+ skol_info = TyConSkol TypeSynonymFlavour tc_name
tcDataDefn :: SDoc -> RolesInfo -> Name
-> HsDataDefn GhcRn -> TcM (TyCon, [DerivInfo])
@@ -2739,7 +2744,9 @@ tcDataDefn err_ctxt roles_info tc_name
; unless (mk_permissive_kind hsc_src cons) $
checkDataKindSig (DataDeclSort new_or_data) final_res_kind
- ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt
+ ; let skol_tvs = binderVars tycon_binders
+ ; stupid_tc_theta <- pushLevelAndSolveEqualities skol_info skol_tvs $
+ tcHsContext ctxt
; stupid_theta <- zonkTcTypesToTypes stupid_tc_theta
; kind_signatures <- xoptM LangExt.KindSignatures
@@ -2775,6 +2782,9 @@ tcDataDefn err_ctxt roles_info tc_name
; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
; return (tycon, [deriv_info]) }
where
+ skol_info = TyConSkol flav tc_name
+ flav = newOrDataToFlavour new_or_data
+
-- Abstract data types in hsig files can have arbitrary kinds,
-- because they may be implemented by type synonyms
-- (which themselves can have arbitrary kinds, not just *). See #13955.
@@ -2912,40 +2922,38 @@ or (Type -> Type) for the equations above) and the instantiated kind.
Note [Generalising in tcTyFamInstEqnGuts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have something like
- type instance forall (a::k) b. F t1 t2 = rhs
+ type instance forall (a::k) b. F (Proxy t1) _ = rhs
Then imp_vars = [k], exp_bndrs = [a::k, b]
-We want to quantify over
- * k, a, and b (all user-specified)
- * and any inferred free kind vars from
- - the kinds of k, a, b
- - the types t1, t2
+We want to quantify over all the free vars of the LHS including
+ * any invisible kind variables arising from instantiating tycons,
+ such as Proxy
+ * wildcards such as '_' above
-However, unlike a type signature like
- f :: forall (a::k). blah
+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
+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.
-So, the simple thing is
- - gather candidates from [k, a, b] and pats
- - quantify over them
-
-Hence the slightly mysterious call:
- candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs)
+See also Note [Re-quantify type variables in rules] in
+GHC.Tc.Gen.Rule, which explains a /very/ similar design when
+generalising over the type of a rewrite rule.
-Simple, neat, but a little non-obvious!
-
-See also Note [Re-quantify type variables in rules] in GHC.Tc.Gen.Rule, which explains
-a very similar design when generalising over the type of a rewrite rule.
-}
--------------------------
tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo
- -> [Name] -> [LHsTyVarBndr () GhcRn] -- Implicit and explicicit binder
+ -> [Name] -> [LHsTyVarBndr () GhcRn] -- Implicit and explicit binder
-> HsTyPats GhcRn -- Patterns
-> LHsType GhcRn -- RHS
-> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs)
@@ -2958,11 +2966,10 @@ 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
- ; (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty)))
- <- pushTcLevelM_ $
- solveEqualities $
- bindImplicitTKBndrs_Q_Skol imp_vars $
- bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
+ ; (tclvl, wanted, (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty))))
+ <- pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $
+ bindImplicitTKBndrs_Q_Skol imp_vars $
+ bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats
-- Ensure that the instance is consistent with its
-- parent class (#16008)
@@ -2970,21 +2977,20 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
; rhs_ty <- tcCheckLHsType hs_rhs_ty (TheKind rhs_kind)
; return (lhs_ty, rhs_ty) }
- -- See Note [Generalising in tcTyFamInstEqnGuts]
-- This code (and the stuff immediately above) is very similar
-- to that in tcDataFamInstHeader. Maybe we should abstract the
-- common code; but for the moment I concluded that it's
-- clearer to duplicate it. Still, if you fix a bug here,
-- check there too!
- ; let scoped_tvs = imp_tvs ++ exp_tvs
- ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
+
+ -- See Note [Generalising in tcTyFamInstEqnGuts]
+ ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys (imp_tvs ++ exp_tvs))
; qtvs <- quantifyTyVars dvs
+ ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
; traceTc "tcTyFamInstEqnGuts 2" $
vcat [ ppr fam_tc
- , text "scoped_tvs" <+> pprTyVars scoped_tvs
, text "lhs_ty" <+> ppr lhs_ty
- , text "dvs" <+> ppr dvs
, text "qtvs" <+> pprTyVars qtvs ]
; (ze, qtvs) <- zonkTyBndrs qtvs
@@ -3167,11 +3173,11 @@ tcConDecl :: KnotTied TyCon -- Representation tycon. Knot-tied!
-> TcM [DataCon]
tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
- (ConDeclH98 { con_name = name
+ (ConDeclH98 { con_name = lname@(L _ name)
, con_ex_tvs = explicit_tkv_nms
, con_mb_cxt = hs_ctxt
, con_args = hs_args })
- = addErrCtxt (dataConCtxtName [name]) $
+ = addErrCtxt (dataConCtxtName [lname]) $
do { -- NB: the tyvars from the declaration header are in scope
-- Get hold of the existential type variables
@@ -3182,62 +3188,63 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
- ; (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts))
- <- pushTcLevelM_ $
- solveEqualities $
- bindExplicitTKBndrs_Skol explicit_tkv_nms $
+ ; (tclvl, wanted, (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts)))
+ <- pushLevelAndSolveEqualitiesX "tcConDecl:H98" $
+ bindExplicitTKBndrs_Skol explicit_tkv_nms $
do { ctxt <- tcHsMbContext hs_ctxt
; let exp_kind = getArgExpKind new_or_data res_kind
; btys <- tcConArgs exp_kind hs_args
- ; field_lbls <- lookupConstructorFields (unLoc name)
+ ; field_lbls <- lookupConstructorFields name
; let (arg_tys, stricts) = unzip btys
; return (ctxt, arg_tys, field_lbls, stricts)
}
+
; let tmpl_tvs = binderVars tmpl_bndrs
+ ; let fake_ty = mkSpecForAllTys tmpl_tvs $
+ mkInvisForAllTys exp_tvbndrs $
+ mkPhiTy ctxt $
+ mkVisFunTys arg_tys $
+ unitTy
+ -- That type is a lie, of course. (It shouldn't end in ()!)
+ -- And we could construct a proper result type from the info
+ -- at hand. But the result would mention only the tmpl_tvs,
+ -- and so it just creates more work to do it right. Really,
+ -- we're only doing this to find the right kind variables to
+ -- quantify over, and this type is fine for that purpose.
-- exp_tvs have explicit, user-written binding sites
-- the kvs below are those kind variables entirely unmentioned by the user
-- and discovered only by generalization
- ; kvs <- kindGeneralizeAll (mkSpecForAllTys tmpl_tvs $
- mkInvisForAllTys exp_tvbndrs $
- mkPhiTy ctxt $
- mkVisFunTys arg_tys $
- unitTy)
- -- That type is a lie, of course. (It shouldn't end in ()!)
- -- And we could construct a proper result type from the info
- -- at hand. But the result would mention only the tmpl_tvs,
- -- and so it just creates more work to do it right. Really,
- -- we're only doing this to find the right kind variables to
- -- quantify over, and this type is fine for that purpose.
+ ; kvs <- kindGeneralizeAll fake_ty
+
+ ; let skol_tvs = kvs ++ tmpl_tvs ++ binderVars exp_tvbndrs
+ ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
-- Zonk to Types
; (ze, qkvs) <- zonkTyBndrs kvs
; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs
- ; let user_qtvs = binderVars user_qtvbndrs
; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys
; ctxt <- zonkTcTypesToTypesX ze ctxt
- ; fam_envs <- tcGetFamInstEnvs
-
-- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
; let
univ_tvbs = tyConInvisTVBinders tmpl_bndrs
univ_tvs = binderVars univ_tvbs
- ex_tvbs = mkTyVarBinders InferredSpec qkvs ++
- user_qtvbndrs
- ex_tvs = qkvs ++ user_qtvs
+ ex_tvbs = mkTyVarBinders InferredSpec qkvs ++ user_qtvbndrs
+ ex_tvs = binderVars ex_tvbs
-- For H98 datatypes, the user-written tyvar binders are precisely
-- the universals followed by the existentials.
-- See Note [DataCon user type variable binders] in GHC.Core.DataCon.
user_tvbs = univ_tvbs ++ ex_tvbs
- buildOneDataCon (L _ name) = do
- { is_infix <- tcConIsInfixH98 name hs_args
- ; rep_nm <- newTyConRepName name
- ; buildDataCon fam_envs name is_infix rep_nm
+ ; traceTc "tcConDecl 2" (ppr name)
+ ; is_infix <- tcConIsInfixH98 name hs_args
+ ; rep_nm <- newTyConRepName name
+ ; fam_envs <- tcGetFamInstEnvs
+ ; dc <- buildDataCon fam_envs name is_infix rep_nm
stricts Nothing field_lbls
univ_tvs ex_tvs user_tvbs
[{- no eq_preds -}] ctxt arg_tys
@@ -3245,10 +3252,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data
-- NB: we put data_tc, the type constructor gotten from the
-- constructor type signature into the data constructor;
-- that way checkValidDataCon can complain if it's wrong.
- }
- ; traceTc "tcConDecl 2" (ppr name)
- ; mapM buildOneDataCon [name]
- }
+
+ ; return [dc] }
+ where
+ skol_info = DataConSkol name
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,
@@ -3262,12 +3269,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
do { traceTc "tcConDecl 1 gadt" (ppr names)
; let (L _ name : _) = names
- ; (imp_tvs, (exp_tvbndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
- <- pushTcLevelM_ $ -- We are going to generalise
- solveEqualities $ -- We won't get another crack, and we don't
- -- want an error cascade
- bindImplicitTKBndrs_Skol implicit_tkv_nms $
- bindExplicitTKBndrs_Skol explicit_tkv_nms $
+ ; (tclvl, wanted, (imp_tvs, (exp_tvbndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts))))
+ <- pushLevelAndSolveEqualitiesX "tcConDecl:GADT" $
+ bindImplicitTKBndrs_Skol implicit_tkv_nms $
+ bindExplicitTKBndrs_Skol explicit_tkv_nms $
do { ctxt <- tcHsMbContext cxt
; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty
-- See Note [GADT return kinds]
@@ -3281,17 +3286,19 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
}
; imp_tvs <- zonkAndScopedSort imp_tvs
-
- ; tkvs <- kindGeneralizeAll (mkSpecForAllTys imp_tvs $
- mkInvisForAllTys exp_tvbndrs $
- mkPhiTy ctxt $
- mkVisFunTys arg_tys $
- res_ty)
-
- ; let tvbndrs = (mkTyVarBinders InferredSpec tkvs)
- ++ (mkTyVarBinders SpecifiedSpec 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
+ ; reportUnsolvedEqualities skol_info (binderVars tvbndrs) tclvl wanted
+
-- Zonk to Types
; (ze, tvbndrs) <- zonkTyVarBinders tvbndrs
; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys
@@ -3306,11 +3313,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
arg_tys' = substScaledTys arg_subst arg_tys
res_ty' = substTy arg_subst res_ty
-
- ; fam_envs <- tcGetFamInstEnvs
-
-- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls)
+ ; fam_envs <- tcGetFamInstEnvs
; let
buildOneDataCon (L _ name) = do
{ is_infix <- tcConIsInfixGADT name hs_args
@@ -3325,9 +3330,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
-- constructor type signature into the data constructor;
-- that way checkValidDataCon can complain if it's wrong.
}
- ; traceTc "tcConDecl 2" (ppr names)
- ; mapM buildOneDataCon names
- }
+ ; mapM buildOneDataCon names }
+ where
+ skol_info = DataConSkol (unLoc (head names))
{- Note [GADT return kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 36d25d0eaf..b0dfa80f90 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -30,6 +30,7 @@ import GHC.Tc.TyCl.Utils ( addTyConsToGblEnv )
import GHC.Tc.TyCl.Class ( tcClassDecl2, tcATDefault,
HsSigFun, mkHsSigFun, badMethodErr,
findMethodBind, instantiateMethod )
+import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
import GHC.Tc.Gen.Sig
import GHC.Tc.Utils.Monad
import GHC.Tc.Validity
@@ -856,11 +857,10 @@ tcDataFamInstHeader
tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
hs_ctxt hs_pats m_ksig hs_cons new_or_data
= do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
- ; (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
- <- pushTcLevelM_ $
- solveEqualities $
- bindImplicitTKBndrs_Q_Skol imp_vars $
- bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
+ ; (tclvl, wanted, (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind))))
+ <- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
+ bindImplicitTKBndrs_Q_Skol imp_vars $
+ bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
do { stupid_theta <- tcHsContext hs_ctxt
; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
; (lhs_applied_ty, lhs_applied_kind)
@@ -882,7 +882,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
-- is compatible with the explicit signature (or Type, if there
-- is none)
; let hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats
- ; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind
+ ; _ <- unifyKind (Just (ppr hs_lhs)) lhs_applied_kind res_kind
; traceTc "tcDataFamInstHeader" $
vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind ]
@@ -891,19 +891,20 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
, lhs_applied_kind
, res_kind ) }
- -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
-- This code (and the stuff immediately above) is very similar
-- to that in tcTyFamInstEqnGuts. Maybe we should abstract the
-- common code; but for the moment I concluded that it's
-- clearer to duplicate it. Still, if you fix a bug here,
-- check there too!
- ; let scoped_tvs = imp_tvs ++ exp_tvs
- ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs)
+
+ -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts]
+ ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys (imp_tvs ++ exp_tvs))
; qtvs <- quantifyTyVars dvs
+ ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted
-- Zonk the patterns etc into the Type world
; (ze, qtvs) <- zonkTyBndrs qtvs
- ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
+ ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty
; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
; master_res_kind <- zonkTcTypeToTypeX ze master_res_kind
; instance_res_kind <- zonkTcTypeToTypeX ze instance_res_kind
@@ -925,9 +926,9 @@ 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
+ exp_bndrs = mb_bndrs `orElse` []
-- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, wrinkle (2).
tc_kind_sig Nothing
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index fd2d1f00ce..71f628aa3a 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -969,17 +969,23 @@ addHoles wc holes
dropMisleading :: WantedConstraints -> WantedConstraints
-- Drop misleading constraints; really just class constraints
-- See Note [Constraints and errors] in GHC.Tc.Utils.Monad
+-- for why this function is so strange, treating the 'simples'
+-- and the implications differently. Sigh.
dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
- = WC { wc_simple = filterBag keep_ct simples
+ = WC { wc_simple = filterBag insolubleCt simples
, wc_impl = mapBag drop_implic implics
, wc_holes = filterBag isOutOfScopeHole holes }
where
drop_implic implic
- = implic { ic_wanted = dropMisleading (ic_wanted implic) }
- keep_ct ct
- = case classifyPredType (ctPred ct) of
- ClassPred {} -> False
- _ -> True
+ = implic { ic_wanted = drop_wanted (ic_wanted implic) }
+ drop_wanted (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
+ = WC { wc_simple = filterBag keep_ct simples
+ , wc_impl = mapBag drop_implic implics
+ , wc_holes = filterBag isOutOfScopeHole holes }
+
+ keep_ct ct = case classifyPredType (ctPred ct) of
+ ClassPred {} -> False
+ _ -> True
isSolvedStatus :: ImplicStatus -> Bool
isSolvedStatus (IC_Solved {}) = True
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index 985cbae01b..9d46f8ba16 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/compiler/GHC/Tc/Types/Evidence.hs
@@ -461,7 +461,7 @@ use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
evidence bindings are allowed. Notebly ():
- Places in types where we are solving kind constraints (all of which
- are equalities); see solveEqualities, solveLocalEqualities
+ are equalities); see solveEqualities
- When unifying forall-types
-}
@@ -763,7 +763,7 @@ important) are solved in three steps:
EvCsEmpty
- (see GHC.Tc.Solver.simpl_top and GHC.Tc.Solver.defaultCallStacks)
+ (see GHC.Tc.Solver.simplifyTopWanteds and GHC.Tc.Solver.defaultCallStacks)
This provides a lightweight mechanism for building up call-stacks
explicitly, but is notably limited by the fact that the stack will
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index 96bff3d261..f50cab2bb7 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -1816,10 +1816,33 @@ Here 'p' is out of scope, so we get an insoluble Hole constraint. But
the visible type application fails in the monad (throws an exception).
We must not discard the out-of-scope error.
-So we /retain the insoluble constraints/ if there is an exception.
-Hence:
- - insolublesOnly in tryCaptureConstraints
- - emitConstraints in the Left case of captureConstraints
+It's distressingly delicate though:
+
+* If we discard too /many/ constraints we may fail to report the error
+ that led us to interrupte the constraint gathering process.
+
+ One particular example "variable out of scope" Hole constraints. For
+ example (#12529):
+ f = p @ Int
+ Here 'p' is out of scope, so we get an insoluble Hole constraint. But
+ 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.
+
+* If we discard too /few/ constraints, we may get the misleading
+ class constraints mentioned above. But we may /also/ end up taking
+ constraints built at some inner level, and emitting them at some
+ outer level, and then breaking the TcLevel invariants
+ See Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType
+
+So dropMisleading has a horridly ad-hoc structure. It keeps only
+/insoluble/ flat constraints (which are unlikely to very visibly trip
+up on the TcLevel invariant, but all /implication/ constraints (except
+the class constraints inside them). The implication constraints are
+OK because they set the ambient level before attempting to solve any
+inner constraints. Ugh! I hate this. But it seems to work.
However note that freshly-generated constraints like (Int ~ Bool), or
((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 62e39879d7..88c354fd80 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -4,7 +4,7 @@
-}
-{-# LANGUAGE CPP, TupleSections, MultiWayIf, PatternSynonyms #-}
+{-# LANGUAGE CPP, TupleSections, MultiWayIf, PatternSynonyms, BangPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -21,9 +21,9 @@ module GHC.Tc.Utils.TcMType (
newNamedFlexiTyVar,
newFlexiTyVarTy, -- Kind -> TcM TcType
newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
- newOpenFlexiTyVarTy, newOpenTypeKind,
+ newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind,
newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
- cloneMetaTyVar,
+ newAnonMetaTyVar, cloneMetaTyVar,
newFmvTyVar, newFskTyVar,
newMultiplicityVar,
@@ -70,19 +70,23 @@ module GHC.Tc.Utils.TcMType (
zonkTcTyVarToTyVar, zonkInvisTVBinder,
zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV,
zonkTyCoVarsAndFVList,
- candidateQTyVarsOfType, candidateQTyVarsOfKind,
- candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
- CandidatesQTvs(..), delCandidates, candidateKindVars, partitionCandidates,
- zonkAndSkolemise, skolemiseQuantifiedTyVar,
- defaultTyVar, quantifyTyVars, isQuantifiableTv,
+
zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind, zonkTyCoVarKindBinder,
-
zonkEvVar, zonkWC, zonkImplication, zonkSimples,
zonkId, zonkCoVar,
zonkCt, zonkSkolemInfo,
- skolemiseUnboundMetaTyVar,
+ ---------------------------------
+ -- Promotion, defaulting, skolemisation
+ defaultTyVar, promoteTyVar, promoteTyVarSet,
+ quantifyTyVars, isQuantifiableTv,
+ skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar,
+
+ candidateQTyVarsOfType, candidateQTyVarsOfKind,
+ candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
+ CandidatesQTvs(..), delCandidates,
+ candidateKindVars, partitionCandidates,
------------------------------
-- Levity polymorphism
@@ -464,7 +468,7 @@ readExpType exp_ty
-- | Returns the expected type when in checking mode.
checkingExpType_maybe :: ExpType -> Maybe TcType
checkingExpType_maybe (Check ty) = Just ty
-checkingExpType_maybe _ = Nothing
+checkingExpType_maybe (Infer {}) = Nothing
-- | Returns the expected type when in checking mode. Panics if in inference
-- mode.
@@ -759,7 +763,6 @@ the thinking.
{- Note [TyVarTv]
~~~~~~~~~~~~~~~~~
-
A TyVarTv can unify with type *variables* only, including other TyVarTvs and
skolems. Sometimes, they can unify with type variables that the user would
rather keep distinct; see #11203 for an example. So, any client of this
@@ -774,7 +777,7 @@ types (GHC Proposal 29).
The remaining uses of newTyVarTyVars are
* In kind signatures, see
GHC.Tc.TyCl Note [Inferring kinds for type declarations]
- and Note [Kind checking for GADTs]
+ and Note [Kind checking for GADTs]
* In partial type signatures, see Note [Quantified variables in partial type signatures]
-}
@@ -1080,8 +1083,13 @@ newOpenTypeKind
-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
+ = do { tv <- newOpenFlexiTyVar
+ ; return (mkTyVarTy tv) }
+
+newOpenFlexiTyVar :: TcM TcTyVar
+newOpenFlexiTyVar
= do { kind <- newOpenTypeKind
- ; newFlexiTyVarTy kind }
+ ; newFlexiTyVar kind }
newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- Instantiate with META type variables
@@ -1619,11 +1627,11 @@ alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for
generalisation, and so we generalise it. alpha[1] does not, and so
we leave it alone.
-Note that not *every* variable with a higher level will get generalised,
-either due to the monomorphism restriction or other quirks. See, for
-example, the code in GHC.Tc.Solver.decideMonoTyVars and in
-GHC.Tc.Gen.HsType.kindGeneralizeSome, both of which exclude certain otherwise-eligible
-variables from being generalised.
+Note that not *every* variable with a higher level will get
+generalised, either due to the monomorphism restriction or other
+quirks. See, for example, the code in GHC.Tc.Solver.decideMonoTyVars
+and in GHC.Tc.Gen.HsType.kindGeneralizeSome, both of which exclude
+certain otherwise-eligible variables from being generalised.
Using level numbers for quantification is implemented in the candidateQTyVars...
functions, by adding only those variables with a level strictly higher than
@@ -1643,10 +1651,9 @@ For more information about deterministic sets see
Note [Deterministic UniqFM] in GHC.Types.Unique.DFM.
-}
-quantifyTyVars
- :: CandidatesQTvs -- See Note [Dependent type variables]
- -- Already zonked
- -> TcM [TcTyVar]
+quantifyTyVars :: CandidatesQTvs -- See Note [Dependent type variables]
+ -- Already zonked
+ -> TcM [TcTyVar]
-- See Note [quantifyTyVars]
-- Can be given a mixture of TcTyVars and TyVars, in the case of
-- associated type declarations. Also accepts covars, but *never* returns any.
@@ -1654,28 +1661,28 @@ quantifyTyVars
-- invariants on CandidateQTvs, we do not have to filter out variables
-- free in the environment here. Just quantify unconditionally, subject
-- to the restrictions in Note [quantifyTyVars].
-quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
+quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set })
-- short-circuit common case
- | isEmptyDVarSet dep_tkvs
- , isEmptyDVarSet nondep_tkvs
+ | isEmptyDVarSet dep_kv_set
+ , isEmptyDVarSet nondep_tkv_set
= do { traceTc "quantifyTyVars has nothing to quantify" empty
; return [] }
| otherwise
- = do { traceTc "quantifyTyVars 1" (ppr dvs)
+ = do { traceTc "quantifyTyVars {" (ppr dvs)
- ; let dep_kvs = scopedSort $ dVarSetElems dep_tkvs
- -- scopedSort: put the kind variables into
- -- well-scoped order.
- -- E.g. [k, (a::k)] not the other way round
+ ; let dep_kvs = scopedSort $ dVarSetElems dep_kv_set
+ -- scopedSort: put the kind variables into
+ -- well-scoped order.
+ -- E.g. [k, (a::k)] not the other way round
- nondep_tvs = dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs)
+ nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set)
-- See Note [Dependent type variables]
-- The `minus` dep_tkvs removes any kind-level vars
-- e.g. T k (a::k) Since k appear in a kind it'll
-- be in dv_kvs, and is dependent. So remove it from
-- dv_tvs which will also contain k
- -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
+ -- NB kinds of tvs are already zonked
-- In the non-PolyKinds case, default the kind variables
-- to *, and zonk the tyvars as usual. Notice that this
@@ -1689,7 +1696,7 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
-- mentioned in the kinds of the nondep_tvs'
-- now refer to the dep_kvs'
- ; traceTc "quantifyTyVars 2"
+ ; traceTc "quantifyTyVars }"
(vcat [ text "nondep:" <+> pprTyVars nondep_tvs
, text "dep:" <+> pprTyVars dep_kvs
, text "dep_kvs'" <+> pprTyVars dep_kvs'
@@ -2018,14 +2025,45 @@ Consider this:
All very silly. I think its harmless to ignore the problem. We'll end up with
a \/\a in the final result but all the occurrences of a will be zonked to ()
+-}
-************************************************************************
+{- *********************************************************************
* *
- Zonking types
+ Promotion
* *
-************************************************************************
+********************************************************************* -}
--}
+promoteTyVar :: TcTyVar -> TcM Bool
+-- When we float a constraint out of an implication we must restore
+-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType
+-- Return True <=> we did some promotion
+-- Also returns either the original tyvar (no promotion) or the new one
+-- See Note [Promoting unification variables]
+promoteTyVar tv
+ = do { tclvl <- getTcLevel
+ ; if (isFloatedTouchableMetaTyVar tclvl tv)
+ then do { cloned_tv <- cloneMetaTyVar tv
+ ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl
+ ; writeMetaTyVar tv (mkTyVarTy rhs_tv)
+ ; traceTc "promoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv)
+ ; return True }
+ else do { traceTc "promoteTyVar: no" (ppr tv)
+ ; return False } }
+
+-- Returns whether or not *any* tyvar is defaulted
+promoteTyVarSet :: TcTyVarSet -> TcM Bool
+promoteTyVarSet tvs
+ = do { bools <- mapM promoteTyVar (nonDetEltsUniqSet tvs)
+ -- Non-determinism is OK because order of promotion doesn't matter
+
+ ; return (or bools) }
+
+
+{- *********************************************************************
+* *
+ Zonking types
+* *
+********************************************************************* -}
zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
-- Zonk a type and take its free variables
View Lorry Controller Status