Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : master
http://hackage.haskell.org/trac/ghc/changeset/6a58aa0cb05bd20681435ba027c2e65bd30a5176 >--------------------------------------------------------------- commit 6a58aa0cb05bd20681435ba027c2e65bd30a5176 Author: Simon Peyton Jones <simo...@microsoft.com> Date: Fri Oct 19 01:20:12 2012 +0100 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. Example 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 >--------------------------------------------------------------- compiler/typecheck/Inst.lhs | 4 ++++ compiler/typecheck/TcSimplify.lhs | 27 +++++++++++++++++++++++++++ 2 files changed, 31 insertions(+), 0 deletions(-) diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 04ea870..305e05c 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -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 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 600a772..406fd3a 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -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) where skols' = skols `extendVarSetList` ic_skols imp `extendVarSetList` ic_fsks imp @@ -936,6 +939,30 @@ approximateWC wc do_bag f = foldrBag (unionBags.f) emptyBag \end{code} +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 _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
