Commit ff3d07ad authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Improve TcSimplify.approximateWC, fixing Trac #8155

See Note [ApproximateWC]
parent f5d148cf
......@@ -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
......
......@@ -816,29 +816,34 @@ 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
new_trapping_tvs = trapping_tvs `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
do_bag :: (a -> Bag c) -> Bag a -> Bag c
do_bag f = foldrBag (unionBags.f) emptyBag
\end{code}
......@@ -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]
~~~~~~~~~~~~~~~~~~~
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment