[commit: ghc] master: Improve TcSimplify.approximateWC, fixing Trac #8155 (ff3d07a)
git at git.haskell.org
git at git.haskell.org
Thu Aug 29 17:45:57 CEST 2013
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/ff3d07addf6af962c4d0e69d2ac02218643046d1/ghc
>---------------------------------------------------------------
commit ff3d07addf6af962c4d0e69d2ac02218643046d1
Author: Simon Peyton Jones <simonpj at microsoft.com>
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]
~~~~~~~~~~~~~~~~~~~
More information about the ghc-commits
mailing list