[Git][ghc/ghc][wip/T22194-flags] 2 commits: Improve partial signatures
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Apr 7 21:30:05 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC
Commits:
65fd65ab by Simon Peyton Jones at 2023-04-07T22:28:57+01:00
Improve partial signatures
This MR fixes #23223. The changes are in two places:
* GHC.Tc.Bind.checkMonomorphismRestriction
See the new `Note [When the MR applies]`
We now no longer stupidly attempt to apply the MR when the user
specifies a context, e.g. f :: Eq a => _ -> _
* GHC.Tc.Solver.decideQuantification
See rewritten `Note [Constraints in partial type signatures]`
Fixing this bug apparently breaks three tests:
* partial-sigs/should_compile/T11192
* partial-sigs/should_fail/Defaulting1MROff
* partial-sigs/should_fail/T11122
However they are all symptoms of #23232, so I'm marking them as
expect_broken(23232).
I feel happy about this MR. Nice.
- - - - -
7d6284da by Simon Peyton Jones at 2023-04-07T22:29:24+01:00
Make approximateWC a bit cleverer
This MR fixes #23224: making approximateWC more clever
See the long `Note [ApproximateWC]` in GHC.Tc.Solver
All this is delicate and ad-hoc -- but it /has/ to be: we are
talking about inferring a type for a binding in the presence of
GADTs, type families and whatnot: known difficult territory.
We just try as hard as we can.
- - - - -
10 changed files:
- compiler/GHC/Tc/Gen/Bind.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Types/Origin.hs
- testsuite/tests/partial-sigs/should_compile/T10403.stderr
- testsuite/tests/partial-sigs/should_compile/T19106.hs
- testsuite/tests/partial-sigs/should_compile/all.T
- + testsuite/tests/partial-sigs/should_fail/T23223.hs
- + testsuite/tests/partial-sigs/should_fail/T23223.stderr
- testsuite/tests/partial-sigs/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/Bind.hs
=====================================
@@ -751,57 +751,102 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
checkMonomorphismRestriction :: [MonoBindInfo] -> [LHsBind GhcRn] -> TcM Bool
-- True <=> apply the MR
+-- See Note [When the MR applies]
checkMonomorphismRestriction mbis lbinds
- | null partial_sigs -- The normal case
= do { mr_on <- xoptM LangExt.MonomorphismRestriction
; let mr_applies = mr_on && any (restricted . unLoc) lbinds
- ; when mr_applies $ mapM_ checkOverloadedSig sigs
+ ; when mr_applies $ mapM_ checkOverloadedSig mbis
; return mr_applies }
-
- | otherwise -- See Note [Partial type signatures and the monomorphism restriction]
- = return (all is_mono_psig partial_sigs)
-
where
- sigs, partial_sigs :: [TcIdSigInst]
- sigs = [sig | MBI { mbi_sig = Just sig } <- mbis]
- partial_sigs = [sig | sig@(TISI { sig_inst_sig = PartialSig {} }) <- sigs]
-
- complete_sig_bndrs :: NameSet
- complete_sig_bndrs
- = mkNameSet [ idName bndr
- | TISI { sig_inst_sig = CompleteSig { sig_bndr = bndr }} <- sigs ]
-
- is_mono_psig (TISI { sig_inst_theta = theta, sig_inst_wcx = mb_extra_constraints })
- = null theta && isNothing mb_extra_constraints
+ no_mr_bndrs :: NameSet
+ no_mr_bndrs = mkNameSet (mapMaybe no_mr_name mbis)
+
+ no_mr_name :: MonoBindInfo -> Maybe Name
+ -- Just n for binders that have a signature that says "no MR needed for me"
+ no_mr_name (MBI { mbi_sig = Just sig })
+ | TISI { sig_inst_sig = info, sig_inst_theta = theta, sig_inst_wcx = wcx } <- sig
+ = case info of
+ CompleteSig { sig_bndr = bndr } -> Just (idName bndr)
+ PartialSig { psig_name = nm }
+ | null theta, isNothing wcx -> Nothing -- f :: _ -> _
+ | otherwise -> Just nm -- f :: Num a => a -> _
+ -- For the latter case, we don't want the MR:
+ -- the user has explicitly specified a type-class context
+ no_mr_name _ = Nothing
-- The Haskell 98 monomorphism restriction
restricted (PatBind {}) = True
- restricted (VarBind { var_id = v }) = no_sig v
+ restricted (VarBind { var_id = v }) = mr_needed_for v
restricted (FunBind { fun_id = v, fun_matches = m }) = restricted_match m
- && no_sig (unLoc v)
+ && mr_needed_for (unLoc v)
restricted b = pprPanic "isRestrictedGroup/unrestricted" (ppr b)
restricted_match mg = matchGroupArity mg == 0
-- No args => like a pattern binding
-- Some args => a function binding
- no_sig nm = not (nm `elemNameSet` complete_sig_bndrs)
+ mr_needed_for nm = not (nm `elemNameSet` no_mr_bndrs)
-checkOverloadedSig :: TcIdSigInst -> TcM ()
+checkOverloadedSig :: MonoBindInfo -> TcM ()
-- Example:
-- f :: Eq a => a -> a
-- K f = e
-- The MR applies, but the signature is overloaded, and it's
-- best to complain about this directly
-- c.f #11339
-checkOverloadedSig sig
- | not (null (sig_inst_theta sig))
- , let orig_sig = sig_inst_sig sig
+checkOverloadedSig (MBI { mbi_sig = mb_sig })
+ | Just (TISI { sig_inst_sig = orig_sig, sig_inst_theta = theta, sig_inst_wcx = wcx }) <- mb_sig
+ , not (null theta && isNothing wcx)
= setSrcSpan (sig_loc orig_sig) $
failWith $ TcRnOverloadedSig orig_sig
| otherwise
= return ()
+{- Note [When the MR applies]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The Monomorphism Restriction (MR) applies as specifies in the Haskell Report:
+
+* If -XMonomorphismRestriction is on, and
+* Any binding is restricted
+
+A binding is restricted if:
+* It is a pattern binding e.g. (x,y) = e
+* Or it is a FunBind with no arguments e.g. f = rhs
+ and the binder `f` lacks a No-MR signature
+
+A binder f has a No-MR signature if
+
+* It has a complete type signature
+ e.g. f :: Num a => a -> a
+
+* Or it has a /partial/ type signature with a /context/
+ e.g. f :: (_) => a -> _
+ g :: Num a => a -> _
+ h :: (Num a, _) => a -> _
+ All of f,g,h have a No-MR signature. They say that the function is overloaded
+ so it's silly to try to apply the MR. This means that #20076 and #19106 work out
+ fine. Ditto #11016, which looked like
+ f4 :: (?loc :: Int) => _
+ f4 = ?loc
+
+ This partial-signature stuff is a bit ad-hoc but seems to match our
+ use-cases. See also Note [Constraints in partial type signatures]
+ in GHC.Tc.Solver.
+
+Example: the MR does apply to
+ k :: _ -> _
+ k = rhs
+because k's binding has no arguments, and `k` does not have
+a No-MR signature.
+
+All of this checking takes place after synonym expansion. For example:
+ type Wombat a = forall b. Eq [b] => ...b...a...
+ f5 :: Wombat _
+This (and does) behave just like
+ f5 :: forall b. Eq [b] => ...b..._...
+
+-}
+
--------------
mkExport :: TcPragEnv
-> WantedConstraints -- residual constraints, already emitted (for errors only)
@@ -850,15 +895,9 @@ mkExport prag_fn residual insoluble qtvs theta
then return idHsWrapper -- Fast path; also avoids complaint when we infer
-- an ambiguous type and have AllowAmbiguousType
-- e..g infer x :: forall a. F a -> Int
- else tcSubTypeSigma GhcBug20076
+ else tcSubTypeSigma (Shouldn'tHappenOrigin "mkExport")
sig_ctxt sel_poly_ty poly_ty
- -- as Note [Impedance matching] explains, this should never fail,
- -- and thus we'll never see an error message. It *may* do
- -- instantiation, but no message will ever be printed to the
- -- user, and so we use Shouldn'tHappenOrigin.
- -- Actually, there is a bug here: #20076. So we tell the user
- -- that they hit the bug. Once #20076 is fixed, change this
- -- back to Shouldn'tHappenOrigin.
+ -- See Note [Impedance matching]
; localSigWarn poly_id mb_sig
@@ -1102,33 +1141,6 @@ It might be possible to fix these difficulties somehow, but there
doesn't seem much point. Indeed, adding a partial type signature is a
way to get per-binding inferred generalisation.
-Note [Partial type signatures and the monomorphism restriction]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We apply the MR if /none/ of the partial signatures has a context. e.g.
- f :: _ -> Int
- f x = rhs
-The partial type signature says, in effect, "there is no context", which
-amounts to appplying the MR. Indeed, saying
- f :: _
- f = rhs
-is a way for forcing the MR to apply.
-
-But we /don't/ want to apply the MR if the partial signatures do have
-a context e.g. (#11016):
- f2 :: (?loc :: Int) => _
- f2 = ?loc
-It's stupid to apply the MR here. This test includes an extra-constraints
-wildcard; that is, we don't apply the MR if you write
- f3 :: _ => blah
-
-But watch out. We don't want to apply the MR to
- type Wombat a = forall b. Eq b => ...b...a...
- f4 :: Wombat _
-Here f4 doesn't /look/ as if it has top-level overloading, but in fact it
-does, hidden under Wombat. We can't "see" that because we only have access
-to the HsType at the moment. That's why we do the check in
-checkMonomorphismRestriction.
-
Note [Quantified variables in partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
@@ -1206,7 +1218,6 @@ considered:
more indirect, but we need the "don't generalise over Concrete variables"
stuff anyway.
-
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -513,12 +513,12 @@ ppr_tvs tvs = braces (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
-- Instantiate a type signature; only used with plan InferGen
-tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
+tcInstSig hs_sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
= setSrcSpan loc $ -- Set the binding site of the tyvars
do { (tv_prs, theta, tau) <- tcInstTypeBndrs (idType poly_id)
-- See Note [Pattern bindings and complete signatures]
- ; return (TISI { sig_inst_sig = sig
+ ; return (TISI { sig_inst_sig = hs_sig
, sig_inst_skols = tv_prs
, sig_inst_wcs = []
, sig_inst_wcx = Nothing
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1,4 +1,4 @@
-{-# LANGUAGE RecursiveDo #-}
+{-# LANGUAGE MultiWayIf, RecursiveDo #-}
module GHC.Tc.Solver(
InferMode(..), simplifyInfer, findInferredDiff,
@@ -1142,7 +1142,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
= do { -- When quantifying, we want to preserve any order of variables as they
-- appear in partial signatures. cf. decideQuantifiedTyVars
let psig_tv_tys = [ mkTyVarTy tv | sig <- partial_sigs
- , (_,Bndr tv _) <- sig_inst_skols sig ]
+ , (_,Bndr tv _) <- sig_inst_skols sig ]
psig_theta = [ pred | sig <- partial_sigs
, pred <- sig_inst_theta sig ]
@@ -1535,8 +1535,7 @@ decideQuantification
decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
= do { -- Step 1: find the mono_tvs
; (candidates, co_vars, mono_tvs0)
- <- decidePromotedTyVars infer_mode
- name_taus psigs candidates
+ <- decidePromotedTyVars infer_mode name_taus psigs candidates
-- Step 2: default any non-mono tyvars, and re-simplify
-- This step may do some unification, but result candidates is zonked
@@ -1553,19 +1552,16 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
; min_theta <- pickQuantifiablePreds (mkVarSet qtvs) mono_tvs0 candidates
- -- Add psig_theta back in here, even though it's already
- -- part of candidates, because we always want to quantify over
- -- psig_theta, and pickQuantifiableCandidates might have
- -- dropped some e.g. CallStack constraints. c.f #14658
- -- equalities (a ~ Bool)
- -- It's helpful to use the same "find difference" algorithm here as
- -- we use in GHC.Tc.Gen.Bind.chooseInferredQuantifiers (#20921)
+ -- Take account of partial type signatures
-- See Note [Constraints in partial type signatures]
; let min_psig_theta = mkMinimalBySCs id psig_theta
- ; theta <- if null psig_theta
- then return min_theta -- Fast path for the non-partial-sig case
- else do { diff <- findInferredDiff min_psig_theta min_theta
- ; return (min_psig_theta ++ diff) }
+ ; theta <- if
+ | null psigs -> return min_theta -- Case (P3)
+ | not (all has_extra_constraints_wildcard psigs) -- Case (P2)
+ -> return min_psig_theta
+ | otherwise -- Case (P1)
+ -> do { diff <- findInferredDiff min_psig_theta min_theta
+ ; return (min_psig_theta ++ diff) }
; traceTc "decideQuantification"
(vcat [ text "infer_mode:" <+> ppr infer_mode
@@ -1576,37 +1572,62 @@ decideQuantification skol_info infer_mode rhs_tclvl name_taus psigs candidates
, text "theta:" <+> ppr theta ])
; return (qtvs, theta, co_vars) }
+ where
+ has_extra_constraints_wildcard (TISI { sig_inst_wcx = Just {} }) = True
+ has_extra_constraints_wildcard _ = False
+
{- Note [Constraints in partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have a partial type signature
- f :: (Eq a, C a, _) => blah
+Suppose we have decided to quantify over min_theta, say (Eq a, C a, Ix a).
+Then we distinguish three cases:
+
+(P1) No partial type signatures: just quantify over min_theta
+
+(P2) Partial type signatures with no extra_constraints wildcard:
+ e.g. f :: (Eq a, C a) => a -> _
+ Quantify over psig_theta: the user has explicitly specified the
+ entire context.
+
+ That may mean we have an unsolved residual constraint (Ix a) arising
+ from the RHS of the function. But so be it: the user said (Eq a, C a).
-We will ultimately quantify f over (Eq a, C a, <diff>), where
+(P3) Partial type signature with an extra_constraints wildcard.
+ e.g. f :: (Eq a, C a, _) => a -> a
+ Quantify over (psig_theta ++ diff)
+ where diff = min_theta - psig_theta, using findInferredDiff.
+ In our example, diff = Ix a
- * <diff> is the result of
- findInferredDiff (Eq a, C a) <quant-theta>
- in GHC.Tc.Gen.Bind.chooseInferredQuantifiers
+Some rationale and observations
- * <quant-theta> is the theta returned right here,
- by decideQuantification
+* See Note [When the MR applies] in GHC.Tc.Gen.Bind.
-At least for single functions we would like to quantify f over
-precisely the same theta as <quant-theta>, so that we get to take
-the short-cut path in GHC.Tc.Gen.Bind.mkExport, and avoid calling
-tcSubTypeSigma for impedance matching. Why avoid? Because it falls
-over for ambiguous types (#20921).
+* We always want to quantify over psig_theta (if present). The user specified
+ it! And pickQuantifiableCandidates might have dropped some
+ e.g. CallStack constraints. c.f #14658
+ equalities (a ~ Bool)
-We can get precisely the same theta by using the same algorithm,
-findInferredDiff.
+* In case (P3) we ask that /all/ the signatures have an extra-constraints
+ wildcard. It's a bit arbitrary; not clear what the "right" thing is.
-All of this goes wrong if we have (a) mutual recursion, (b) multiple
-partial type signatures, (c) with different constraints, and (d)
-ambiguous types. Something like
+* It's helpful to use the same "find difference" algorithm, `findInferredDiff`,
+ here as we use in GHC.Tc.Gen.Bind.chooseInferredQuantifiers (#20921)
+
+ At least for single functions we would like to quantify f over precisely the
+ same theta as <quant-theta>, so that we get to take the short-cut path in
+ `GHC.Tc.Gen.Bind.mkExport`, and avoid calling `tcSubTypeSigma` for impedance
+ matching. Why avoid? Because it falls over for ambiguous types (#20921).
+
+ We can get precisely the same theta by using the same algorithm,
+ `findInferredDiff`.
+
+* All of this goes wrong if we have (a) mutual recursion, (b) multiple
+ partial type signatures, (c) with different constraints, and (d)
+ ambiguous types. Something like
f :: forall a. Eq a => F a -> _
f x = (undefined :: a) == g x undefined
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.
+ But that's a battle for another day.
-}
decidePromotedTyVars :: InferMode
@@ -1704,7 +1725,7 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
-- by some variable that is free in the env't
mono_tvs = (mono_tvs2 `unionVarSet` constrained_tvs)
- `delVarSetList` psig_qtvs
+ `delVarSetList` psig_qtvs
-- (`delVarSetList` psig_qtvs): if the user has explicitly
-- asked for quantification, then that request "wins"
-- over the MR.
@@ -1723,6 +1744,8 @@ decidePromotedTyVars infer_mode name_taus psigs candidates
; traceTc "decidePromotedTyVars" $ vcat
[ text "infer_mode =" <+> ppr infer_mode
+ , text "psigs =" <+> ppr psigs
+ , text "psig_qtvs =" <+> ppr psig_qtvs
, text "mono_tvs0 =" <+> ppr mono_tvs0
, text "no_quant =" <+> ppr no_quant
, text "maybe_quant =" <+> ppr maybe_quant
@@ -1844,7 +1867,8 @@ decideQuantifiedTyVars skol_info name_taus psigs candidates
-- See Note [pickQuantifiablePreds]
pickQuantifiablePreds
:: TyVarSet -- Quantifying over these
- -> TcTyVarSet -- These ones are free in the enviroment
+ -> 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
-- This function decides whether a particular constraint should be
@@ -1856,9 +1880,9 @@ pickQuantifiablePreds qtvs mono_tvs0 theta
mapMaybe (pick_me is_nested) theta) }
where
pick_me is_nested pred
- | let pred_tvs = tyCoVarsOfType pred
+ = let pred_tvs = tyCoVarsOfType pred
mentions_qtvs = pred_tvs `intersectsVarSet` qtvs
- = case classifyPredType pred of
+ in case classifyPredType pred of
ClassPred cls tys
| Just {} <- isCallStackPred cls tys
@@ -2109,15 +2133,16 @@ 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. We never want to show the programmer a type with `Any` in it.
+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:
-Hence, for a top-level binding, we eliminate the candidate from the
-pool, by asking
- Do not quantify over the constraint if it mentions a variable that is
- (a) not quantified (i.e. is determined by the type environment), but
- (b) do not appear literally in the environment (mono_tvs0)?
+ 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
@@ -2131,14 +2156,24 @@ 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 -- except by the fudep.
-
-However this 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.
+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.
@@ -3155,32 +3190,41 @@ defaultTyVarTcS the_tv
| otherwise
= return False -- the common case
-approximateWC :: Bool -> WantedConstraints -> Cts
+approximateWC :: Bool -- See Wrinkle (W3) in Note [ApproximateWC]
+ -> WantedConstraints
+ -> Cts
-- Second return value is the depleted wc
--- Third return value is YesFDsCombined <=> multiple constraints for the same fundep floated
-- Postcondition: Wanted Cts
-- See Note [ApproximateWC]
-- See Note [floatKindEqualities vs approximateWC]
approximateWC float_past_equalities wc
- = float_wc emptyVarSet wc
+ = float_wc False emptyVarSet wc
where
- float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
- float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
- = filterBag (is_floatable trapping_tvs) simples `unionBags`
- concatMapBag (float_implic trapping_tvs) implics
- float_implic :: TcTyCoVarSet -> Implication -> Cts
- float_implic trapping_tvs imp
- | float_past_equalities || ic_given_eqs imp /= MaybeGivenEqs
- = float_wc new_trapping_tvs (ic_wanted imp)
- | otherwise -- Take care with equalities
- = emptyCts -- See (1) under Note [ApproximateWC]
+ 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
+ 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
-
- is_floatable skol_tvs ct
- | isGivenCt ct = False
- | insolubleEqCt ct = False
- | otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+ new_encl_eqs = encl_eqs || ic_given_eqs imp == MaybeGivenEqs
+
+ is_floatable encl_eqs skol_tvs ct
+ | isGivenCt ct = False
+ | insolubleEqCt ct = False
+ | tyCoVarsOfCt ct `intersectsVarSet` skol_tvs = False
+ | 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
{- Note [ApproximateWC]
~~~~~~~~~~~~~~~~~~~~~~~
@@ -3193,28 +3237,39 @@ 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.
-There is one caveat:
-
-1. When inferring most-general types (in simplifyInfer), we do *not*
- float anything out if the implication binds equality constraints,
- because that defeats the OutsideIn story. Consider
- data T a where
- TInt :: T Int
- MkT :: T a
-
- f TInt = 3::Int
-
- We get the implication (a ~ Int => res ~ Int), where so far we've decided
- f :: T a -> res
- We don't want to float (res~Int) out because then we'll infer
- f :: T a -> Int
- which is only on of the possible types. (GHC 7.6 accidentally *did*
- float out of such implications, which meant it would happily infer
- non-principal types.)
-
- HOWEVER (#12797) in findDefaultableGroups we are not worried about
- the most-general type; and we /do/ want to float out of equalities.
- Hence the boolean flag to approximateWC.
+Wrinkle (W1)
+ When inferring most-general types (in simplifyInfer), we
+ do *not* float an equality constraint if the implication binds
+ equality constraints, because that defeats the OutsideIn story.
+ Consider data T a where TInt :: T Int MkT :: T a
+
+ f TInt = 3::Int
+
+ We get the implication (a ~ Int => res ~ Int), where so far we've decided
+ f :: T a -> res
+ We don't want to float (res~Int) out because then we'll infer
+ f :: T a -> Int
+ which is only on of the possible types. (GHC 7.6 accidentally *did*
+ float out of such implications, which meant it would happily infer
+ 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.
+
+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.
------ Historical note -----------
There used to be a second caveat, driven by #8155
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -591,9 +591,7 @@ data CtOrigin
| IfThenElseOrigin -- An if-then-else expression
| BracketOrigin -- An overloaded quotation bracket
| StaticOrigin -- A static form
- | Shouldn'tHappenOrigin String
- -- the user should never see this one
- | GhcBug20076 -- see #20076
+ | Shouldn'tHappenOrigin String -- The user should never see this one
-- | Testing whether the constraint associated with an instance declaration
-- in a signature file is satisfied upon instantiation.
@@ -819,13 +817,6 @@ pprCtOrigin (Shouldn'tHappenOrigin note)
, text "https://gitlab.haskell.org/ghc/ghc/wikis/report-a-bug >>"
]
-pprCtOrigin GhcBug20076
- = vcat [ text "GHC Bug #20076 <https://gitlab.haskell.org/ghc/ghc/-/issues/20076>"
- , text "Assuming you have a partial type signature, you can avoid this error"
- , text "by either adding an extra-constraints wildcard (like `(..., _) => ...`,"
- , text "with the underscore at the end of the constraint), or by avoiding the"
- , text "use of a simplifiable constraint in your partial type signature." ]
-
pprCtOrigin (ProvCtxtOrigin PSB{ psb_id = (L _ name) })
= hang (ctoHerald <+> text "the \"provided\" constraints claimed by")
2 (text "the signature of" <+> quotes (ppr name))
@@ -927,7 +918,6 @@ pprCtO (ProvCtxtOrigin {}) = text "a provided constraint"
pprCtO (InstProvidedOrigin {}) = text "a provided constraint"
pprCtO (CycleBreakerOrigin orig) = pprCtO orig
pprCtO (FRROrigin {}) = text "a representation-polymorphism check"
-pprCtO GhcBug20076 = text "GHC Bug #20076"
pprCtO (WantedSuperclassOrigin {}) = text "a superclass constraint"
pprCtO (InstanceSigOrigin {}) = text "a type signature in an instance"
pprCtO (AmbiguityCheckOrigin {}) = text "a type ambiguity check"
=====================================
testsuite/tests/partial-sigs/should_compile/T10403.stderr
=====================================
@@ -14,41 +14,17 @@ T10403.hs:16:12: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
• In the type signature: h1 :: _ => _
T10403.hs:20:7: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
- • Found type wildcard ‘_’
- standing for ‘(a1 -> a2) -> f0 a1 -> H f0’
- Where: ‘f0’ is an ambiguous type variable
- ‘a2’, ‘a1’ are rigid type variables bound by
- the inferred type of h2 :: (a1 -> a2) -> f0 a1 -> H f0
+ • Found type wildcard ‘_’ standing for ‘(a1 -> a2) -> f a1 -> H f’
+ Where: ‘a2’, ‘a1’, ‘f’ are rigid type variables bound by
+ the inferred type of h2 :: (a1 -> a2) -> f a1 -> H f
at T10403.hs:23:1-41
• In the type signature: h2 :: _
T10403.hs:23:15: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
- • Ambiguous type variable ‘f0’ arising from a use of ‘fmap’
- prevents the constraint ‘(Functor f0)’ from being solved.
- Relevant bindings include
- b :: f0 a1 (bound at T10403.hs:23:6)
- h2 :: (a1 -> a2) -> f0 a1 -> H f0 (bound at T10403.hs:23:1)
- Probable fix: use a type annotation to specify what ‘f0’ should be.
- Potentially matching instances:
- instance Functor IO -- Defined in ‘GHC.Base’
- instance Functor (B t) -- Defined at T10403.hs:11:10
- ...plus 8 others
- ...plus one instance involving out-of-scope types
- (use -fprint-potential-instances to see them all)
+ • No instance for ‘Functor f’ arising from a use of ‘fmap’
+ Possible fix:
+ add (Functor f) to the context of
+ the inferred type of h2 :: (a1 -> a2) -> f a1 -> H f
• In the second argument of ‘(.)’, namely ‘fmap (const ())’
In the expression: (H . fmap (const ())) (fmap f b)
In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b)
-
-T10403.hs:29:8: warning: [GHC-46956] [-Wdeferred-type-errors (in -Wdefault)]
- • Couldn't match type ‘f0’ with ‘B t’
- Expected: H (B t)
- Actual: H f0
- • because type variable ‘t’ would escape its scope
- This (rigid, skolem) type variable is bound by
- the type signature for:
- app2 :: forall t. H (B t)
- at T10403.hs:28:1-15
- • In the expression: h2 (H . I) (B ())
- In an equation for ‘app2’: app2 = h2 (H . I) (B ())
- • Relevant bindings include
- app2 :: H (B t) (bound at T10403.hs:29:1)
=====================================
testsuite/tests/partial-sigs/should_compile/T19106.hs
=====================================
@@ -3,6 +3,13 @@
module T19106 where
+-- This is a very subtle program:
+-- From the body of the function we get [W] Show a
+-- That can be satisfied only from the /combination/ of
+-- [G] a ~ [b] from type sig
+-- [G] G a from pattern match (MkT x)
+-- The type instance G [b] = Show b
+
f :: (a ~ [b]) => T a -> _ -> String
f (MkT x) _ = show x
=====================================
testsuite/tests/partial-sigs/should_compile/all.T
=====================================
@@ -71,7 +71,7 @@ test('T10519', normal, compile, [''])
test('T10463', normal, compile, [''])
test('ExprSigLocal', normal, compile, [''])
test('T11016', normal, compile, [''])
-test('T11192', normal, compile, [''])
+test('T11192', expect_broken(23232), compile, [''])
test('SuperCls', normal, compile, [''])
test('T12033', normal, compile, [''])
test('T11339a', normal, compile, [''])
=====================================
testsuite/tests/partial-sigs/should_fail/T23223.hs
=====================================
@@ -0,0 +1,5 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+module Foo where
+
+f :: (Show a) => a -> _ -> Bool
+f x y = x>x
=====================================
testsuite/tests/partial-sigs/should_fail/T23223.stderr
=====================================
@@ -0,0 +1,11 @@
+
+T23223.hs:5:10: error: [GHC-39999]
+ • Could not deduce ‘Ord a’ arising from a use of ‘>’
+ from the context: Show a
+ bound by the inferred type of f :: Show a => a -> w -> Bool
+ at T23223.hs:5:1-11
+ Possible fix:
+ add (Ord a) to the context of
+ the inferred type of f :: Show a => a -> w -> Bool
+ • In the expression: x > x
+ In an equation for ‘f’: f x y = x > x
=====================================
testsuite/tests/partial-sigs/should_fail/all.T
=====================================
@@ -1,6 +1,6 @@
test('AnnotatedConstraint', normal, compile_fail, [''])
test('AnnotatedConstraintNotForgotten', normal, compile_fail, [''])
-test('Defaulting1MROff', normal, compile, [''])
+test('Defaulting1MROff', expect_broken(23232), compile, [''])
test('ExtraConstraintsWildcardInExpressionSignature', normal, compile, [''])
test('ExtraConstraintsWildcardInPatternSignature', normal, compile_fail, [''])
test('ExtraConstraintsWildcardInPatternSplice', [req_interp, normal], compile_fail, [''])
@@ -58,7 +58,7 @@ test('WildcardInTypeSynonymRHS', normal, compile_fail, [''])
test('T10615', normal, compile_fail, [''])
test('T10045', normal, compile_fail, [''])
test('T10999', normalise_fun(normalise_errmsg), compile_fail, [''])
-test('T11122', normal, compile, [''])
+test('T11122', expect_broken(23232), compile, [''])
test('T11515', normal, compile_fail, [''])
test('T11976', normal, compile_fail, [''])
test('PatBind3', normal, compile_fail, [''])
@@ -72,3 +72,4 @@ test('T14449', normal, compile_fail, [''])
test('T14479', normal, compile_fail, [''])
test('T14584', normal, compile, [''])
test('T14584a', normal, compile, [''])
+test('T23223', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/58df60df7efe9e7920d962da3525a35826608b2d...7d6284dacc3bf215bfe55006e830583b0d163074
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/58df60df7efe9e7920d962da3525a35826608b2d...7d6284dacc3bf215bfe55006e830583b0d163074
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/20230407/11839646/attachment-0001.html>
More information about the ghc-commits
mailing list