[project @ 2004-03-11 14:34:22 by simonpj]
authorsimonpj <unknown>
Thu, 11 Mar 2004 14:34:24 +0000 (14:34 +0000)
committersimonpj <unknown>
Thu, 11 Mar 2004 14:34:24 +0000 (14:34 +0000)
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
ghc/compiler/typecheck/TcEnv.lhs
ghc/compiler/typecheck/TcExpr.lhs
ghc/compiler/typecheck/TcSimplify.lhs

index f27a782..eaf433e 100644 (file)
@@ -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}
 
 
index cf86e56..cb2eb28 100644 (file)
@@ -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
index 8383353..1714a33 100644 (file)
@@ -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
index db7e183..3c0ac28 100644 (file)
@@ -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}