Repository : ssh://[email protected]/ghc On branch : master Link : http://ghc.haskell.org/trac/ghc/changeset/ff3d07addf6af962c4d0e69d2ac02218643046d1/ghc
>--------------------------------------------------------------- commit ff3d07addf6af962c4d0e69d2ac02218643046d1 Author: Simon Peyton Jones <[email protected]> Date: Wed Aug 28 16:37:59 2013 +0100 Improve TcSimplify.approximateWC, fixing Trac #8155 See Note [ApproximateWC] >--------------------------------------------------------------- ff3d07addf6af962c4d0e69d2ac02218643046d1 compiler/typecheck/TcRnTypes.lhs | 5 ++- compiler/typecheck/TcSimplify.lhs | 85 ++++++++++++++++++++++++------------- 2 files changed, 58 insertions(+), 32 deletions(-) diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 43b4f36..94787eb 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -916,12 +916,13 @@ data Ct cc_loc :: CtLoc } - | CNonCanonical { -- See Note [NonCanonical Semantics] + | CNonCanonical { -- See Note [NonCanonical Semantics] cc_ev :: CtEvidence, cc_loc :: CtLoc } - | CHoleCan { + | CHoleCan { -- Treated as an "insoluble" constraint + -- See Note [Insoluble constraints] cc_ev :: CtEvidence, cc_loc :: CtLoc, cc_occ :: OccName -- The name of this hole diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index b17f395..b39bc85 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -816,28 +816,33 @@ defaultTyVar the_tv approximateWC :: WantedConstraints -> Cts -- Postcondition: Wanted or Derived Cts +-- See Note [ApproximateWC] approximateWC wc = float_wc emptyVarSet wc where float_wc :: TcTyVarSet -> WantedConstraints -> Cts - float_wc skols (WC { wc_flat = flats, wc_impl = implics }) - = do_bag (float_flat skols) flats `unionBags` - do_bag (float_implic skols) implics + float_wc trapping_tvs (WC { wc_flat = flats, wc_impl = implics }) + = filterBag is_floatable flats `unionBags` + do_bag (float_implic new_trapping_tvs) implics + where + new_trapping_tvs = fixVarSet grow trapping_tvs + is_floatable ct = tyVarsOfCt ct `disjointVarSet` new_trapping_tvs + + grow tvs = foldrBag grow_one tvs flats + grow_one ct tvs | ct_tvs `intersectsVarSet` tvs = tvs `unionVarSet` ct_tvs + | otherwise = tvs + where + ct_tvs = tyVarsOfCt ct float_implic :: TcTyVarSet -> Implication -> Cts - float_implic skols imp + float_implic trapping_tvs imp | hasEqualities (ic_given imp) -- Don't float out of equalities = emptyCts -- cf floatEqualities - | otherwise -- See Note [approximateWC] - = float_wc skols' (ic_wanted imp) + | otherwise -- See Note [ApproximateWC] + = float_wc new_trapping_tvs (ic_wanted imp) where - skols' = skols `extendVarSetList` ic_skols imp `extendVarSetList` ic_fsks imp - - float_flat :: TcTyVarSet -> Ct -> Cts - float_flat skols ct - | tyVarsOfCt ct `disjointVarSet` skols - = singleCt ct - | otherwise = emptyCts + new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp + `extendVarSetList` ic_fsks imp do_bag :: (a -> Bag c) -> Bag a -> Bag c do_bag f = foldrBag (unionBags.f) emptyBag @@ -849,23 +854,43 @@ approximateWC takes a constraint, typically arising from the RHS of a let-binding whose type we are *inferring*, and extracts from it some *flat* constraints that we might plausibly abstract over. Of course the top-level flat constraints are plausible, but we also float constraints -out from inside, if the are not captured by skolems. - -However we do *not* float anything out if the implication binds equality -constriants, 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.) +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 that might be defaulted. + +There are two caveats: + +1. 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.) + +2. We do not float out an inner constraint that shares a type variable + (transitively) with one that is trapped by a skolem. Eg + forall a. F a ~ beta, Integral beta + We don't want to float out (Integral beta). Doing so would be bad + when defaulting, because then we'll default beta:=Integer, and that + makes the error message much worse; we'd get + Can't solve F a ~ Integer + rather than + Can't solve Integral (F a) + + Moreover, floating out these "contaminated" constraints doesn't help + when generalising either. If we generalise over (Integral b), we still + can't solve the retained implication (forall a. F a ~ b). Indeed, + arguably that too would be a harder error to understand. Note [DefaultTyVar] ~~~~~~~~~~~~~~~~~~~ _______________________________________________ ghc-commits mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-commits
