[Git][ghc/ghc][wip/T25266] Improve the generalisation code in Solver.simplifyInfer
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Oct 18 08:01:45 UTC 2024
Simon Peyton Jones pushed to branch wip/T25266 at Glasgow Haskell Compiler / GHC
Commits:
c2694cb7 by Simon Peyton Jones at 2024-10-18T09:01:11+01:00
Improve the generalisation code in Solver.simplifyInfer
The code in `decideQuantification` has become quite complicated.
This MR straightens it out, adds a new Note, and on the way
fixes #25266.
See especially Note [decideAndPromoteTyVars] which is is where
all the action happens in this MR.
- - - - -
23 changed files:
- compiler/GHC/Data/Bag.hs
- compiler/GHC/Tc/Deriv/Infer.hs
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Instance/FunDeps.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Default.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/TyCl/PatSyn.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
- testsuite/tests/partial-sigs/should_fail/T10615.stderr
- testsuite/tests/polykinds/T14172.stderr
- testsuite/tests/typecheck/should_compile/T13785.hs
- testsuite/tests/typecheck/should_compile/T13785.stderr
- + testsuite/tests/typecheck/should_compile/T25266.hs
- + testsuite/tests/typecheck/should_compile/T25266a.hs
- + testsuite/tests/typecheck/should_compile/T25266a.stderr
- + testsuite/tests/typecheck/should_compile/T25266b.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T18398.stderr
Changes:
=====================================
compiler/GHC/Data/Bag.hs
=====================================
@@ -16,7 +16,7 @@ module GHC.Data.Bag (
mapBag, pprBag,
elemBag, lengthBag,
filterBag, partitionBag, partitionBagWith,
- concatBag, catBagMaybes, foldBag,
+ concatBag, catBagMaybes, foldBag_flip,
isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, allBag,
listToBag, nonEmptyToBag, bagToList, headMaybe, mapAccumBagL,
concatMapBag, concatMapBagPair, mapMaybeBag, mapMaybeBagM, unzipBag,
@@ -194,24 +194,10 @@ partitionBagWith pred (TwoBags b1 b2)
partitionBagWith pred (ListBag vs) = (listToBag sats, listToBag fails)
where (sats, fails) = partitionWith pred (toList vs)
-foldBag :: (r -> r -> r) -- Replace TwoBags with this; should be associative
- -> (a -> r) -- Replace UnitBag with this
- -> r -- Replace EmptyBag with this
- -> Bag a
- -> r
-
-{- Standard definition
-foldBag t u e EmptyBag = e
-foldBag t u e (UnitBag x) = u x
-foldBag t u e (TwoBags b1 b2) = (foldBag t u e b1) `t` (foldBag t u e b2)
-foldBag t u e (ListBag xs) = foldr (t.u) e xs
--}
-
--- More tail-recursive definition, exploiting associativity of "t"
-foldBag _ _ e EmptyBag = e
-foldBag t u e (UnitBag x) = u x `t` e
-foldBag t u e (TwoBags b1 b2) = foldBag t u (foldBag t u e b2) b1
-foldBag t u e (ListBag xs) = foldr (t.u) e xs
+foldBag_flip :: (a -> b -> b) -> Bag a -> b -> b
+-- Just foldr with flipped arguments,
+-- so it can be chained more nicely
+foldBag_flip k bag z = foldr k z bag
mapBag :: (a -> b) -> Bag a -> Bag b
mapBag = fmap
=====================================
compiler/GHC/Tc/Deriv/Infer.hs
=====================================
@@ -763,9 +763,11 @@ simplifyDeriv (DS { ds_loc = loc, ds_tvs = tvs
-- See [STEP DAC HOIST]
-- From the simplified constraints extract a subset 'good' that will
-- become the context 'min_theta' for the derived instance.
- ; let residual_simple = approximateWC True solved_wanteds
- head_size = pSizeClassPred clas inst_tys
- good = mapMaybeBag get_good residual_simple
+ ; let residual_simple = approximateWC False solved_wanteds
+ -- False: ignore any non-quantifiable constraints,
+ -- including equalities hidden under Given equalities
+ head_size = pSizeClassPred clas inst_tys
+ good = mapMaybeBag get_good residual_simple
-- Returns @Just p@ (where @p@ is the type of the Ct) if a Ct is
-- suitable to be inferred in the context of a derived instance.
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -490,8 +490,8 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc closed bind_list
; let plan = decideGeneralisationPlan dflags top_lvl closed sig_fn bind_list
; traceTc "Generalisation plan" (ppr plan)
; result@(_, scaled_poly_ids) <- case plan of
- NoGen -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
- InferGen -> tcPolyInfer rec_tc prag_fn sig_fn bind_list
+ NoGen -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
+ InferGen -> tcPolyInfer top_lvl rec_tc prag_fn sig_fn bind_list
CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind
; let poly_ids = map scaledThing scaled_poly_ids
@@ -708,12 +708,13 @@ To address this we to do a few things
-}
tcPolyInfer
- :: RecFlag -- Whether it's recursive after breaking
+ :: TopLevelFlag
+ -> RecFlag -- Whether it's recursive after breaking
-- dependencies based on type signatures
-> TcPragEnv -> TcSigFun
-> [LHsBind GhcRn]
-> TcM (LHsBinds GhcTc, [Scaled TcId])
-tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
+tcPolyInfer top_lvl rec_tc prag_fn tc_sig_fn bind_list
= do { (tclvl, wanted, (binds', mono_infos))
<- pushLevelAndCaptureConstraints $
tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
@@ -733,7 +734,7 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
; ((qtvs, givens, ev_binds, insoluble), residual)
- <- captureConstraints $ simplifyInfer tclvl infer_mode sigs name_taus wanted
+ <- captureConstraints $ simplifyInfer top_lvl tclvl infer_mode sigs name_taus wanted
; let inferred_theta = map evVarPred givens
; scaled_exports <- checkNoErrs $
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -696,7 +696,8 @@ tcExprSig expr sig@(TcPartialSig (PSig { psig_name = name, psig_loc = loc }))
| otherwise
= NoRestrictions
; ((qtvs, givens, ev_binds, _), residual)
- <- captureConstraints $ simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
+ <- captureConstraints $
+ simplifyInfer NotTopLevel tclvl infer_mode [sig_inst] [(name, tau)] wanted
; emitConstraints residual
; tau <- liftZonkM $ zonkTcType tau
=====================================
compiler/GHC/Tc/Instance/FunDeps.hs
=====================================
@@ -578,11 +578,22 @@ closeWrtFunDeps preds fixed_tvs
= case classifyPredType pred of
EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
-- See Note [Equality superclasses]
- ClassPred cls tys -> [ instFD fd cls_tvs tys
- | let (cls_tvs, cls_fds) = classTvsFds cls
- , fd <- cls_fds ]
+
+ ClassPred cls tys | not (isIPClass cls)
+ -- isIPClass: see Note [closeWrtFunDeps ignores implicit parameters]
+ -> [ instFD fd cls_tvs tys
+ | let (cls_tvs, cls_fds) = classTvsFds cls
+ , fd <- cls_fds ]
_ -> []
+{- Note [closeWrtFunDeps ignores implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Implicit params don't really determine a type variable (that is, we might have
+IP "c" Bool and IP "c" Int in different places within the same program), and
+skipping this causes implicit params to monomorphise too many variables; see
+Note [Inheriting implicit parameters] in GHC.Tc.Solver. Skipping causes
+typecheck/should_compile/tc219 to fail.
+-}
{- *********************************************************************
* *
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -2582,7 +2582,7 @@ tcRnExpr hsc_env mode rdr_expr
let { fresh_it = itName uniq (getLocA rdr_expr) } ;
((qtvs, dicts, _, _), residual)
<- captureConstraints $
- simplifyInfer tclvl infer_mode
+ simplifyInfer TopLevel tclvl infer_mode
[] {- No sig vars -}
[(fresh_it, res_ty)]
lie ;
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -14,6 +14,7 @@ module GHC.Tc.Solver(
tcCheckGivens,
tcCheckWanteds,
tcNormalise,
+ approximateWC, -- Exported for plugins to use
captureTopConstraints,
@@ -48,7 +49,7 @@ import GHC.Tc.Utils.TcType
import GHC.Core.Predicate
import GHC.Core.Type
import GHC.Core.Ppr
-import GHC.Core.TyCon ( TyConBinder, isTypeFamilyTyCon )
+import GHC.Core.TyCon ( TyConBinder )
import GHC.Types.Name
import GHC.Types.Id
@@ -58,9 +59,11 @@ import GHC.Types.Var.Set
import GHC.Types.Basic
import GHC.Types.Error
-import GHC.Utils.Misc
+import GHC.Driver.DynFlags( DynFlags, xopt )
+import GHC.Driver.Flags( WarningFlag(..) )
import GHC.Utils.Panic
import GHC.Utils.Outputable
+import GHC.Utils.Misc( filterOut )
import GHC.Data.Bag
@@ -882,7 +885,8 @@ instance Outputable InferMode where
ppr EagerDefaulting = text "EagerDefaulting"
ppr NoRestrictions = text "NoRestrictions"
-simplifyInfer :: TcLevel -- Used when generating the constraints
+simplifyInfer :: TopLevelFlag
+ -> TcLevel -- Used when generating the constraints
-> InferMode
-> [TcIdSigInst] -- Any signatures (possibly partial)
-> [(Name, TcTauType)] -- Variables to be generalised,
@@ -893,7 +897,7 @@ simplifyInfer :: TcLevel -- Used when generating the constraints
TcEvBinds, -- ... binding these evidence variables
Bool) -- True <=> the residual constraints are insoluble
-simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
+simplifyInfer top_lvl rhs_tclvl infer_mode sigs name_taus wanteds
| isEmptyWC wanteds
= do { -- When quantifying, we want to preserve any order of variables as they
-- appear in partial signatures. cf. decideQuantifiedTyVars
@@ -946,9 +950,8 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
; wanted_transformed <- TcM.liftZonkM $ TcM.zonkWC wanted_transformed
; let definite_error = insolubleWC wanted_transformed
-- See Note [Quantification with errors]
- quant_pred_candidates
- | definite_error = []
- | otherwise = ctsPreds (approximateWC False wanted_transformed)
+ wanted_dq | definite_error = emptyWC
+ | otherwise = wanted_transformed
-- Decide what type variables and constraints to quantify
-- NB: quant_pred_candidates is already fully zonked
@@ -957,9 +960,11 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
-- NB: bound_theta are fully zonked
-- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
-- in GHC.Tc.Utils.TcType
- ; rec { (qtvs, bound_theta, co_vars) <- decideQuantification skol_info infer_mode rhs_tclvl
- name_taus partial_sigs
- quant_pred_candidates
+ ; rec { (qtvs, bound_theta, co_vars) <- decideQuantification
+ top_lvl rhs_tclvl infer_mode
+ skol_info name_taus partial_sigs
+ wanted_dq
+
; bound_theta_vars <- mapM TcM.newEvVar bound_theta
; let full_theta = map idType bound_theta_vars
@@ -975,7 +980,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
-- All done!
; traceTc "} simplifyInfer/produced residual implication for quantification" $
- vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
+ vcat [ text "wanted_dq =" <+> ppr wanted_dq
, text "psig_theta =" <+> ppr psig_theta
, text "bound_theta =" <+> pprCoreBinders bound_theta_vars
, text "qtvs =" <+> ppr qtvs
@@ -1278,20 +1283,21 @@ simplifyInfer.
-}
decideQuantification
- :: SkolemInfo
- -> InferMode
+ :: TopLevelFlag
-> TcLevel
+ -> InferMode
+ -> SkolemInfo
-> [(Name, TcTauType)] -- Variables to be generalised
-> [TcIdSigInst] -- Partial type signatures (if any)
- -> [PredType] -- Candidate theta; already zonked
+ -> WantedConstraints -- Candidate theta; already zonked
-> TcM ( [TcTyVar] -- Quantify over these (skolems)
, [PredType] -- and this context (fully zonked)
, CoVarSet)
-- See Note [Deciding quantification]
-decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
+decideQuantification top_lvl rhs_tclvl infer_mode skol_info name_taus psigs wanted
= do { -- Step 1: find the mono_tvs
- ; (candidates, co_vars, mono_tvs0)
- <- decidePromotedTyVars infer_mode name_taus psigs candidates
+ ; (candidates, co_vars)
+ <- decideAndPromoteTyVars top_lvl rhs_tclvl infer_mode name_taus psigs wanted
-- Step 2: default any non-mono tyvars, and re-simplify
-- This step may do some unification, but result candidates is zonked
@@ -1308,11 +1314,11 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
do { candidates <- TcM.zonkTcTypes candidates
; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
; return (candidates, psig_theta) }
- ; min_theta <- pickQuantifiablePreds (mkVarSet qtvs) mono_tvs0 candidates
-- Take account of partial type signatures
-- See Note [Constraints in partial type signatures]
; let min_psig_theta = mkMinimalBySCs id psig_theta
+ min_theta = pickQuantifiablePreds (mkVarSet qtvs) candidates
; theta <- if
| null psigs -> return min_theta -- Case (P3)
| not (all has_extra_constraints_wildcard psigs) -- Case (P2)
@@ -1396,147 +1402,376 @@ Some rationale and observations
g :: forall b. Show b => F b -> _ -> b
g x y = let _ = (f y, show x) in x
But that's a battle for another day.
+
+Note [Generalising top-level bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ class C a b | a -> b where ..
+ f x = ...[W] C Int beta[1]...
+
+When generalising `f`, closeWrtFunDeps will promote beta[1] to beta[0].
+But we do NOT want to make a top level type
+ f :: C Int beta[0] => blah
+The danger is that beta[0] is defaulted to Any, and that then appears
+in a user error message. Even if the type `blah` mentions beta[0], /and/
+there is a call that fixes beta[0] to (say) Bool, we'll end up with
+[W] C Int Bool, which is insoluble. Why insoluble? If there was an
+ instance C Int Bool
+then fundeps would have fixed beta:=Bool in the first place.
+
+If the binding of `f` is nested, things are different: we can
+definitely see all the calls.
+
+For nested bindings, I think it just doesn't matter. No one cares what this
+variable ends up being; it seems silly to halt compilation around it. (Like in
+the length [] case.)
-}
-decidePromotedTyVars :: InferMode
- -> [(Name,TcType)]
- -> [TcIdSigInst]
- -> [PredType]
- -> TcM ([PredType], CoVarSet, TcTyVarSet)
--- We are about to generalise over type variables at level N
--- Each must be either
--- (P) promoted
--- (D) defaulted
--- (Q) quantified
--- This function finds (P), the type variables that we are going to promote:
--- (a) Mentioned in a constraint we can't generalise (the MR)
--- (b) Mentioned in the kind of a CoVar; we can't quantify over a CoVar,
--- so we must not quantify over a type variable free in its kind
--- (c) Connected by an equality or fundep to
--- * a type variable at level < N, or
--- * A tyvar subject to (a), (b) or (c)
--- Having found all such level-N tyvars that we can't generalise,
--- promote them, to eliminate them from further consideration.
---
--- Also return CoVars that appear free in the final quantified types
--- we can't quantify over these, and we must make sure they are in scope
-decidePromotedTyVars infer_mode name_taus psigs candidates
- = do { tc_lvl <- TcM.getTcLevel
- ; (no_quant, maybe_quant) <- pick infer_mode candidates
+decideAndPromoteTyVars :: TopLevelFlag -> TcLevel
+ -> InferMode
+ -> [(Name,TcType)]
+ -> [TcIdSigInst]
+ -> WantedConstraints
+ -> TcM ([PredType], CoVarSet)
+-- See Note [decideAndPromoteTyVars]
+decideAndPromoteTyVars top_lvl rhs_tclvl infer_mode name_taus psigs wanted
+ = do { dflags <- getDynFlags
-- If possible, we quantify over partial-sig qtvs, so they are
-- not mono. Need to zonk them because they are meta-tyvar TyVarTvs
- ; (psig_qtvs, psig_theta, taus) <- TcM.liftZonkM $
- do { psig_qtvs <- zonkTcTyVarsToTcTyVars $ binderVars $
- concatMap (map snd . sig_inst_skols) psigs
- ; psig_theta <- mapM TcM.zonkTcType $
- concatMap sig_inst_theta psigs
- ; taus <- mapM (TcM.zonkTcType . snd) name_taus
- ; return (psig_qtvs, psig_theta, taus) }
+ ; (psig_qtvs, psig_theta, tau_tys) <- getSeedTys name_taus psigs
- ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
+ ; let is_top_level = isTopLevel top_lvl -- A syntactically top-level binding
- -- (b) The co_var_tvs are tvs mentioned in the types of covars or
+ -- Step 1 of Note [decideAndPromoteTyVars]
+ -- Get candidate constraints, decide which we can potentially quantify
+ (can_quant_cts, no_quant_cts) = approximateWCX wanted
+ can_quant = ctsPreds can_quant_cts
+ no_quant = ctsPreds no_quant_cts
+
+ -- Step 2 of Note [decideAndPromoteTyVars]
+ -- Apply the monomorphism restriction
+ (post_mr_quant, mr_no_quant) = applyMR dflags infer_mode can_quant
+
+ -- The co_var_tvs are tvs mentioned in the types of covars or
-- coercion holes. We can't quantify over these covars, so we
-- must include the variable in their types in the mono_tvs.
-- E.g. If we can't quantify over co :: k~Type, then we can't
-- quantify over k either! Hence closeOverKinds
-- Recall that coVarsOfTypes also returns coercion holes
- co_vars = coVarsOfTypes (psig_tys ++ taus ++ candidates)
+ co_vars = coVarsOfTypes (mkTyVarTys psig_qtvs ++ psig_theta
+ ++ tau_tys ++ post_mr_quant)
co_var_tvs = closeOverKinds co_vars
- mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
- tyCoVarsOfTypes candidates
- -- We need to grab all the non-quantifiable tyvars in the
- -- types so that we can grow this set to find other
- -- non-quantifiable tyvars. This can happen with something like
- -- f x y = ...
- -- where z = x 3
- -- The body of z tries to unify the type of x (call it alpha[1])
- -- with (beta[2] -> gamma[2]). This unification fails because
- -- alpha is untouchable, leaving [W] alpha[1] ~ (beta[2] -> gamma[2]).
- -- We need to know not to quantify over beta or gamma, because they
- -- are in the equality constraint with alpha. Actual test case:
- -- typecheck/should_compile/tc213
-
- mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
-
- -- mono_tvs1 is now the set of variables from an outer scope
- -- (that's mono_tvs0) and the set of covars, closed over kinds.
- -- Given this set of variables we know we will not quantify,
- -- we want to find any other variables that are determined by this
- -- set, by functional dependencies or equalities. We thus use
- -- closeWrtFunDeps to find all further variables determined by this root
- -- set. See Note [growThetaTyVars vs closeWrtFunDeps]
-
- non_ip_candidates = filterOut isIPLikePred candidates
- -- implicit params don't really determine a type variable
- -- (that is, we might have IP "c" Bool and IP "c" Int in different
- -- places within the same program), and
- -- skipping this causes implicit params to monomorphise too many
- -- variables; see Note [Inheriting implicit parameters] in GHC.Tc.Solver.
- -- Skipping causes typecheck/should_compile/tc219 to fail.
-
- mono_tvs2 = closeWrtFunDeps non_ip_candidates mono_tvs1
- -- mono_tvs2 now contains any variable determined by the "root
- -- set" of monomorphic tyvars in mono_tvs1.
-
- constrained_tvs = filterVarSet (isQuantifiableTv tc_lvl) $
- closeWrtFunDeps non_ip_candidates (tyCoVarsOfTypes no_quant)
- `minusVarSet` mono_tvs2
- -- constrained_tvs: the tyvars that we are not going to
- -- quantify /solely/ because of the monomorphism restriction
- --
- -- (`minusVarSet` mono_tvs2): a type variable is only
- -- "constrained" (so that the MR bites) if it is not
- -- free in the environment (#13785) or is determined
- -- by some variable that is free in the env't
-
- mono_tvs = (mono_tvs2 `unionVarSet` constrained_tvs)
- `delVarSetList` psig_qtvs
- -- (`delVarSetList` psig_qtvs): if the user has explicitly
- -- asked for quantification, then that request "wins"
- -- over the MR.
- --
- -- What if a psig variable is also free in the environment
- -- (i.e. says "no" to isQuantifiableTv)? That's OK: explanation
- -- in Step 2 of Note [Deciding quantification].
-
- -- Warn about the monomorphism restriction
- ; when (case infer_mode of { ApplyMR -> True; _ -> False}) $ do
- let dia = TcRnMonomorphicBindings (map fst name_taus)
- diagnosticTc (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus) dia
-
- -- Promote the mono_tvs: see Note [Promote monomorphic tyvars]
- ; _ <- promoteTyVarSet mono_tvs
-
- ; traceTc "decidePromotedTyVars" $ vcat
- [ text "infer_mode =" <+> ppr infer_mode
+ -- outer_tvs are mentioned in `wanted, and belong to some outer level.
+ -- We definitely can't quantify over them
+ outer_tvs = outerLevelTyVars rhs_tclvl $
+ tyCoVarsOfTypes can_quant `unionVarSet` tyCoVarsOfTypes no_quant
+
+ -- Step 3 of Note [decideAndPromoteTyVars]
+ -- Identify mono_tvs: the type variables that we must not quantify over
+ mono_tvs_without_mr
+ | is_top_level = outer_tvs
+ | otherwise = outer_tvs -- (a)
+ `unionVarSet` tyCoVarsOfTypes no_quant -- (b)
+ `unionVarSet` co_var_tvs -- (c)
+
+ mono_tvs_with_mr
+ = -- Even at top level, we don't quantify over type variables
+ -- mentioned in constraints that the MR tells us not to quantify
+ -- See Note [decideAndPromoteTyVars] (DP2)
+ mono_tvs_without_mr `unionVarSet` tyCoVarsOfTypes mr_no_quant
+
+ --------------------------------------------------------------------
+ -- Step 4 of Note [decideAndPromoteTyVars]
+ -- Use closeWrtFunDeps to find any other variables that are determined by mono_tvs
+ add_determined tvs = closeWrtFunDeps post_mr_quant tvs
+ `delVarSetList` psig_qtvs
+ -- Why delVarSetList psig_qtvs?
+ -- If the user has explicitly asked for quantification, then that
+ -- request "wins" over the MR.
+ --
+ -- What if a psig variable is also free in the environment
+ -- (i.e. says "no" to isQuantifiableTv)? That's OK: explanation
+ -- in Step 2 of Note [Deciding quantification].
+
+ mono_tvs_with_mr_det = add_determined mono_tvs_with_mr
+ mono_tvs_without_mr_det = add_determined mono_tvs_without_mr
+
+ --------------------------------------------------------------------
+ -- Step 5 of Note [decideAndPromoteTyVars]
+ -- Do not quantify over any constraint mentioning a "newly-mono" tyvar.
+ newly_mono_tvs = mono_tvs_with_mr_det `minusVarSet` mono_tvs_with_mr
+ final_quant
+ | is_top_level = filterOut (predMentions newly_mono_tvs) post_mr_quant
+ | otherwise = post_mr_quant
+
+ --------------------------------------------------------------------
+ -- Check if the Monomorphism Restriction has bitten
+ ; warn_mr <- woptM Opt_WarnMonomorphism
+ ; when (warn_mr && case infer_mode of { ApplyMR -> True; _ -> False}) $
+ diagnosticTc (not (mono_tvs_with_mr_det `subVarSet` mono_tvs_without_mr_det)) $
+ TcRnMonomorphicBindings (map fst name_taus)
+ -- If there is a variable in mono_tvs, but not in mono_tvs_wo_mr
+ -- then the MR has "bitten" and reduced polymorphism.
+
+ --------------------------------------------------------------------
+ -- Step 6: Promote the mono_tvs: see Note [Promote monomorphic tyvars]
+ ; _ <- promoteTyVarSet mono_tvs_with_mr_det
+
+ ; traceTc "decideAndPromoteTyVars" $ vcat
+ [ text "rhs_tclvl =" <+> ppr rhs_tclvl
+ , text "top =" <+> ppr is_top_level
+ , text "infer_mode =" <+> ppr infer_mode
, text "psigs =" <+> ppr psigs
, text "psig_qtvs =" <+> ppr psig_qtvs
- , text "mono_tvs0 =" <+> ppr mono_tvs0
+ , text "outer_tvs =" <+> ppr outer_tvs
+ , text "mono_tvs_with_mr =" <+> ppr mono_tvs_with_mr
+ , text "mono_tvs_without_mr =" <+> ppr mono_tvs_without_mr
+ , text "mono_tvs_with_mr_det =" <+> ppr mono_tvs_with_mr_det
+ , text "mono_tvs_without_mr_det =" <+> ppr mono_tvs_without_mr_det
+ , text "newly_mono_tvs =" <+> ppr newly_mono_tvs
+ , text "can_quant =" <+> ppr can_quant
+ , text "post_mr_quant =" <+> ppr post_mr_quant
, text "no_quant =" <+> ppr no_quant
- , text "maybe_quant =" <+> ppr maybe_quant
- , text "mono_tvs =" <+> ppr mono_tvs
+ , text "mr_no_quant =" <+> ppr mr_no_quant
+ , text "final_quant =" <+> ppr final_quant
, text "co_vars =" <+> ppr co_vars ]
- ; return (maybe_quant, co_vars, mono_tvs0) }
+ ; return (final_quant, co_vars) }
+ -- We return `co_vars` that appear free in the final quantified types
+ -- we can't quantify over these, and we must make sure they are in scope
+
+-------------------
+applyMR :: DynFlags -> InferMode -> [PredType]
+ -> ( [PredType] -- Quantify over these
+ , [PredType] ) -- But not over these
+-- Split the candidates into ones we definitely
+-- won't quantify, and ones that we might
+applyMR _ NoRestrictions cand = (cand, [])
+applyMR _ ApplyMR cand = ([], cand)
+applyMR dflags EagerDefaulting cand = partition not_int_ct cand
where
- pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
- -- Split the candidates into ones we definitely
- -- won't quantify, and ones that we might
- pick ApplyMR cand = return (cand, [])
- pick NoRestrictions cand = return ([], cand)
- pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings
- ; return (partition (is_int_ct os) cand) }
-
- -- is_int_ct returns True for a constraint we should /not/ quantify
+ ovl_strings = xopt LangExt.OverloadedStrings dflags
+
+ -- not_int_ct returns True for a constraint we /can/ quantify
-- For EagerDefaulting, do not quantify over
-- over any interactive class constraint
- is_int_ct ovl_strings pred
+ not_int_ct pred
= case classifyPredType pred of
- ClassPred cls _ -> isInteractiveClass ovl_strings cls
- _ -> False
+ ClassPred cls _ -> not (isInteractiveClass ovl_strings cls)
+ _ -> True
+
+-------------------
+outerLevelTyVars :: TcLevel -> TcTyVarSet -> TcTyVarSet
+-- Find just the tyvars that are bound outside rhs_tc_lvl
+outerLevelTyVars rhs_tclvl tvs
+ = filterVarSet is_outer_tv tvs
+ where
+ is_outer_tv tcv
+ | isTcTyVar tcv -- Might be a CoVar; change this when gather covars separately
+ = rhs_tclvl `strictlyDeeperThan` tcTyVarLevel tcv
+ | otherwise
+ = False
+
+{- Note [decideAndPromoteTyVars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We are about to generalise a let-binding at "outer level" N, where we have
+typechecked its RHS at "rhs level" N+1. Each tyvar must be either
+ (P) promoted
+ (D) defaulted
+ (Q) quantified
+The function `decideAndPromoteTyVars` figures out (P), the type variables
+mentioned in constraints should definitely not be quantified, and promotes them
+to the outer level, namely N.
+
+The plan
+
+* Step 1. Use `approximateWCX` to extract, from the RHS `WantedConstraints`,
+ the PredTypes that we might quantify over; and also those that we can't.
+ Example: suppose the `wanted` is this:
+ (d1:Eq alpha, forall b. (F b ~ a) => (co:t1 ~ t2), (d:Show alpha))
+ Then
+ can_quant = [Eq alpha, Show alpha]
+ no_quant = (t1 ~ t2)
+ We can't quantify over that (t1~t2) because of the enclosing equality (F b ~ a).
+
+ We also choose never to quantify over some forms of equality constraints.
+ Both this and the "given-equality" thing are described in
+ Note [Quantifying over equality constraints] in GHC.Tc.Types.Constraint.
+
+* Step 2. Further trim can_quant using the Monomorphism Restriction, yielding the
+ further `mr_no_quant` predicates that we won't quantify over; plus `post_mr_quant`,
+ which we can in principle quantify.
+
+* Step 3. Identify the type variables we definitely won't quantify, because they are:
+ a) From an outer level <=N anyway
+ b) Mentioned in a constraint we /can't/ quantify. See Wrinkle (DP1).
+ c) Mentioned in the kind of a CoVar; we can't quantify over a CoVar,
+ so we must not quantify over a type variable free in its kind
+ d) Mentioned in a constraint that the MR says we should not quantify.
+
+ There is a special case for top-level bindings: see Wrinkle (DP2).
+
+* Step 4. Close wrt functional dependencies and equalities.Example
+ Example
+ f x y = ...
+ where z = x 3
+ The body of z tries to unify the type of x (call it alpha[1]) with
+ (beta[2] -> gamma[2]). This unification fails because alpha is untouchable, leaving
+ [W] alpha[1] ~ (beta[2] -> gamma[2])
+ We need to know not to quantify over beta or gamma, because they are in the
+ equality constraint with alpha. Actual test case: typecheck/should_compile/tc213
+
+ Another example. Suppose we have
+ class C a b | a -> b
+ and a constraint ([W] C alpha beta), if we promote alpha we should promote beta.
+
+ See also Note [growThetaTyVars vs closeWrtFunDeps]
+
+* Step 5. Further restrict the quantifiable constraints `post_mr_quant` to ones
+ that do not mention a "newly mono" tyvar. The "newly-mono" tyvars are the ones
+ not free in the envt, nor forced to be promoted by the MR; but are determined
+ (via fundeps) by them. Example:
+ class C a b | a -> b
+ [W] C Int beta[1], tau = beta[1]->Int
+ We promote beta[1] to beta[0] since it is determined by fundep, but we do not
+ want to generate f :: (C Int beta[0]) => beta[0] -> Int Rather, we generate
+ f :: beta[0] -> Int, but leave [W] C Int beta[0] in the residual constraints,
+ which will probably cause a type error
+
+ See Note [Do not quantify over constraints that determine a variable]
+
+* Step 6: actually promote the type variables we don't want to quantify.
+ We must do this: see Note [Promote monomorphic tyvars].
+
+We also add a warning that signals when the MR "bites".
+
+Wrinkles
+
+(DP1) In step 3, why (b)? Consider the example given in Step 1. we can't
+ quantify over the constraint (t1~t2). But if we quantify over the /tyvars/ in
+ t1 or t2, we may simply make that constraint insoluble (#25266 was an example).
+
+(DP2) In Step 3, for top-level bindings, we do (a,d), but /not/ (b,c). Reason:
+ see Note [The top-level Any principle]. At top level we are very reluctant to
+ promote type variables. But for bindings affected by the MR we have no choice
+ but to promote.
+
+Note [The top-level Any principle]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Key principle: we never want to show the programmer a type with `Any` in it.
+
+Most /top level/ bindings have a type signature, so none of this arises. But
+where a top-level binding lacks a signature, we don't want to infer a type like
+ f :: alpha[0] -> Int
+and then subsequently default alpha[0]:=Any. Exposing `Any` to the user is bad
+bad bad. Better to report an error, which is what may well happen if we
+quantify over alpha instead.
+
+For /nested/ bindings, a monomorphic type like `f :: alpha[0] -> Int` is fine,
+because we can see all the call sites of `f`, and they will probably fix
+`alpha`. In contrast, we can't see all of (or perhaps any of) the calls of
+top-level (exported) functions, reducing the worries about "spooky action at a
+distance".
+
+Note [Do not quantify over constraints that determine a variable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (typecheck/should_compile/tc231), where we're trying to infer
+the type of a top-level declaration. We have
+ class Zork s a b | a -> b
+and the candidate constraint at the end of simplifyInfer is
+ [W] Zork alpha[1] (Z [Char]) beta[1]
+We definitely want to quantify over `alpha` (which is mentioned in the
+tau-type).
+
+But we do *not* want to quantify over `beta`: it is determined by the
+functional dependency on Zork: note that the second argument to Zork
+in the Wanted is a variable-free `Z [Char]`. Quantifying over it
+would be "Henry Ford polymorphism". (Presumably we don't have an
+instance in scope that tells us what `beta` actually is.) Instead
+we promote `beta[1]` to `beta[0]`, in `decidePromotedTyVars`.
+
+The question here: do we want to quantify over the constraint, to
+give the type
+ forall a. Zork a (Z [Char]) beta[0] => blah
+Definitely not: see Note [The top-level Any principle]
+
+What we really want (to catch the Zork example) is this:
+
+ Quantify over the constraint only if all its free variables are
+ (a) quantified, or
+ (b) appears in the type of something in the environment (mono_tvs0).
+
+To understand (b) consider
+
+ class C a b where { op :: a -> b -> () }
+
+ mr = 3 -- mr :: alpha
+ f1 x = op x mr -- f1 :: forall b. b -> (), plus [W] C b alpha
+ intify = mr + (4 :: Int)
+
+In `f1` should we quantify over that `(C b alpha)`? Answer: since `alpha` is
+free in the type envt, yes we should. After all, if we'd typechecked `intify`
+first, we'd have set `alpha := Int`, and /then/ we'd certainly quantify. The
+delicate Zork situation applies when beta is completely unconstrained (not free
+in the environment) -- except by the fundep. Hence `newly_mono`.
+
+Another way to put it: let's say `alpha` is in `outer_tvs`. It must be that
+some variable `x` has `alpha` free in its type. If we are at top-level (and we
+are, because nested decls don't go through this path all), then `x` must also
+be at top-level. And, by induction, `x` will not have Any in its type when all
+is said and done. The induction is well-founded because, if `x` is mutually
+recursive with the definition at hand, then their constraints get processed
+together (or `x` has a type signature, in which case the type doesn't have
+`Any`). So the key thing is that we must not introduce a new top-level
+unconstrained variable here.
+
+However this regrettably-subtle reasoning is needed only for /top-level/
+declarations. For /nested/ decls we can see all the calls, so we'll instantiate
+that quantifed `Zork a (Z [Char]) beta` constraint at call sites, and either
+solve it or not (probably not). We won't be left with a still-callable function
+with Any in its type. So for nested definitions we don't make this tricky test.
+
+Historical note: we had a different, and more complicated test before, but it
+was utterly wrong: #23199.
+
+Note [Promote monomorphic tyvars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Promote any type variables that are free in the environment. Eg
+ f :: forall qtvs. bound_theta => zonked_tau
+The free vars of f's type become free in the envt, and hence will show
+up whenever 'f' is called. They may currently at rhs_tclvl, but they
+had better be unifiable at the outer_tclvl! Example: envt mentions
+alpha[1]
+ tau_ty = beta[2] -> beta[2]
+ constraints = alpha ~ [beta]
+we don't quantify over beta (since it is fixed by envt)
+so we must promote it! The inferred type is just
+ f :: beta -> beta
+
+NB: promoteTyVarSet ignores coercion variables
+
+Note [Defaulting during simplifyInfer]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we are inferring a type, we simplify the constraint, and then use
+approximateWC to produce a list of candidate constraints. Then we MUST
+
+ a) Promote any meta-tyvars that have been floated out by
+ approximateWC, to restore invariant (WantedInv) described in
+ Note [TcLevel invariants] in GHC.Tc.Utils.TcType.
+
+ b) Default the kind of any meta-tyvars that are not mentioned in
+ in the environment.
+
+To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
+have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
+should! If we don't solve the constraint, we'll stupidly quantify over
+(C (a->Int)) and, worse, in doing so skolemiseQuantifiedTyVar will quantify over
+(b:*) instead of (a:OpenKind), which can lead to disaster; see #7332.
+#7641 is a simpler example.
+
+-}
-------------------
defaultTyVarsAndSimplify :: TcLevel
@@ -1544,6 +1779,7 @@ defaultTyVarsAndSimplify :: TcLevel
-> TcM [PredType] -- Guaranteed zonked
-- Default any tyvar free in the constraints;
-- and re-simplify in case the defaulting allows further simplification
+-- See Note [Defaulting during simplifyInfer]
defaultTyVarsAndSimplify rhs_tclvl candidates
= do { -- Default any kind/levity vars
; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
@@ -1592,118 +1828,87 @@ decideQuantifiedTyVars skol_info name_taus psigs candidates
= do { -- Why psig_tys? We try to quantify over everything free in here
-- See Note [Quantification and partial signatures]
-- Wrinkles 2 and 3
- ; (psig_tv_tys, psig_theta, tau_tys) <- TcM.liftZonkM $
- do { psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
- , (_,Bndr tv _) <- sig_inst_skols sig ]
- ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
- , pred <- sig_inst_theta sig ]
- ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
- ; return (psig_tv_tys, psig_theta, tau_tys) }
-
- ; let -- Try to quantify over variables free in these types
- psig_tys = psig_tv_tys ++ psig_theta
- seed_tys = psig_tys ++ tau_tys
-
- -- Now "grow" those seeds to find ones reachable via 'candidates'
+ (psig_qtvs, psig_theta, tau_tys) <- getSeedTys name_taus psigs
+
+ ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
+ seed_tvs = tyCoVarsOfTypes (psig_tys ++ tau_tys)
+
+ -- "Grow" those seeds to find ones reachable via 'candidates'
-- See Note [growThetaTyVars vs closeWrtFunDeps]
- grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
+ grown_tcvs = growThetaTyVars candidates seed_tvs
-- Now we have to classify them into kind variables and type variables
-- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars
--
- -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces
- -- them in that order, so that the final qtvs quantifies in the same
- -- order as the partial signatures do (#13524)
- ; dv at DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} <- candidateQTyVarsOfTypes $
- psig_tys ++ candidates ++ tau_tys
+ -- The psig_tys are first in seed_tys, then candidates, then tau_tvs.
+ -- This makes candidateQTyVarsOfTypes produces them in that order, so that the
+ -- final qtvs quantifies in the same- order as the partial signatures do (#13524)
+ ; dv at DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
+ <- candidateQTyVarsOfTypes $
+ psig_tys ++ candidates ++ tau_tys
; let pick = (`dVarSetIntersectVarSet` grown_tcvs)
dvs_plus = dv { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
; traceTc "decideQuantifiedTyVars" (vcat
- [ text "tau_tys =" <+> ppr tau_tys
- , text "candidates =" <+> ppr candidates
+ [ text "candidates =" <+> ppr candidates
, text "cand_kvs =" <+> ppr cand_kvs
, text "cand_tvs =" <+> ppr cand_tvs
- , text "tau_tys =" <+> ppr tau_tys
- , text "seed_tys =" <+> ppr seed_tys
- , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
+ , text "seed_tys =" <+> ppr seed_tvs
, text "grown_tcvs =" <+> ppr grown_tcvs
, text "dvs =" <+> ppr dvs_plus])
; quantifyTyVars skol_info DefaultNonStandardTyVars dvs_plus }
------------------
+getSeedTys :: [(Name,TcType)] -- The type of each RHS in the group
+ -> [TcIdSigInst] -- Any partial type signatures
+ -> TcM ( [TcTyVar] -- Zonked partial-sig quantified tyvars
+ , ThetaType -- Zonked partial signature thetas
+ , [TcType] ) -- Zonked tau-tys from the bindings
+getSeedTys name_taus psigs
+ = TcM.liftZonkM $
+ do { psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | TISI{ sig_inst_skols = skols } <- psigs
+ , (_, Bndr tv _) <- skols ]
+ ; psig_theta <- mapM TcM.zonkTcType [ pred | TISI{ sig_inst_theta = theta } <- psigs
+ , pred <- theta ]
+ ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
+ ; return ( map getTyVar psig_tv_tys
+ , psig_theta
+ , tau_tys ) }
+
+------------------
+predMentions :: TcTyVarSet -> TcPredType -> Bool
+predMentions qtvs pred = tyCoVarsOfType pred `intersectsVarSet` qtvs
+
-- | When inferring types, should we quantify over a given predicate?
-- See Note [pickQuantifiablePreds]
pickQuantifiablePreds
:: TyVarSet -- Quantifying over these
- -> TcTyVarSet -- mono_tvs0: variables mentioned a candidate
- -- constraint that come from some outer level
-> TcThetaType -- Proposed constraints to quantify
- -> TcM TcThetaType -- A subset that we can actually quantify
+ -> TcThetaType -- A subset that we can actually quantify
-- This function decides whether a particular constraint should be
-- quantified over, given the type variables that are being quantified
-pickQuantifiablePreds qtvs mono_tvs0 theta
- = do { tc_lvl <- TcM.getTcLevel
- ; let is_nested = not (isTopTcLevel tc_lvl)
- ; return (mkMinimalBySCs id $ -- See Note [Minimize by Superclasses]
- mapMaybe (pick_me is_nested) theta) }
+pickQuantifiablePreds qtvs theta
+ = mkMinimalBySCs id $ -- See Note [Minimize by Superclasses]
+ mapMaybe pick_me theta
where
- pick_me is_nested pred
- = let pred_tvs = tyCoVarsOfType pred
- mentions_qtvs = pred_tvs `intersectsVarSet` qtvs
- in case classifyPredType pred of
-
- ClassPred cls tys
- | Just {} <- isCallStackPred cls tys
- -- NEVER infer a CallStack constraint. Otherwise we let
- -- the constraints bubble up to be solved from the outer
- -- context, or be defaulted when we reach the top-level.
- -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
- -> Nothing
-
+ pick_me pred
+ = case classifyPredType pred of
+ ClassPred cls _
| isIPClass cls
- -> Just pred -- See Note [Inheriting implicit parameters]
-
- | not mentions_qtvs
- -> Nothing -- Don't quantify over predicates that don't
- -- mention any of the quantified type variables
-
- | is_nested
- -> Just pred
-
- -- From here on, we are thinking about top-level defns only
-
- | pred_tvs `subVarSet` (qtvs `unionVarSet` mono_tvs0)
- -- See Note [Do not quantify over constraints that determine a variable]
- -> Just pred
-
- | otherwise
- -> Nothing
+ -> Just pred -- Pick, say, (?x::Int) whether or not it mentions qtvs
+ -- See Note [Inheriting implicit parameters]
EqPred eq_rel ty1 ty2
- | mentions_qtvs
- , quantify_equality eq_rel ty1 ty2
+ | predMentions qtvs pred
, Just (cls, tys) <- boxEqPred eq_rel ty1 ty2
-- boxEqPred: See Note [Lift equality constraints when quantifying]
-> Just (mkClassPred cls tys)
| otherwise
-> Nothing
- IrredPred {} | mentions_qtvs -> Just pred
- | otherwise -> Nothing
-
- ForAllPred {} -> Nothing
-
- -- See Note [Quantifying over equality constraints]
- quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2
- quantify_equality ReprEq _ _ = True
-
- quant_fun ty
- = case tcSplitTyConApp_maybe ty of
- Just (tc, tys) | isTypeFamilyTyCon tc
- -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs
- _ -> False
+ _ | predMentions qtvs pred -> Just pred
+ | otherwise -> Nothing
------------------
growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
@@ -1725,24 +1930,8 @@ growThetaTyVars theta tcvs
pred_tcvs = tyCoVarsOfType pred
-{- Note [Promote monomorphic tyvars]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Promote any type variables that are free in the environment. Eg
- f :: forall qtvs. bound_theta => zonked_tau
-The free vars of f's type become free in the envt, and hence will show
-up whenever 'f' is called. They may currently at rhs_tclvl, but they
-had better be unifiable at the outer_tclvl! Example: envt mentions
-alpha[1]
- tau_ty = beta[2] -> beta[2]
- constraints = alpha ~ [beta]
-we don't quantify over beta (since it is fixed by envt)
-so we must promote it! The inferred type is just
- f :: beta -> beta
-
-NB: promoteTyVarSet ignores coercion variables
-
-Note [pickQuantifiablePreds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [pickQuantifiablePreds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When pickQuantifiablePreds is called we have decided what type
variables to quantify over, `qtvs`. The only quesion is: which of the
unsolved candidate predicates should we quantify over? Call them
@@ -1754,58 +1943,37 @@ For the members of unsolved_constraints that we select for picked_theta
it is easy to solve, by identity. For the others we just hope that
we can solve them.
-So which of the candidates should we pick to quantify over? In some
-situations we distinguish top-level from nested bindings. The point
-about nested binding is that
- (a) the types may mention type variables free in the environment
- (b) all of the call sites are statically visible, reducing the
- worries about "spooky action at a distance".
-
-First, never pick a constraint that doesn't mention any of the quantified
-variables `qtvs`. Picking such a constraint essentially moves the solving of
-the constraint from this function definition to call sites. But because the
-constraint mentions no quantified variables, call sites have no advantage
-over the definition site. Well, not quite: there could be new constraints
-brought into scope by a pattern-match against a constrained (e.g. GADT)
-constructor. Example
-
- data T a where { T1 :: T1 Bool; ... }
-
- f :: forall a. a -> T a -> blah
- f x t = let g y = x&&y -- This needs a~Bool
- in case t of
- T1 -> g True
- ....
-
-At g's call site we have `a~Bool`, so we /could/ infer
- g :: forall . (a~Bool) => Bool -> Bool -- qtvs = {}
-
-This is all very contrived, and probably just postponse type errors to
-the call site. If that's what you want, write a type signature.
-
-Actually, implicit parameters is an exception to the "no quantified vars"
-rule (see Note [Inheriting implicit parameters]) so we can't actually
-simply test this case first.
-
-Now we consider the different sorts of constraints:
+So which of the candidates should we pick to quantify over? It's pretty easy:
-* For ClassPred constraints:
+* Never pick a constraint that doesn't mention any of the quantified
+ variables `qtvs`. Picking such a constraint essentially moves the solving of
+ the constraint from this function definition to call sites. But because the
+ constraint mentions no quantified variables, call sites have no advantage
+ over the definition site. Well, not quite: there could be new constraints
+ brought into scope by a pattern-match against a constrained (e.g. GADT)
+ constructor. Example
- * Never pick a CallStack constraint.
- See Note [Overview of implicit CallStacks]
+ data T a where { T1 :: T1 Bool; ... }
- * Always pick an implicit-parameter constraint.
- Note [Inheriting implicit parameters]
+ f :: forall a. a -> T a -> blah
+ f x t = let g y = x&&y -- This needs a~Bool
+ in case t of
+ T1 -> g True
+ ....
- * For /top-level/ class constraints see
- Note [Do not quantify over constraints that determine a variable]
+ At g's call site we have `a~Bool`, so we /could/ infer
+ g :: forall . (a~Bool) => Bool -> Bool -- qtvs = {}
-* For EqPred constraints see Note [Quantifying over equality constraints]
+ This is all very contrived, and probably just postponse type errors to
+ the call site. If that's what you want, write a type signature.
-* For IrredPred constraints, we allow anything that mentions the quantified
- type variables.
+* Implicit parameters is an exception to the "no quantified vars"
+ rule (see Note [Inheriting implicit parameters]) so we can't actually
+ simply test this case first.
-* A ForAllPred should not appear: the candidates come from approximateWC.
+* Finally, we may need to "box" equality predicates: if we want to quantify
+ over `a ~# b`, we actually quantify over the boxed version, `a ~ b`.
+ See Note [Lift equality constraints when quantifying].
Notice that we do /not/ consult -XFlexibleContexts here. For example,
we allow `pickQuantifiablePreds` to quantify over a constraint like
@@ -1852,102 +2020,6 @@ parameters, *even if* they don't mention the bound type variables.
Reason: because implicit parameters, uniquely, have local instance
declarations. See pickQuantifiablePreds.
-Note [Quantifying over equality constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Should we quantify over an equality constraint (s ~ t)
-in pickQuantifiablePreds?
-
-* It is always /sound/ to quantify over a constraint -- those
- quantified constraints will need to be proved at each call site.
-
-* We definitely don't want to quantify over (Maybe a ~ Bool), to get
- f :: forall a. (Maybe a ~ Bool) => blah
- That simply postpones a type error from the function definition site to
- its call site. Fortunately we have already filtered out insoluble
- constraints: see `definite_error` in `simplifyInfer`.
-
-* What about (a ~ T alpha b), where we are about to quantify alpha, `a` and
- `b` are in-scope skolems, and `T` is a data type. It's pretty unlikely
- that this will be soluble at a call site, so we don't quantify over it.
-
-* What about `(F beta ~ Int)` where we are going to quantify `beta`?
- Should we quantify over the (F beta ~ Int), to get
- f :: forall b. (F b ~ Int) => blah
- Aha! Perhaps yes, because at the call site we will instantiate `b`, and
- perhaps we have `instance F Bool = Int`. So we *do* quantify over a
- type-family equality where the arguments mention the quantified variables.
-
-This is all a bit ad-hoc.
-
-Note [Do not quantify over constraints that determine a variable]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (typecheck/should_compile/tc231), where we're trying to infer
-the type of a top-level declaration. We have
- class Zork s a b | a -> b
-and the candidate constraint at the end of simplifyInfer is
- [W] Zork alpha[1] (Z [Char]) beta[1]
-We definitely want to quantify over `alpha` (which is mentioned in the
-tau-type).
-
-But we do *not* want to quantify over `beta`: it is determined by the
-functional dependency on Zork: note that the second argument to Zork
-in the Wanted is a variable-free `Z [Char]`. Quantifying over it
-would be "Henry Ford polymorphism". (Presumably we don't have an
-instance in scope that tells us what `beta` actually is.) Instead
-we promote `beta[1]` to `beta[0]`, in `decidePromotedTyVars`.
-
-The question here: do we want to quantify over the constraint, to
-give the type
- forall a. Zork a (Z [Char]) beta[0] => blah
-Definitely not. Since we're not quantifying over beta, it has been
-promoted; and then will be zapped to Any in the final zonk. So we end
-up with a (perhaps exported) type involving
- forall a. Zork a (Z [Char]) Any => blah
-No no no:
-
- Key principle: we never want to show the programmer
- a type with `Any` in it.
-
-What we really want (to catch the Zork example) is this:
-
- Quantify over the constraint only if all its free variables are
- (a) quantified, or
- (b) appears in the type of something in the environment (mono_tvs0).
-
-To understand (b) consider
-
- class C a b where { op :: a -> b -> () }
-
- mr = 3 -- mr :: alpha
- f1 x = op x mr -- f1 :: forall b. b -> (), plus [W] C b alpha
- intify = mr + (4 :: Int)
-
-In `f1` should we quantify over that `(C b alpha)`? Answer: since `alpha`
-is free in the type envt, yes we should. After all, if we'd typechecked
-`intify` first, we'd have set `alpha := Int`, and /then/ we'd certainly
-quantify. The delicate Zork situation applies when beta is completely
-unconstrained (not free in the environment) -- except by the fundep.
-
-Another way to put it: let's say `alpha` is in `mono_tvs0`. It must be that
-some variable `x` has `alpha` free in its type. If we are at top-level (and we
-are, because nested decls don't go through this path all), then `x` must also
-be at top-level. And, by induction, `x` will not have Any in its type when all
-is said and done. The induction is well-founded because, if `x` is mutually
-recursive with the definition at hand, then their constraints get processed
-together (or `x` has a type signature, in which case the type doesn't have
-`Any`). So the key thing is that we must not introduce a new top-level
-unconstrained variable here.
-
-However this regrettably-subtle reasoning is needed only for /top-level/
-declarations. For /nested/ decls we can see all the calls, so we'll
-instantiate that quantifed `Zork a (Z [Char]) beta` constraint at call sites,
-and either solve it or not (probably not). We won't be left with a
-still-callable function with Any in its type. So for nested definitions we
-don't make this tricky test.
-
-Historical note: we had a different, and more complicated test
-before, but it was utterly wrong: #23199.
-
Note [Quantification and partial signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When choosing type variables to quantify, the basic plan is to
@@ -2177,63 +2249,4 @@ whatever, because the type-class defaulting rules have yet to run.
An alternate implementation would be to emit a Wanted constraint setting
the RuntimeRep variable to LiftedRep, but this seems unnecessarily indirect.
-
-Note [Promote _and_ default when inferring]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we are inferring a type, we simplify the constraint, and then use
-approximateWC to produce a list of candidate constraints. Then we MUST
-
- a) Promote any meta-tyvars that have been floated out by
- approximateWC, to restore invariant (WantedInv) described in
- Note [TcLevel invariants] in GHC.Tc.Utils.TcType.
-
- b) Default the kind of any meta-tyvars that are not mentioned in
- in the environment.
-
-To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
-have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
-should! If we don't solve the constraint, we'll stupidly quantify over
-(C (a->Int)) and, worse, in doing so skolemiseQuantifiedTyVar will quantify over
-(b:*) instead of (a:OpenKind), which can lead to disaster; see #7332.
-#7641 is a simpler example.
-
-Note [Promoting unification variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we float an equality out of an implication we must "promote" free
-unification variables of the equality, in order to maintain Invariant
-(WantedInv) from Note [TcLevel invariants] in GHC.Tc.Types.TcType.
-
-This is absolutely necessary. Consider the following example. We start
-with two implications and a class with a functional dependency.
-
- class C x y | x -> y
- instance C [a] [a]
-
- (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
- (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
-
-We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
-They may react to yield that (beta := [alpha]) which can then be pushed inwards
-the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
-(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
-beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
-
- class C x y | x -> y where
- op :: x -> y -> ()
-
- instance C [a] [a]
-
- type family F a :: *
-
- h :: F Int -> ()
- h = undefined
-
- data TEx where
- TEx :: a -> TEx
-
- f (x::beta) =
- let g1 :: forall b. b -> ()
- g1 _ = h [x]
- g2 z = case z of TEx y -> (h [[undefined]], op x [y])
- in (g1 '3', g2 undefined)
-}
=====================================
compiler/GHC/Tc/Solver/Default.hs
=====================================
@@ -818,7 +818,11 @@ findDefaultableGroups (default_tys, extended_defaults) wanteds
, defaultable_tyvar tv
, defaultable_classes (map (classTyCon . sndOf3) group) ]
where
- simples = approximateWC True wanteds
+ simples = approximateWC True wanteds
+ -- True: for the purpose of defaulting we don't care
+ -- about shape or enclosing equalities
+ -- See (W3) in Note [ApproximateWC] in GHC.Tc.Types.Constraint
+
(unaries, non_unaries) = partitionWith find_unary (bagToList simples)
unary_groups = equivClasses cmp_tv unaries
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -73,9 +73,6 @@ simplifyWantedsTcM wanted
solveWanteds :: WantedConstraints -> TcS WantedConstraints
solveWanteds wc@(WC { wc_errors = errs })
- | isEmptyWC wc -- Fast path
- = return wc
- | otherwise
= do { cur_lvl <- TcS.getTcLevel
; traceTcS "solveWanteds {" $
vcat [ text "Level =" <+> ppr cur_lvl
@@ -106,6 +103,9 @@ simplify_loop :: Int -> IntWithInf -> Bool
-- else, so we do them once, at the end in solveWanteds
simplify_loop n limit definitely_redo_implications
wc@(WC { wc_simple = simples, wc_impl = implics })
+ | isSolvedWC wc -- Fast path
+ = return wc
+ | otherwise
= do { csTraceTcS $
text "simplify_loop iteration=" <> int n
<+> (parens $ hsep [ text "definitely_redo =" <+> ppr definitely_redo_implications <> comma
@@ -145,7 +145,7 @@ maybe_simplify_again n limit unif_happened wc@(WC { wc_simple = simples })
| unif_happened
= simplify_loop n limit True wc
- | superClassesMightHelp wc
+ | superClassesMightHelp wc -- Returns False quickly if wc is solved
= -- We still have unsolved goals, and apparently no way to solve them,
-- so try expanding superclasses at this level, both Given and Wanted
do { pending_given <- getPendingGivenScs
=====================================
compiler/GHC/Tc/TyCl/PatSyn.hs
=====================================
@@ -154,7 +154,7 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
; ((univ_tvs, req_dicts, ev_binds, _), residual)
<- captureConstraints $
- simplifyInfer tclvl NoRestrictions [] named_taus wanted
+ simplifyInfer TopLevel tclvl NoRestrictions [] named_taus wanted
; top_ev_binds <- checkNoErrs (simplifyTop residual)
; addTopEvBinds top_ev_binds $
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -61,7 +61,7 @@ module GHC.Tc.Types.Constraint (
tyCoVarsOfWC, tyCoVarsOfWCList,
insolubleWantedCt, insolubleCt, insolubleIrredCt,
insolubleImplic, nonDefaultableTyVarsOfWC,
- approximateWC,
+ approximateWCX, approximateWC,
Implication(..), implicationPrototype, checkTelescopeSkol,
ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
@@ -1815,60 +1815,121 @@ At the end, we will hopefully have substituted uf1 := F alpha, and we
will be able to report a more informative error:
'Can't construct the infinite type beta ~ F alpha beta'
+
************************************************************************
* *
- Invariant checking (debug only)
+ approximateWC
* *
************************************************************************
-}
-approximateWC :: Bool -- See Wrinkle (W3) in Note [ApproximateWC]
- -> WantedConstraints
- -> Cts
--- Second return value is the depleted wc
--- Postcondition: Wanted Cts
+type ApproxWC = ( Bag Ct -- Free quantifiable constraints
+ , Bag Ct ) -- Free non-quantifiable constraints
+ -- due to shape, or enclosing equality
+
+approximateWC :: Bool -> WantedConstraints -> Bag Ct
+approximateWC include_non_quantifiable cts
+ | include_non_quantifiable = quant `unionBags` no_quant
+ | otherwise = quant
+ where
+ (quant, no_quant) = approximateWCX cts
+
+approximateWCX :: WantedConstraints -> ApproxWC
+-- The "X" means "extended";
+-- we return both quantifiable and non-quantifiable constraints
-- See Note [ApproximateWC]
-- See Note [floatKindEqualities vs approximateWC]
-approximateWC float_past_equalities wc
- = float_wc False emptyVarSet wc
+approximateWCX wc
+ = float_wc False emptyVarSet wc (emptyBag, emptyBag)
where
float_wc :: Bool -- True <=> there are enclosing equalities
-> TcTyCoVarSet -- Enclosing skolem binders
- -> WantedConstraints -> Cts
- float_wc encl_eqs trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
- = filterBag (is_floatable encl_eqs trapping_tvs) simples `unionBags`
- concatMapBag (float_implic encl_eqs trapping_tvs) implics
-
- float_implic :: Bool -> TcTyCoVarSet -> Implication -> Cts
+ -> WantedConstraints
+ -> ApproxWC -> ApproxWC
+ float_wc encl_eqs trapping_tvs (WC { wc_simple = simples, wc_impl = implics }) acc
+ = foldBag_flip (float_ct encl_eqs trapping_tvs) simples $
+ foldBag_flip (float_implic encl_eqs trapping_tvs) implics $
+ acc
+
+ float_implic :: Bool -> TcTyCoVarSet -> Implication
+ -> ApproxWC -> ApproxWC
float_implic encl_eqs trapping_tvs imp
= float_wc new_encl_eqs new_trapping_tvs (ic_wanted imp)
where
new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
new_encl_eqs = encl_eqs || ic_given_eqs imp == MaybeGivenEqs
- is_floatable encl_eqs skol_tvs ct
- | isGivenCt ct = False
- | insolubleCt ct = False
- | tyCoVarsOfCt ct `intersectsVarSet` skol_tvs = False
+ float_ct :: Bool -> TcTyCoVarSet -> Ct
+ -> ApproxWC -> ApproxWC
+ float_ct encl_eqs skol_tvs ct acc@(quant, no_quant)
+ | isGivenCt ct = acc
+ -- There can be (insoluble) Given constraints in wc_simple,
+ -- there so that we get error reports for unreachable code
+ -- See `given_insols` in GHC.Tc.Solver.Solve.solveImplication
+ | insolubleCt ct = acc
+ | tyCoVarsOfCt ct `intersectsVarSet` skol_tvs = acc
| otherwise
= case classifyPredType (ctPred ct) of
- EqPred {} -> float_past_equalities || not encl_eqs
- -- See Wrinkle (W1)
- ClassPred {} -> True -- See Wrinkle (W2)
- IrredPred {} -> True -- ..both in Note [ApproximateWC]
- ForAllPred {} -> False
+ -- See the classification in Note [ApproximateWC]
+ EqPred eq_rel ty1 ty2
+ | not encl_eqs -- See Wrinkle (W1)
+ , quantify_equality eq_rel ty1 ty2
+ -> add_to_quant
+ | otherwise
+ -> add_to_no_quant
+
+ ClassPred cls tys
+ | Just {} <- isCallStackPred cls tys
+ -- NEVER infer a CallStack constraint. Otherwise we let
+ -- the constraints bubble up to be solved from the outer
+ -- context, or be defaulted when we reach the top-level.
+ -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
+ -> add_to_no_quant
+
+ | otherwise
+ -> add_to_quant -- See Wrinkle (W2)
+
+ IrredPred {} -> add_to_quant -- See Wrinkle (W2)
+
+ ForAllPred {} -> add_to_no_quant -- Never quantify these
+ where
+ add_to_quant = (ct `consBag` quant, no_quant)
+ add_to_no_quant = (quant, ct `consBag` no_quant)
+
+ -- See Note [Quantifying over equality constraints]
+ quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2
+ quantify_equality ReprEq _ _ = True
+
+ quant_fun ty
+ = case tcSplitTyConApp_maybe ty of
+ Just (tc, _) -> isTypeFamilyTyCon tc
+ _ -> False
{- Note [ApproximateWC]
~~~~~~~~~~~~~~~~~~~~~~~
approximateWC takes a constraint, typically arising from the RHS of a
-let-binding whose type we are *inferring*, and extracts from it some
-*simple* constraints that we might plausibly abstract over. Of course
-the top-level simple constraints are plausible, but we also float constraints
-out from inside, if they are not captured by skolems.
+let-binding whose type we are *inferring*, and extracts from it some *simple*
+constraints that we might plausibly abstract over. Of course the top-level
+simple constraints are plausible, but we also float constraints out from inside,
+if they are not captured by skolems.
The same function is used when doing type-class defaulting (see the call
to applyDefaultingRules) to extract constraints that might be defaulted.
+We proceed by classifying the constraint:
+ * ClassPred:
+ * Never pick a CallStack constraint.
+ See Note [Overview of implicit CallStacks]
+ * Always pick an implicit-parameter constraint.
+ Note [Inheriting implicit parameters]
+ See wrinkle (W2)
+
+ * EqPred: see Note [Quantifying over equality constraints]
+
+ * IrredPred: we allow anything.
+
+ * ForAllPred: never quantify over these
+
Wrinkle (W1)
When inferring most-general types (in simplifyInfer), we
do *not* float an equality constraint if the implication binds
@@ -1884,22 +1945,19 @@ Wrinkle (W1)
non-principal types.)
Wrinkle (W2)
- We do allow /class/ constraints to float, even if
- the implication binds equalities. This is a subtle point: see #23224.
- In principle, a class constraint might ultimately be satisfiable from
- a constraint bound by an implication (see #19106 for an example of this
- kind), but it's extremely obscure and I was unable to construct a
- concrete example. In any case, in super-subtle cases where this might
- make a difference, you would be much better advised to simply write a
- type signature.
-
- I included IrredPred here too, for good measure. In general,
- abstracting over more constraints does no harm.
+ We do allow /class/ constraints to float, even if the implication binds
+ equalities. This is a subtle point: see #23224. In principle, a class
+ constraint might ultimately be satisfiable from a constraint bound by an
+ implication (see #19106 for an example of this kind), but it's extremely
+ obscure and I was unable to construct a concrete example. In any case, in
+ super-subtle cases where this might make a difference, you would be much
+ better advised to simply write a type signature.
Wrinkle (W3)
- In findDefaultableGroups we are not worried about the
- most-general type; and we /do/ want to float out of equalities
- (#12797). Hence the boolean flag to approximateWC.
+ In findDefaultableGroups we are not worried about the most-general type; and
+ we /do/ want to float out of equalities (#12797). Hence we just union the two
+ returned lists.
+
------ Historical note -----------
There used to be a second caveat, driven by #8155
@@ -1926,6 +1984,33 @@ you want. So I simply removed the extra code to implement the
contamination stuff. There was zero effect on the testsuite (not even #8155).
------ End of historical note -----------
+Note [Quantifying over equality constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Should we quantify over an equality constraint (s ~ t)
+in pickQuantifiablePreds?
+
+* It is always /sound/ to quantify over a constraint -- those
+ quantified constraints will need to be proved at each call site.
+
+* We definitely don't want to quantify over (Maybe a ~ Bool), to get
+ f :: forall a. (Maybe a ~ Bool) => blah
+ That simply postpones a type error from the function definition site to
+ its call site. Fortunately we have already filtered out insoluble
+ constraints: see `definite_error` in `simplifyInfer`.
+
+* What about (a ~ T alpha b), where we are about to quantify alpha, `a` and
+ `b` are in-scope skolems, and `T` is a data type. It's pretty unlikely
+ that this will be soluble at a call site, so we don't quantify over it.
+
+* What about `(F beta ~ Int)` where we are going to quantify `beta`?
+ Should we quantify over the (F beta ~ Int), to get
+ f :: forall b. (F b ~ Int) => blah
+ Aha! Perhaps yes, because at the call site we will instantiate `b`, and
+ perhaps we have `instance F Bool = Int`. So we *do* quantify over a
+ type-family equality where the arguments mention the quantified variables.
+
+This is all a bit ad-hoc.
+
************************************************************************
* *
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -78,9 +78,8 @@ module GHC.Tc.Utils.TcMType (
---------------------------------
-- Promotion, defaulting, skolemisation
defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet,
- quantifyTyVars, isQuantifiableTv,
+ quantifyTyVars, doNotQuantifyTyVars,
zonkAndSkolemise, skolemiseQuantifiedTyVar,
- doNotQuantifyTyVars,
candidateQTyVarsOfType, candidateQTyVarsOfKind,
candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
@@ -1788,15 +1787,6 @@ quantifyTyVars skol_info ns_strat dvs
| otherwise
= Just <$> skolemiseQuantifiedTyVar skol_info tkv
-isQuantifiableTv :: TcLevel -- Level of the context, outside the quantification
- -> TcTyVar
- -> Bool
-isQuantifiableTv outer_tclvl tcv
- | isTcTyVar tcv -- Might be a CoVar; change this when gather covars separately
- = tcTyVarLevel tcv `strictlyDeeperThan` outer_tclvl
- | otherwise
- = False
-
zonkAndSkolemise :: SkolemInfo -> TcTyCoVar -> ZonkM TcTyCoVar
-- A tyvar binder is never a unification variable (TauTv),
-- rather it is always a skolem. It *might* be a TyVarTv.
@@ -2414,7 +2404,7 @@ promoteMetaTyVarTo :: HasDebugCallStack => TcLevel -> TcTyVar -> TcM Bool
-- invariant (WantedInv) in Note [TcLevel invariants] 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]
+-- See Note [Promote monomorphic tyvars] in GHC.Tc.Solver
promoteMetaTyVarTo tclvl tv
| assertPpr (isMetaTyVar tv) (ppr tv) $
tcTyVarLevel tv `strictlyDeeperThan` tclvl
=====================================
testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr
=====================================
@@ -1,12 +1,12 @@
ExtraTcsUntch.hs:23:18: error: [GHC-83865]
• Couldn't match expected type: F Int
- with actual type: [[a0]]
+ with actual type: [p0]
• In the first argument of ‘h’, namely ‘[x]’
In the expression: h [x]
In an equation for ‘g1’: g1 _ = h [x]
• Relevant bindings include
- x :: [a0] (bound at ExtraTcsUntch.hs:21:3)
- f :: [a0] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
+ x :: p0 (bound at ExtraTcsUntch.hs:21:3)
+ f :: p0 -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
ExtraTcsUntch.hs:25:38: error: [GHC-83865]
• Couldn't match expected type: F Int
@@ -14,7 +14,4 @@ ExtraTcsUntch.hs:25:38: error: [GHC-83865]
• In the first argument of ‘h’, namely ‘[[undefined]]’
In the expression: h [[undefined]]
In the expression: (h [[undefined]], op x [y])
- • Relevant bindings include
- x :: [a0] (bound at ExtraTcsUntch.hs:21:3)
- f :: [a0] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1)
=====================================
testsuite/tests/partial-sigs/should_fail/T10615.stderr
=====================================
@@ -1,34 +1,39 @@
T10615.hs:5:7: error: [GHC-88464]
- • Found type wildcard ‘_’ standing for ‘w1’
- Where: ‘w1’ is an ambiguous type variable
+ • Found type wildcard ‘_’ standing for ‘w’
+ Where: ‘w’ is a rigid type variable bound by
+ the inferred type of f1 :: w -> f
+ at T10615.hs:6:1-10
To use the inferred type, enable PartialTypeSignatures
• In the type signature: f1 :: _ -> f
T10615.hs:6:6: error: [GHC-25897]
- • Couldn't match type ‘f’ with ‘b1 -> w1’
- Expected: w1 -> f
- Actual: w1 -> b1 -> w1
+ • Couldn't match type ‘f’ with ‘b1 -> w’
+ Expected: w -> f
+ Actual: w -> b1 -> w
‘f’ is a rigid type variable bound by
- the inferred type of f1 :: w1 -> f
+ the inferred type of f1 :: w -> f
at T10615.hs:5:1-12
• In the expression: const
In an equation for ‘f1’: f1 = const
- • Relevant bindings include f1 :: w1 -> f (bound at T10615.hs:6:1)
+ • Relevant bindings include f1 :: w -> f (bound at T10615.hs:6:1)
T10615.hs:8:7: error: [GHC-88464]
- • Found type wildcard ‘_’ standing for ‘w0’
- Where: ‘w0’ is an ambiguous type variable
+ • Found type wildcard ‘_’ standing for ‘w’
+ Where: ‘w’ is a rigid type variable bound by
+ the inferred type of f2 :: w -> _f
+ at T10615.hs:9:1-10
To use the inferred type, enable PartialTypeSignatures
• In the type signature: f2 :: _ -> _f
T10615.hs:9:6: error: [GHC-25897]
- • Couldn't match type ‘_f’ with ‘b0 -> w0’
- Expected: w0 -> _f
- Actual: w0 -> b0 -> w0
+ • Couldn't match type ‘_f’ with ‘b0 -> w’
+ Expected: w -> _f
+ Actual: w -> b0 -> w
‘_f’ is a rigid type variable bound by
- the inferred type of f2 :: w0 -> _f
+ the inferred type of f2 :: w -> _f
at T10615.hs:8:1-13
• In the expression: const
In an equation for ‘f2’: f2 = const
- • Relevant bindings include f2 :: w0 -> _f (bound at T10615.hs:9:1)
+ • Relevant bindings include f2 :: w -> _f (bound at T10615.hs:9:1)
+
=====================================
testsuite/tests/polykinds/T14172.stderr
=====================================
@@ -1,7 +1,9 @@
T14172.hs:7:46: error: [GHC-88464]
- • Found type wildcard ‘_’ standing for ‘a'1 :: k0’
- Where: ‘k0’ is an ambiguous type variable
- ‘a'1’ is an ambiguous type variable
+ • Found type wildcard ‘_’ standing for ‘a'’
+ Where: ‘a'’ is a rigid type variable bound by
+ the inferred type of
+ traverseCompose :: (a -> f b) -> g a -> f (h a')
+ at T14172.hs:8:1-46
To use the inferred type, enable PartialTypeSignatures
• In the first argument of ‘h’, namely ‘_’
In the first argument of ‘f’, namely ‘(h _)’
@@ -10,19 +12,18 @@ T14172.hs:7:46: error: [GHC-88464]
T14172.hs:8:19: error: [GHC-25897]
• Couldn't match type ‘a’ with ‘g'1 a'0’
- Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a'1)
- Actual: (Unwrapped (Compose f'0 g'1 a'0)
- -> f (Unwrapped (h a'1)))
- -> Compose f'0 g'1 a'0 -> f (h a'1)
+ Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a')
+ Actual: (Unwrapped (Compose f'0 g'1 a'0) -> f (Unwrapped (h a')))
+ -> Compose f'0 g'1 a'0 -> f (h a')
‘a’ is a rigid type variable bound by
the inferred type of
- traverseCompose :: (a -> f b) -> g a -> f (h a'1)
+ traverseCompose :: (a -> f b) -> g a -> f (h a')
at T14172.hs:7:1-47
• In the first argument of ‘(.)’, namely ‘_Wrapping Compose’
In the expression: _Wrapping Compose . traverse
In an equation for ‘traverseCompose’:
traverseCompose = _Wrapping Compose . traverse
• Relevant bindings include
- traverseCompose :: (a -> f b) -> g a -> f (h a'1)
+ traverseCompose :: (a -> f b) -> g a -> f (h a')
(bound at T14172.hs:8:1)
=====================================
testsuite/tests/typecheck/should_compile/T13785.hs
=====================================
@@ -2,15 +2,20 @@
{-# OPTIONS_GHC -Wmonomorphism-restriction #-}
module Bug where
-class Monad m => C m where
- c :: (m Char, m Char)
+class Monad x => C x where
+ c :: (x Char, x Char)
foo :: forall m. C m => m Char
-foo = bar >> baz >> bar2
+foo = bar >> baz >> bar1 >> bar2
where
-- Should not get MR warning
bar, baz :: m Char
(bar, baz) = c
+ -- Should not get MR warning
+ (bar1, baz1) = c :: (m Char, m Char)
+
-- Should get MR warning
+ -- Natural type for the "whole binding": forall x. C x => (x Char, x Char)
+ -- MR makes it less polymorphic => warning.
(bar2, baz2) = c
=====================================
testsuite/tests/typecheck/should_compile/T13785.stderr
=====================================
@@ -1,12 +1,13 @@
-
-T13785.hs:16:5: warning: [GHC-55524] [-Wmonomorphism-restriction]
+T13785.hs:21:5: warning: [GHC-55524] [-Wmonomorphism-restriction]
• The Monomorphism Restriction applies to the bindings
for ‘bar2’, ‘baz2’
• In an equation for ‘foo’:
foo
- = bar >> baz >> bar2
+ = bar >> baz >> bar1 >> bar2
where
bar, baz :: m Char
(bar, baz) = c
+ (bar1, baz1) = c :: (m Char, m Char)
(bar2, baz2) = c
Suggested fix: Consider giving ‘baz2’ and ‘bar2’ a type signature
+
=====================================
testsuite/tests/typecheck/should_compile/T25266.hs
=====================================
@@ -0,0 +1,127 @@
+{-# OPTIONS_GHC -Wno-missing-methods #-}
+{-# LANGUAGE GHC2021 #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE ImplicitPrelude #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module GHC25266 where
+
+import Control.Monad.IO.Class (MonadIO (liftIO))
+import Control.Monad.Trans.Class (MonadTrans (lift))
+import Control.Monad.Trans.Reader (ReaderT, mapReaderT, runReaderT)
+import Data.Kind (Type)
+import Data.Void (Void)
+import GHC.Stack (HasCallStack, withFrozenCallStack)
+
+class MonadIO m => CanRunDB m where
+ unsafeUnlabelledRunDB :: HasCallStack => SqlPersistT m a -> m a
+
+type DBImpl backend env = ReaderT env (ReaderT backend IO)
+
+newtype DBWith backend env a = DB (DBImpl backend env a)
+ deriving newtype (Functor, Applicative, Monad)
+
+type DBEnv = ()
+
+type DB = DBWith SqlBackend DBEnv
+
+class Monad m => PersistentOperation m where
+ type PersistentBackend m
+ unsafeLiftPersistentOperation :: HasCallStack => ReaderT (PersistentBackend m) IO a -> m a
+
+instance PersistentOperation (DBWith backend env) where
+ type PersistentBackend (DBWith backend env) = backend
+ unsafeLiftPersistentOperation = DB . lift . checkpointCallStack
+
+toSqlPersistTIO :: env -> DBWith backend env a -> ReaderT backend IO a
+toSqlPersistTIO env (DB act) = runReaderT act env
+
+hoistIO :: MonadIO m => ReaderT backend IO a -> ReaderT backend m a
+hoistIO = mapReaderT liftIO
+
+liftToSqlPersistT :: forall m a backend. (CanRunDB m) => DBWith backend DBEnv a -> ReaderT backend m a
+liftToSqlPersistT action = do
+ let dbEnv = ()
+ hoistIO $ toSqlPersistTIO dbEnv action
+
+runDB :: (HasCallStack, CanRunDB m) => DB a -> m a
+runDB action = withFrozenCallStack unsafeUnlabelledRunDB $ liftToSqlPersistT action
+
+streamRows ::
+ forall m a.
+ (MonadUnliftIO m, CanRunDB m) =>
+ (forall n. (PersistentOperation n, PersistentBackend n ~ SqlBackend) => n [a]) ->
+ ConduitT () [a] m ()
+streamRows runQuery = go (10 :: Integer)
+ where
+ go n
+ | n < 0 = pure ()
+ | otherwise = do
+ rows <- lift . runDB $ runQuery
+ yield rows
+ go (n - 1)
+
+expectedList :: [Int]
+expectedList = [1, 2, 3]
+
+query :: forall n. (PersistentOperation n, PersistentBackend n ~ SqlBackend) => n [Int]
+query = pure expectedList
+
+test_success :: forall m. (MonadUnliftIO m, CanRunDB m) => m [[Int]]
+test_success = do
+ let conduit = streamRows query .| (sinkList @_ @[Int])
+ runConduit conduit
+
+test_fail :: forall m. (MonadUnliftIO m, CanRunDB m) => m [[Int]]
+test_fail = do
+ let conduit = streamRows query .| sinkList
+ runConduit conduit
+
+-----
+-- annotated-exception
+-----
+
+checkpointCallStack
+ -- :: (MonadCatch m, HasCallStack)
+ :: (Monad m, HasCallStack)
+ => m a
+ -> m a
+checkpointCallStack = id
+
+-----
+-- conduit
+-----
+
+data ConduitT i o (m :: Type -> Type) r
+instance Functor (ConduitT i o m)
+instance Applicative (ConduitT i o m)
+instance Monad (ConduitT i o m)
+instance MonadTrans (ConduitT i o)
+
+(.|) :: Monad m => ConduitT a b m () -> ConduitT b c m r -> ConduitT a c m r
+(.|) = undefined
+
+runConduit :: Monad m => ConduitT () Void m r -> m r
+runConduit = undefined
+
+sinkList :: Monad m => ConduitT a o m [a]
+sinkList = undefined
+
+yield :: Monad m => o -> ConduitT i o m ()
+yield = undefined
+
+-----
+-- persistent
+-----
+
+data SqlBackend
+
+type SqlPersistT = ReaderT SqlBackend
+
+-----
+-- unliftio
+-----
+
+class MonadIO m => MonadUnliftIO m where
+ withRunInIO :: ((forall a. m a -> IO a) -> IO b) -> m b
=====================================
testsuite/tests/typecheck/should_compile/T25266a.hs
=====================================
@@ -0,0 +1,13 @@
+{-# LANGUAGE GADTs #-}
+
+module T25266a where
+
+data T a where { T1 :: T Int; T2 :: a -> T a }
+
+-- Rejected, becuase there is no principal type,
+-- and the function is top level
+f x y t = (case t of
+ T1 -> length [x,y]
+ T2 _ -> 2) :: Int
+
+
=====================================
testsuite/tests/typecheck/should_compile/T25266a.stderr
=====================================
@@ -0,0 +1,21 @@
+T25266a.hs:10:41: error: [GHC-25897]
+ • Could not deduce ‘p1 ~ p2’
+ from the context: a ~ Int
+ bound by a pattern with constructor: T1 :: T Int,
+ in a case alternative
+ at T25266a.hs:10:23-24
+ ‘p1’ is a rigid type variable bound by
+ the inferred type of f :: p1 -> p2 -> T a -> Int
+ at T25266a.hs:(9,1)-(11,40)
+ ‘p2’ is a rigid type variable bound by
+ the inferred type of f :: p1 -> p2 -> T a -> Int
+ at T25266a.hs:(9,1)-(11,40)
+ • In the expression: y
+ In the first argument of ‘length’, namely ‘[x, y]’
+ In the expression: length [x, y]
+ • Relevant bindings include
+ y :: p2 (bound at T25266a.hs:9:5)
+ x :: p1 (bound at T25266a.hs:9:3)
+ f :: p1 -> p2 -> T a -> Int (bound at T25266a.hs:9:1)
+ Suggested fix: Consider giving ‘f’ a type signature
+
=====================================
testsuite/tests/typecheck/should_compile/T25266b.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE GADTs #-}
+
+module T25266b where
+
+data T a where { T1 :: T Int; T2 :: a -> T a }
+
+h :: Int -> (Int,Int)
+-- Binding for `f` is accepted; we do not generalise it
+-- f :: forall a. alpha -> beta -> T a -> Int
+-- We figure out alpha/beta from the call sites
+h p = let f x y t = (case t of
+ T1 -> length [x,y]
+ T2 _ -> 2) :: Int
+ in (f p (4::Int) (T2 'c'), f 4 5 (T2 "oooh"))
+
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -934,4 +934,7 @@ test('T25125', normal, compile, [''])
test('T24845a', normal, compile, [''])
test('T23501a', normal, compile, [''])
test('T23501b', normal, compile, [''])
+test('T25266', normal, compile, [''])
+test('T25266a', normal, compile_fail, [''])
+test('T25266b', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T18398.stderr
=====================================
@@ -6,7 +6,7 @@ T18398.hs:13:34: error: [GHC-39999]
In the expression: case x of MkEx _ -> meth x y
T18398.hs:13:70: error: [GHC-39999]
- • No instance for ‘C Ex t0’ arising from a use of ‘meth’
+ • No instance for ‘C Ex t1’ arising from a use of ‘meth’
• In the expression: meth x z
In a case alternative: MkEx _ -> meth x z
In the expression: case x of MkEx _ -> meth x z
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c2694cb71a1b9e2e193040fd1951f01477bfbc5a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c2694cb71a1b9e2e193040fd1951f01477bfbc5a
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20241018/a76d0ab7/attachment-0001.html>
More information about the ghc-commits
mailing list