[project @ 2004-08-18 09:33:03 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index db7e183..b7002f8 100644 (file)
@@ -21,12 +21,12 @@ 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
 import Inst            ( lookupInst, LookupInstResult(..),
-                         tyVarsOfInst, fdPredsOfInsts, fdPredsOfInst, newDicts,
+                         tyVarsOfInst, fdPredsOfInsts, newDicts, 
                          isDict, isClassDict, isLinearInst, linearInstType,
                          isStdClassTyVarDict, isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
@@ -35,16 +35,16 @@ import Inst         ( lookupInst, LookupInstResult(..),
                          newDictsFromOld, tcInstClassOp,
                          getDictClassTys, isTyVarDict,
                          instLoc, zonkInst, tidyInsts, tidyMoreInsts,
-                         Inst, pprInsts, pprInstsInFull, tcGetInstEnvs,
-                         isIPDict, isInheritableInst, pprDFuns
+                         Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
+                         isIPDict, isInheritableInst, pprDFuns, pprDictsTheta
                        )
 import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals )
-import InstEnv         ( lookupInstEnv, classInstEnv )
+import InstEnv         ( lookupInstEnv, classInstances )
 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,100 @@ 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 (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..}) 
+  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.
+  
+
+A note about Plan C (arising from "bug" reported by George Russel March 2004)
+Consider this:
+
+      instance (HasBinary ty IO) => HasCodedValue ty
+
+      foo :: HasCodedValue a => String -> IO a
+
+      doDecodeIO :: HasCodedValue a => () -> () -> IO a
+      doDecodeIO codedValue view  
+        = let { act = foo "foo" } in  act
+
+You might think this should work becuase the call to foo gives rise to a constraint
+(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO.  But the
+restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
+constraint using the (rather bogus) instance declaration, and now we are stuffed.
+
+I claim this is not really a bug -- but it bit Sergey as well as George.  So here's
+plan D
+
+
+Plan D (a variant of plan B)
+  Step 1: Simplify the constraints as much as possible (to deal 
+  with Plan A's problem), BUT DO NO IMPROVEMENT.  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 point here is that it's generally OK to have too few qtvs; that is,
+  to make the thing more monomorphic than it could be.  We don't want to
+  do that in the common cases, but in wierd cases it's ok: the programmer
+  can always add a signature.  
+
+  Too few qtvs => too many wanteds, which is what happens if you do less
+  improvement.
+
+
 \begin{code}
 tcSimplifyRestricted   -- Used for restricted binding groups
                        -- i.e. ones subject to the monomorphism restriction
@@ -863,39 +957,41 @@ 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
+       -- Zonk everything in sight
+  = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
+    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
+    tcGetGlobalTyVars                          `thenM` \ gbl_tvs' ->
+
+       -- '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) ->
+       --
+       -- BUT do no improvement!  See Plan D above
+    reduceContextWithoutImprovement 
+       doc reduceMe wanteds'           `thenM` \ (_frees, _binds, constrained_dicts) ->
 
        -- 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)
+       qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
                         `minusVarSet` constrained_tvs
+        try_me inst | isFreeWrtTyVars qtvs inst = Free
+                   | otherwise                 = ReduceMe
     in
     traceTc (text "tcSimplifyRestricted" <+> vcat [
-               pprInsts wanteds, pprInsts foo_frees, pprInsts constrained_dicts,
-               ppr foo_binds,
+               pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
+               ppr _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
+       -- necessary, so try again, this time more gently, knowing the exact
        -- set of type variables to quantify over.
        --
        -- We quantify only over constraints that are captured by qtvs;
@@ -907,28 +1003,11 @@ tcSimplifyRestricted doc tau_tvs wanteds
        -- 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)
+    reduceContextWithoutImprovement 
+       doc try_me wanteds'             `thenM` \ (frees, binds, irreds) ->
+    ASSERT( null irreds )
+    extendLIEs frees                   `thenM_`
+    returnM (varSetElems qtvs, binds)
 \end{code}
 
 
@@ -975,7 +1054,7 @@ because the scsel will mess up matching.  Instead we want
        forall dIntegralInt, dNumInt.
        fromIntegral Int Int dIntegralInt dNumInt = id Int
 
-Hence "DontReduce NoSCs"
+Hence "WithoutSCs"
 
 \begin{code}
 tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
@@ -991,7 +1070,7 @@ tcSimplifyToDicts wanteds
     doc = text "tcSimplifyToDicts"
 
        -- Reduce methods and lits only; stop as soon as we get a dictionary
-    try_me inst        | isDict inst = DontReduce NoSCs        -- See notes above for why NoSCs
+    try_me inst        | isDict inst = KeepDictWithoutSCs      -- See notes above re "WithoutSCs"
                | otherwise   = ReduceMe
 \end{code}
 
@@ -1135,7 +1214,8 @@ data WhatToDo
                        -- produce an error message of any kind.
                        -- It might be quite legitimate such as (Eq a)!
 
- | DontReduce WantSCs          -- Return as irreducible
+ | KeepDictWithoutSCs  -- Return as irreducible; don't add its superclasses
+                       -- Rather specialised: see notes with tcSimplifyToDicts
 
  | DontReduceUnlessConstant    -- Return as irreducible unless it can
                                -- be reduced to a constant in one step
@@ -1153,6 +1233,7 @@ data WantSCs = NoSCs | AddSCs     -- Tells whether we should add the superclasses
 
 \begin{code}
 type Avails = FiniteMap Inst Avail
+emptyAvails = emptyFM
 
 data Avail
   = IsFree             -- Used for free Insts
@@ -1393,7 +1474,7 @@ reduceContext doc try_me givens wanteds
             ]))                                        `thenM_`
 
         -- Build the Avail mapping from "givens"
-    foldlM addGiven emptyFM givens                     `thenM` \ init_state ->
+    foldlM addGiven emptyAvails givens                 `thenM` \ init_state ->
 
         -- Do the real work
     reduceList (0,[]) try_me wanteds init_state                `thenM` \ avails ->
@@ -1418,23 +1499,54 @@ reduceContext doc try_me givens wanteds
 
     returnM (no_improvement, frees, binds, irreds)
 
+-- reduceContextWithoutImprovement differs from reduceContext
+--     (a) no improvement
+--     (b) 'givens' is assumed empty
+reduceContextWithoutImprovement doc try_me wanteds
+  =
+    traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
+            text "----------------------",
+            doc,
+            text "wanted" <+> ppr wanteds,
+            text "----------------------"
+            ]))                                        `thenM_`
+
+        -- Do the real work
+    reduceList (0,[]) try_me wanteds emptyAvails       `thenM` \ avails ->
+    extractResults avails wanteds                      `thenM` \ (binds, irreds, frees) ->
+
+    traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
+            text "----------------------",
+            doc,
+            text "wanted" <+> ppr wanteds,
+            text "----",
+            text "avails" <+> pprAvails avails,
+            text "frees" <+> ppr frees,
+            text "----------------------"
+            ]))                                        `thenM_`
+
+    returnM (frees, binds, irreds)
+
 tcImprove :: Avails -> TcM Bool                -- False <=> no change
 -- Perform improvement using all the predicates in Avails
 tcImprove avails
- =  tcGetInstEnvs                      `thenM` \ (home_ie, pkg_ie) ->
+ =  tcGetInstEnvs                      `thenM` \ inst_envs -> 
     let
-       preds = [ (pred, pp_loc)
+       preds = [ (dictPred inst, pp_loc)
                | inst <- keysFM avails,
-                 let pp_loc = pprInstLoc (instLoc inst),
-                 pred <- fdPredsOfInst inst
+                 isDict inst,
+                 let pp_loc = pprInstLoc (instLoc inst)
                ]
                -- Avails has all the superclasses etc (good)
                -- It also has all the intermediates of the deduction (good)
                -- It does not have duplicates (good)
                -- NB that (?x::t1) and (?x::t2) will be held separately in avails
                --    so that improve will see them separate
+               --
+               -- Notice that we only look at dicts; LitInsts and Methods will have
+               -- been squished, so their dicts will be in Avails too
        eqns = improve get_insts preds
-       get_insts clas = classInstEnv home_ie clas ++ classInstEnv pkg_ie clas
+       get_insts clas = classInstances inst_envs clas
      in
      if null eqns then
        returnM True
@@ -1443,10 +1555,11 @@ tcImprove avails
         mappM_ unify eqns      `thenM_`
        returnM False
   where
-    unify ((qtvs, t1, t2), doc)
+    unify ((qtvs, pairs), doc)
         = addErrCtxt doc                               $
           tcInstTyVars VanillaTv (varSetElems qtvs)    `thenM` \ (_, _, tenv) ->
-          unifyTauTy (substTy tenv t1) (substTy tenv t2)
+          mapM_ (unif_pr tenv) pairs
+    unif_pr tenv (ty1,ty2) =  unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.
@@ -1486,7 +1599,8 @@ reduceList (n,stack) try_me wanteds state
   =
 #ifdef DEBUG
    (if n > 8 then
-       pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
+       pprTrace "Interesting! Context reduction stack deeper than 8:" 
+                (nest 2 (pprStack stack))
     else (\x->x))
 #endif
     go wanteds state
@@ -1508,7 +1622,7 @@ reduce stack try_me wanted avails
   | otherwise
   = case try_me wanted of {
 
-      DontReduce want_scs -> addIrred want_scs avails wanted
+      KeepDictWithoutSCs -> addIrred NoSCs avails wanted
 
     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
                                     -- First, see if the inst can be reduced to a constant in one step
@@ -2113,7 +2227,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
@@ -2140,38 +2254,44 @@ addNoInstanceErrs mb_what givens dicts
          | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
          | otherwise
          = case lookupInstEnv dflags inst_envs clas tys of
-               res@(ms, _) 
-                 | length ms > 1 -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
-                 | otherwise     -> (overlap_doc, dict : no_inst_dicts)        -- No match
-               -- NB: there can be exactly one match, in the case where we have
-               --      instance C a where ...
-               -- (In this case, lookupInst doesn't bother to look up, 
-               --  unless -fallow-undecidable-instances is set.)
-               -- So we report this as "no instance" rather than "overlap"; the fix is
-               -- to specify -fallow-undecidable-instances, but we leave that to the programmer!
+               -- The case of exactly one match and no unifiers means
+               -- a successful lookup.  That can't happen here.
+#ifdef DEBUG
+               ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
+#endif
+               ([], _)  -> (overlap_doc, dict : no_inst_dicts)         -- No match
+               res      -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
          where
            (clas,tys) = getDictClassTys dict
     in
+       
+       -- Now generate a good message for the no-instance bunch
     mk_probable_fix tidy_env2 mb_what no_inst_dicts    `thenM` \ (tidy_env3, probable_fix) ->
     let
        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
+       -- And emit both the non-instance and overlap messages
     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 
-               then empty
-               else parens (ptext SLIT("The choice depends on the instantiation of") <+>
-                            quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))))]
+               ASSERT( not (null matches) )
+               if not (isSingleton matches)
+               then    -- Two or more matches
+                    empty
+               else    -- One match, plus some unifiers
+               ASSERT( not (null unifiers) )
+               parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
+                                quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
+                             ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
       where
        dfuns = [df | (_, (_,_,df)) <- matches]
 
@@ -2180,12 +2300,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 +2331,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 +2366,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 +2377,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 (pprStack stack)]
 
-reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
+pprStack stack = vcat (map pprInstInFull stack)
 \end{code}