From 9ec3012e2fd5b998e32897c03551574038fd59a8 Mon Sep 17 00:00:00 2001 From: simonpj Date: Thu, 11 Mar 2004 14:34:24 +0000 Subject: [PATCH] [project @ 2004-03-11 14:34:22 by simonpj] Fix a nasty and long-standing bug in the handling of functional dependencies. The story is told in comments with TcSimplify.tcSimplifyRestricted. We were simpifying a group of constraints *twice*: once to establish the type vars to quantify over, and once "for real" but less brutally. Unfortunately, the less-brutally part meant that we did less improvement, which in turn meant that an invariant (no captured constraints) was violated. Consequential bizarre results. The test is typecheck/should_compile/tc177 --- ghc/compiler/typecheck/Inst.lhs | 42 +++++---- ghc/compiler/typecheck/TcEnv.lhs | 4 +- ghc/compiler/typecheck/TcExpr.lhs | 5 +- ghc/compiler/typecheck/TcSimplify.lhs | 154 +++++++++++++++++++-------------- 4 files changed, 119 insertions(+), 86 deletions(-) diff --git a/ghc/compiler/typecheck/Inst.lhs b/ghc/compiler/typecheck/Inst.lhs index f27a782..eaf433e 100644 --- a/ghc/compiler/typecheck/Inst.lhs +++ b/ghc/compiler/typecheck/Inst.lhs @@ -8,7 +8,7 @@ module Inst ( showLIE, Inst, - pprInst, pprInsts, pprInstsInFull, pprDFuns, + pprInst, pprInsts, pprDFuns, pprDictsTheta, pprDictsInFull, tidyInsts, tidyMoreInsts, newDictsFromOld, newDicts, cloneDict, @@ -63,7 +63,7 @@ import TcType ( Type, TcType, TcThetaType, TcTyVarSet, getClassPredTys, getClassPredTys_maybe, mkPredName, isInheritablePred, isIPPred, matchTys, tidyType, tidyTypes, tidyFreeTyVars, tcSplitSigmaTy, - pprPred, pprParendType, pprThetaArrow, pprClassPred + pprPred, pprParendType, pprThetaArrow, pprTheta, pprClassPred ) import Kind ( isSubKind ) import HscTypes ( ExternalPackageState(..) ) @@ -496,27 +496,33 @@ relevant in error messages. instance Outputable Inst where ppr inst = pprInst inst -pprInsts :: [Inst] -> SDoc -pprInsts insts = parens (sep (punctuate comma (map pprInst insts))) +pprDictsTheta :: [Inst] -> SDoc +-- Print in type-like fashion (Eq a, Show b) +pprDictsTheta dicts = pprTheta (map dictPred dicts) -pprInstsInFull insts - = vcat (map go insts) +pprDictsInFull :: [Inst] -> SDoc +-- Print in type-like fashion, but with source location +pprDictsInFull dicts + = vcat (map go dicts) where - go inst = sep [quotes (ppr inst), nest 2 (pprInstLoc (instLoc inst))] + go dict = sep [quotes (ppr (dictPred dict)), nest 2 (pprInstLoc (instLoc dict))] -pprInst (LitInst u lit ty loc) - = hsep [ppr lit, ptext SLIT("at"), ppr ty, show_uniq u] +pprInsts :: [Inst] -> SDoc +-- Debugging: print the evidence :: type +pprInsts insts = brackets (interpp'SP insts) -pprInst (Dict u pred loc) = pprPred pred <+> show_uniq u +pprInst, pprInstInFull :: Inst -> SDoc +-- Debugging: print the evidence :: type +pprInst (LitInst id lit ty loc) = ppr id <+> dcolon <+> ppr ty +pprInst (Dict id pred loc) = ppr id <+> dcolon <+> pprPred pred -pprInst m@(Method u id tys theta tau loc) - = hsep [ppr id, ptext SLIT("at"), - brackets (sep (map pprParendType tys)) {- , - ptext SLIT("theta"), ppr theta, - ptext SLIT("tau"), ppr tau - show_uniq u, - ppr (instToId m) -}] +pprInst m@(Method inst_id id tys theta tau loc) + = ppr inst_id <+> dcolon <+> + braces (sep [ppr id <+> ptext SLIT("at"), + brackets (sep (map pprParendType tys))]) +pprInstInFull inst + = sep [quotes (pprInst inst), nest 2 (pprInstLoc (instLoc inst))] pprDFuns :: [DFunId] -> SDoc -- Prints the dfun as an instance declaration @@ -549,7 +555,7 @@ showLIE :: SDoc -> TcM () -- Debugging showLIE str = do { lie_var <- getLIEVar ; lie <- readMutVar lie_var ; - traceTc (str <+> pprInstsInFull (lieToList lie)) } + traceTc (str <+> vcat (map pprInstInFull (lieToList lie))) } \end{code} diff --git a/ghc/compiler/typecheck/TcEnv.lhs b/ghc/compiler/typecheck/TcEnv.lhs index cf86e56..cb2eb28 100644 --- a/ghc/compiler/typecheck/TcEnv.lhs +++ b/ghc/compiler/typecheck/TcEnv.lhs @@ -47,7 +47,7 @@ module TcEnv( #include "HsVersions.h" -import HsSyn ( LRuleDecl, LHsBinds, LSig ) +import HsSyn ( LRuleDecl, LHsBinds, LSig, pprLHsBinds ) import TcIface ( tcImportDecl ) import TcRnMonad import TcMType ( zonkTcType, zonkTcTyVar, zonkTcTyVarsAndFV ) @@ -601,7 +601,7 @@ pprInstInfo info = vcat [ptext SLIT("InstInfo:") <+> ppr (idType (iDFunId info)) pprInstInfoDetails info = pprInstInfo info $$ nest 2 (details (iBinds info)) where - details (VanillaInst b _) = ppr b + details (VanillaInst b _) = pprLHsBinds b details (NewTypeDerived _) = text "Derived from the representation type" simpleInstInfoTy :: InstInfo -> Type diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs index 8383353..1714a33 100644 --- a/ghc/compiler/typecheck/TcExpr.lhs +++ b/ghc/compiler/typecheck/TcExpr.lhs @@ -654,7 +654,10 @@ tcApp fun args res_ty -- and say so. -- The ~(Check...) is because in the Infer case the tcSubExp -- definitely won't fail, so we can be certain we're in the Check branch -checkArgsCtxt fun args ~(Check expected_res_ty) actual_res_ty tidy_env +checkArgsCtxt fun args (Infer _) actual_res_ty tidy_env + = return (tidy_env, ptext SLIT("Urk infer")) + +checkArgsCtxt fun args (Check expected_res_ty) actual_res_ty tidy_env = zonkTcType expected_res_ty `thenM` \ exp_ty' -> zonkTcType actual_res_ty `thenM` \ act_ty' -> let diff --git a/ghc/compiler/typecheck/TcSimplify.lhs b/ghc/compiler/typecheck/TcSimplify.lhs index db7e183..3c0ac28 100644 --- a/ghc/compiler/typecheck/TcSimplify.lhs +++ b/ghc/compiler/typecheck/TcSimplify.lhs @@ -21,7 +21,7 @@ module TcSimplify ( import {-# SOURCE #-} TcUnify( unifyTauTy ) import TcEnv -- temp -import HsSyn ( HsBind(..), LHsBinds, HsExpr(..), LHsExpr ) +import HsSyn ( HsBind(..), LHsBinds, HsExpr(..), LHsExpr, pprLHsBinds ) import TcHsSyn ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp ) import TcRnMonad @@ -35,8 +35,8 @@ import Inst ( lookupInst, LookupInstResult(..), newDictsFromOld, tcInstClassOp, getDictClassTys, isTyVarDict, instLoc, zonkInst, tidyInsts, tidyMoreInsts, - Inst, pprInsts, pprInstsInFull, tcGetInstEnvs, - isIPDict, isInheritableInst, pprDFuns + Inst, pprInsts, pprDictsInFull, tcGetInstEnvs, + isIPDict, isInheritableInst, pprDFuns, pprDictsTheta ) import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals ) import InstEnv ( lookupInstEnv, classInstEnv ) @@ -44,7 +44,7 @@ import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity ) import TcType ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv), mkClassPred, isOverloadedTy, mkTyConApp, mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys, - tyVarsOfPred, tcEqType ) + tyVarsOfPred, tcEqType, pprPred ) import Id ( idType, mkUserLocal ) import Var ( TyVar ) import Name ( getOccName, getSrcLoc ) @@ -855,6 +855,64 @@ tcSimplCheck doc get_qtvs givens wanted_lie %* * %************************************************************************ +tcSimplifyRestricted infers which type variables to quantify for a +group of restricted bindings. This isn't trivial. + +Eg1: id = \x -> x + We want to quantify over a to get id :: forall a. a->a + +Eg2: eq = (==) + We do not want to quantify over a, because there's an Eq a + constraint, so we get eq :: a->a->Bool (notice no forall) + +So, assume: + RHS has type 'tau', whose free tyvars are tau_tvs + RHS has constraints 'wanteds' + +Plan A (simple) + Quantify over (tau_tvs \ ftvs(wanteds)) + This is bad. The constraints may contain (Monad (ST s)) + where we have instance Monad (ST s) where... + so there's no need to be monomorphic in s! + + Also the constraint might be a method constraint, + whose type mentions a perfectly innocent tyvar: + op :: Num a => a -> b -> a + Here, b is unconstrained. A good example would be + foo = op (3::Int) + We want to infer the polymorphic type + foo :: forall b. b -> b + + +Plan B (cunning, used for a long time up to and including GHC 6.2) + Step 1: Simplify the constraints as much as possible (to deal + with Plan A's problem). Then set + qtvs = tau_tvs \ ftvs( simplify( wanteds ) ) + + Step 2: Now simplify again, treating the constraint as 'free' if + it does not mention qtvs, and trying to reduce it otherwise. + The reasons for this is to maximise sharing. + + This fails for a very subtle reason. Suppose that in the Step 2 + a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'. + In the Step 1 this constraint might have been simplified, perhaps to + (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'. + This won't happen in Step 2... but that in turn might prevent some other + constraint mentioning 'b' from being simplified... and that in turn + breaks the invariant that no constraints are quantified over. + + Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates + the problem. + + +Plan C (brutal) + Step 1: Simplify the constraints as much as possible (to deal + with Plan A's problem). Then set + qtvs = tau_tvs \ ftvs( simplify( wanteds ) ) + Return the bindings from Step 1. + + + \begin{code} tcSimplifyRestricted -- Used for restricted binding groups -- i.e. ones subject to the monomorphism restriction @@ -863,72 +921,37 @@ tcSimplifyRestricted -- Used for restricted binding groups -> [Inst] -- Free in the RHSs -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) TcDictBinds) -- Bindings + -- tcSimpifyRestricted returns no constraints to + -- quantify over; by definition there are none. + -- They are all thrown back in the LIE tcSimplifyRestricted doc tau_tvs wanteds - = -- First squash out all methods, to find the constrained tyvars - -- We can't just take the free vars of wanted_lie because that'll - -- have methods that may incidentally mention entirely unconstrained variables - -- e.g. a call to f :: Eq a => a -> b -> b - -- Here, b is unconstrained. A good example would be - -- foo = f (3::Int) - -- We want to infer the polymorphic type - -- foo :: forall b. b -> b - -- 'reduceMe': Reduce as far as we can. Don't stop at -- dicts; the idea is to get rid of as many type -- variables as possible, and we don't want to stop -- at (say) Monad (ST s), because that reduces -- immediately, with no constraint on s. - simpleReduceLoop doc reduceMe wanteds `thenM` \ (foo_frees, foo_binds, constrained_dicts) -> + = simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, binds, irreds) -> + ASSERT( null frees ) -- Next, figure out the tyvars we will quantify over zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' -> tcGetGlobalTyVars `thenM` \ gbl_tvs -> let - constrained_tvs = tyVarsOfInsts constrained_dicts - qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs) - `minusVarSet` constrained_tvs + constrained_tvs = tyVarsOfInsts irreds + qtvs = (tau_tvs' `minusVarSet` constrained_tvs) + `minusVarSet` oclose (fdPredsOfInsts irreds) gbl_tvs + -- The second minusVarSet arranges not to quantify over + -- any tyvars that are functionally determined by ones in + -- the environment in traceTc (text "tcSimplifyRestricted" <+> vcat [ - pprInsts wanteds, pprInsts foo_frees, pprInsts constrained_dicts, - ppr foo_binds, + pprInsts wanteds, pprInsts frees, pprInsts irreds, + pprLHsBinds binds, ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_` - -- The first step may have squashed more methods than - -- necessary, so try again, this time knowing the exact - -- set of type variables to quantify over. - -- - -- We quantify only over constraints that are captured by qtvs; - -- these will just be a subset of non-dicts. This in contrast - -- to normal inference (using isFreeWhenInferring) in which we quantify over - -- all *non-inheritable* constraints too. This implements choice - -- (B) under "implicit parameter and monomorphism" above. - -- - -- Remember that we may need to do *some* simplification, to - -- (for example) squash {Monad (ST s)} into {}. It's not enough - -- just to float all constraints - restrict_loop doc qtvs wanteds - -- We still need a loop because improvement can take place - -- E.g. if we have (C (T a)) and the instance decl - -- instance D Int b => C (T a) where ... - -- and there's a functional dependency for D. Then we may improve - -- the tyep variable 'b'. - -restrict_loop doc qtvs wanteds - = mappM zonkInst wanteds `thenM` \ wanteds' -> - zonkTcTyVarsAndFV (varSetElems qtvs) `thenM` \ qtvs' -> - let - try_me inst | isFreeWrtTyVars qtvs' inst = Free - | otherwise = ReduceMe - in - reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) -> - if no_improvement then - ASSERT( null irreds ) - extendLIEs frees `thenM_` - returnM (varSetElems qtvs', binds) - else - restrict_loop doc qtvs' (irreds ++ frees) `thenM` \ (qtvs1, binds1) -> - returnM (qtvs1, binds `unionBags` binds1) + extendLIEs irreds `thenM_` + returnM (varSetElems qtvs, binds) \end{code} @@ -2113,7 +2136,7 @@ addTopIPErrs dicts (tidy_env, tidy_dicts) = tidyInsts dicts report dicts = addErrTcM (tidy_env, mk_msg dicts) mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <> - plural tidy_dicts <+> pprInsts tidy_dicts) + plural tidy_dicts <+> pprDictsTheta tidy_dicts) addNoInstanceErrs :: Maybe SDoc -- Nothing => top level -- Just d => d describes the construct @@ -2157,15 +2180,16 @@ addNoInstanceErrs mb_what givens dicts no_inst_doc | null no_inst_dicts = empty | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix] heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+> - ptext SLIT("for") <+> pprInsts no_inst_dicts - | otherwise = sep [ptext SLIT("Could not deduce") <+> pprInsts no_inst_dicts, - nest 2 $ ptext SLIT("from the context") <+> pprInsts tidy_givens] + ptext SLIT("for") <+> pprDictsTheta no_inst_dicts + | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts, + nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens] in addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc) where mk_overlap_msg dict (matches, unifiers) - = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") <+> ppr dict)), + = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") + <+> pprPred (dictPred dict))), sep [ptext SLIT("Matching instances") <> colon, nest 2 (pprDFuns (dfuns ++ unifiers))], if null unifiers @@ -2180,12 +2204,12 @@ addNoInstanceErrs mb_what givens dicts mk_probable_fix tidy_env (Just what) dicts -- Nested (type signatures, instance decls) = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 fix1, nest 2 fix2]) where - fix1 = sep [ptext SLIT("Add") <+> pprInsts dicts, + fix1 = sep [ptext SLIT("Add") <+> pprDictsTheta dicts, ptext SLIT("to the") <+> what] fix2 | null instance_dicts = empty | otherwise = ptext SLIT("Or add an instance declaration for") - <+> pprInsts instance_dicts + <+> pprDictsTheta instance_dicts instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)] -- Insts for which it is worth suggesting an adding an instance declaration -- Exclude implicit parameters, and tyvar dicts @@ -2211,7 +2235,7 @@ addTopAmbigErrs dicts dicts = map fst pairs msg = sep [text "Ambiguous type variable" <> plural tvs <+> pprQuotedList tvs <+> in_msg, - nest 2 (pprInstsInFull dicts)] + nest 2 (pprDictsInFull dicts)] in_msg | isSingleton dicts = text "in the top-level constraint:" | otherwise = text "in these top-level constraints:" @@ -2246,7 +2270,7 @@ warnDefault dicts default_ty (_, tidy_dicts) = tidyInsts dicts warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+> quotes (ppr default_ty), - pprInstsInFull tidy_dicts] + pprDictsInFull tidy_dicts] -- Used for the ...Thetas variants; all top level badDerivedPred pred @@ -2257,7 +2281,7 @@ badDerivedPred pred reduceDepthErr n stack = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n, ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"), - nest 4 (pprInstsInFull stack)] + nest 4 (pprDictsInFull stack)] -reduceDepthMsg n stack = nest 4 (pprInstsInFull stack) +reduceDepthMsg n stack = nest 4 (pprDictsInFull stack) \end{code} -- 1.7.10.4