Commit 6a58aa0c authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

In approximateWC, do not float contraints out of an implication with equalities

Jacques Garrigue pointed out that GHC 7.6 was accepting GADT programs
that our OutsideIn paper said would be rejected.  The reason was that
approximateWC was being too aggressive about floating; see Note
[approximateWC] in TcSimplify.

This simple patch fixes that, but it is (of course) not backward
compatible; a few GADT programs that were (erroneously) accepted
before are now rejected, and will need a type signature.  This could
be under flag control, but I'd rather just make it compulsory.

   data T a where
     TInt :: T Int
     MkT :: T a

   f TInt = 3::Int

Here f (with no type signature) is current accepted, with inferred type
 f :: T a -> Int
but should be rejected
parent e252bb6d
......@@ -524,6 +524,10 @@ hasEqualities givens = any (has_eq . evVarPred) givens
has_eq' (ClassPred cls _tys) = any has_eq (classSCTheta cls)
has_eq' (TuplePred ts) = any has_eq ts
has_eq' (IrredPred _) = True -- Might have equalities in it after reduction?
-- This is conservative. e.g. if there's a constraint function FC with
-- type instance FC Int = Show
-- then we won't float from inside a given constraint (FC Int a), even though
-- it's really the innocuous (Show a). Too bad! Add a type signature
---------------- Getting free tyvars -------------------------
tyVarsOfCt :: Ct -> TcTyVarSet
......@@ -922,6 +922,9 @@ approximateWC wc
float_implic :: TcTyVarSet -> Implication -> Cts
float_implic skols imp
| hasEqualities (ic_given imp) -- Don't float out of equalities
= emptyCts -- cf floatEqualities
| otherwise -- See Note [approximateWC]
= float_wc skols' (ic_wanted imp)
skols' = skols `extendVarSetList` ic_skols imp `extendVarSetList` ic_fsks imp
......@@ -936,6 +939,30 @@ approximateWC wc
do_bag f = foldrBag (unionBags.f) emptyBag
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
*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.)
Note [DefaultTyVar]
defaultTyVar is used on any un-instantiated meta type variables to
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