[project @ 2001-03-01 14:26:00 by simonmar]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index b8db28d..2e6c240 100644 (file)
@@ -31,13 +31,12 @@ import Inst         ( lookupInst, lookupSimpleInst, LookupInstResult(..),
                          getDictClassTys, getIPs, isTyVarDict,
                          instLoc, pprInst, zonkInst, tidyInst, tidyInsts,
                          Inst, LIE, pprInsts, pprInstsInFull,
-                         mkLIE, 
-                         lieToList 
+                         mkLIE, lieToList 
                        )
 import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv )
 import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
 
-import TcType          ( zonkTcTyVarsAndFV )
+import TcType          ( zonkTcTyVarsAndFV, tcInstTyVars )
 import TcUnify         ( unifyTauTy )
 import Id              ( idType )
 import Name            ( Name )
@@ -50,7 +49,7 @@ import Type           ( Type, ClassContext,
                          mkTyVarTy, getTyVar, 
                          isTyVarTy, splitSigmaTy, tyVarsOfTypes
                        )
-import Subst           ( mkTopTyVarSubst, substClasses )
+import Subst           ( mkTopTyVarSubst, substClasses, substTy )
 import PprType         ( pprClassPred )
 import TysWiredIn      ( unitTy )
 import VarSet
@@ -409,18 +408,48 @@ inferLoop doc tau_tvs wanteds
        try_me inst     
          | isFree qtvs inst  = Free
          | isClassDict inst  = DontReduceUnlessConstant        -- Dicts
-         | otherwise         = ReduceMe AddToIrreds            -- Lits and Methods
+         | otherwise         = ReduceMe                        -- Lits and Methods
     in
                -- Step 2
     reduceContext doc try_me [] wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
        
                -- Step 3
     if no_improvement then
-           returnTc (varSetElems qtvs, frees, binds, irreds)
+       returnTc (varSetElems qtvs, frees, binds, irreds)
     else
-           inferLoop doc tau_tvs wanteds
+       -- If improvement did some unification, we go round again.  There
+       -- are two subtleties:
+       --   a) We start again with irreds, not wanteds
+       --      Using an instance decl might have introduced a fresh type variable
+       --      which might have been unified, so we'd get an infinite loop
+       --      if we started again with wanteds!  See example [LOOP]
+       --
+       --   b) It's also essential to re-process frees, because unification
+       --      might mean that a type variable that looked free isn't now.
+       --
+       -- Hence the (irreds ++ frees)
+
+       inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
+       returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}     
 
+Example [LOOP]
+
+       class If b t e r | b t e -> r
+       instance If T t e t
+       instance If F t e e
+       class Lte a b c | a b -> c where lte :: a -> b -> c
+       instance Lte Z b T
+       instance (Lte a b l,If l b a c) => Max a b c
+
+Wanted:        Max Z (S x) y
+
+Then we'll reduce using the Max instance to:
+       (Lte Z (S x) l, If l (S x) Z y)
+and improve by binding l->T, after which we can do some reduction 
+on both the Lte and If constraints.  What we *can't* do is start again
+with (Max Z (S x) y)!
+
 \begin{code}
 isFree qtvs inst
   =  not (tyVarsOfInst inst `intersectsVarSet` qtvs)   -- Constrains no quantified vars
@@ -436,7 +465,7 @@ isFree qtvs inst
 %************************************************************************
 
 @tcSimplifyCheck@ is used when we know exactly the set of variables
-we are going to quantify over.
+we are going to quantify over.  For example, a class or instance declaration.
 
 \begin{code}
 tcSimplifyCheck
@@ -465,16 +494,17 @@ checkLoop doc qtvs givens wanteds
              -- When checking against a given signature we always reduce
              -- until we find a match against something given, or can't reduce
        try_me inst | isFree qtvs' inst  = Free
-                   | otherwise          = ReduceMe AddToIrreds
+                   | otherwise          = ReduceMe 
     in
                -- Step 2
     reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
        
                -- Step 3
     if no_improvement then
-           returnTc (frees, binds, irreds)
+       returnTc (frees, binds, irreds)
     else
-           checkLoop doc qtvs givens wanteds
+       checkLoop doc qtvs givens' (irreds ++ frees)    `thenTc` \ (frees1, binds1, irreds1) ->
+       returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
 
 complainCheck doc givens irreds
   = mapNF_Tc zonkInst given_dicts                      `thenNF_Tc` \ givens' ->
@@ -496,6 +526,8 @@ complainCheck doc givens irreds
 
 @tcSimplifyInferCheck@ is used when we know the consraints we are to simplify
 against, but we don't know the type variables over which we are going to quantify.
+This happens when we have a type signature for a mutually recursive
+group.
 
 \begin{code}
 tcSimplifyInferCheck
@@ -541,20 +573,20 @@ inferCheckLoop doc tau_tvs givens wanteds
              -- When checking against a given signature we always reduce
              -- until we find a match against something given, or can't reduce
        try_me inst | isFree qtvs inst  = Free
-                   | otherwise         = ReduceMe AddToIrreds
+                   | otherwise         = ReduceMe 
     in
                -- Step 2
     reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
        
                -- Step 3
     if no_improvement then
-           returnTc (varSetElems qtvs, frees, binds, irreds)
+       returnTc (varSetElems qtvs, frees, binds, irreds)
     else
-           inferCheckLoop doc tau_tvs givens wanteds
+       inferCheckLoop doc tau_tvs givens' (irreds ++ frees)    `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
+       returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}
 
 
-
 %************************************************************************
 %*                                                                     *
 \subsection{tcSimplifyToDicts}
@@ -582,6 +614,24 @@ and we want to end up with
 But that means that we must simplify the Method for f to (f Int dNumInt)! 
 So tcSimplifyToDicts squeezes out all Methods.
 
+IMPORTANT NOTE:  we *don't* want to do superclass commoning up.  Consider
+
+       fromIntegral :: (Integral a, Num b) => a -> b
+       {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
+
+Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont* 
+want to get
+
+       forall dIntegralInt.
+       fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
+
+because the scsel will mess up matching.  Instead we want
+
+       forall dIntegralInt, dNumInt.
+       fromIntegral Int Int dIntegralInt dNumInt = id Int
+
+Hence "DontReduce NoSCs"
+
 \begin{code}
 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
 tcSimplifyToDicts wanted_lie
@@ -596,8 +646,8 @@ tcSimplifyToDicts wanted_lie
     wanteds = lieToList wanted_lie
 
        -- Reduce methods and lits only; stop as soon as we get a dictionary
-    try_me inst        | isDict inst = DontReduce
-               | otherwise   = ReduceMe AddToIrreds
+    try_me inst        | isDict inst = DontReduce NoSCs
+               | otherwise   = ReduceMe
 \end{code}
 
 
@@ -631,7 +681,7 @@ tcSimplifyIPs ip_names wanted_lie
     here_ip ip = isDict ip && ip `instMentionsIPs` ip_set
 
        -- Simplify any methods that mention the implicit parameter
-    try_me inst | inst `instMentionsIPs` ip_set = ReduceMe AddToIrreds
+    try_me inst | inst `instMentionsIPs` ip_set = ReduceMe
                | otherwise                     = Free
 \end{code}
 
@@ -684,7 +734,7 @@ bindInstsOfLocalFuns init_lie local_ids
                                                -- so it's worth building a set, so that 
                                                -- lookup (in isMethodFor) is faster
 
-    try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
+    try_me inst | isMethodFor overloaded_set inst = ReduceMe
                | otherwise                       = Free
 \end{code}
 
@@ -699,23 +749,22 @@ The main control over context reduction is here
 
 \begin{code}
 data WhatToDo 
- = ReduceMe              -- Try to reduce this
-       NoInstanceAction  -- What to do if there's no such instance
+ = ReduceMe            -- Try to reduce this
+                       -- If there's no instance, behave exactly like
+                       -- DontReduce: add the inst to 
+                       -- the irreductible ones, but don't 
+                       -- produce an error message of any kind.
+                       -- It might be quite legitimate such as (Eq a)!
 
- | DontReduce                  -- Return as irreducible 
+ | DontReduce WantSCs          -- Return as irreducible 
 
  | DontReduceUnlessConstant    -- Return as irreducible unless it can
                                -- be reduced to a constant in one step
 
  | Free                          -- Return as free
 
-data NoInstanceAction
-  = Stop               -- Fail; no error message
-                       -- (Only used when tautology checking.)
-
-  | AddToIrreds                -- Just add the inst to the irreductible ones; don't 
-                       -- produce an error message of any kind.
-                       -- It might be quite legitimate such as (Eq a)!
+data WantSCs = NoSCs | AddSCs  -- Tells whether we should add the superclasses
+                               -- of a predicate when adding it to the avails
 \end{code}
 
 
@@ -740,7 +789,8 @@ data Avail
        TcExpr          -- The RHS
        [Inst]          -- Insts free in the RHS; we need these too
 
-pprAvails avails = vcat (map pprAvail (eltsFM avails))
+pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
+                       | (inst,avail) <- fmToList avails ]
 
 instance Outputable Avail where
     ppr = pprAvail
@@ -784,15 +834,15 @@ bindsAndIrreds avails wanteds
                                -- For implicit parameters, all occurrences share the same
                                -- Id, so there is no need for synonym bindings
                               new_binds | new_id == id = binds
-                                        | otherwise    = binds `AndMonoBinds` new_bind
-                              new_bind = VarMonoBind new_id (HsVar id)
+                                        | otherwise    = addBind binds new_id (HsVar id)
                               new_id   = instToId w
 
-         Just (Rhs rhs ws') -> go avails' (binds `AndMonoBinds` new_bind) irreds (ws' ++ ws)
+         Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
                             where
                                id       = instToId w
                                avails'  = addToFM avails w (BoundTo id)
-                               new_bind = VarMonoBind id rhs
+
+addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
 \end{code}
 
 
@@ -822,7 +872,8 @@ simpleReduceLoop doc try_me wanteds
     if no_improvement then
        returnTc (frees, binds, irreds)
     else
-       simpleReduceLoop doc try_me wanteds
+       simpleReduceLoop doc try_me (irreds ++ frees)   `thenTc` \ (frees1, binds1, irreds1) ->
+       returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
 \end{code}     
 
 
@@ -839,7 +890,7 @@ reduceContext :: SDoc
 
 reduceContext doc try_me givens wanteds
   =
-{-    traceTc (text "reduceContext" <+> (vcat [
+    traceTc (text "reduceContext" <+> (vcat [
             text "----------------------",
             doc,
             text "given" <+> ppr givens,
@@ -847,7 +898,6 @@ reduceContext doc try_me givens wanteds
             text "----------------------"
             ]))                                        `thenNF_Tc_`
 
--}
         -- Build the Avail mapping from "givens"
     foldlNF_Tc addGiven (emptyFM, []) givens           `thenNF_Tc` \ init_state ->
 
@@ -858,7 +908,6 @@ reduceContext doc try_me givens wanteds
        -- In particular, avails includes all superclasses of everything
     tcImprove avails                                   `thenTc` \ no_improvement ->
 
-{-
     traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             doc,
@@ -870,7 +919,6 @@ reduceContext doc try_me givens wanteds
             text "no_improvement =" <+> ppr no_improvement,
             text "----------------------"
             ]))                                        `thenNF_Tc_`
--}
      let
        (binds, irreds) = bindsAndIrreds avails wanteds
      in
@@ -890,8 +938,14 @@ tcImprove avails
      if null eqns then
        returnTc True
      else
-        mapTc_ (\ (t1,t2) -> unifyTauTy t1 t2) eqns    `thenTc_`
+       traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns))    `thenNF_Tc_`
+        mapTc_ unify eqns      `thenTc_`
        returnTc False
+  where
+    unify (qtvs, t1, t2) = tcInstTyVars (varSetElems qtvs)     `thenNF_Tc` \ (_, _, tenv) ->
+                          unifyTauTy (substTy tenv t1) (substTy tenv t2)
+    ppr_eqn (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)) <+>
+                            ppr t1 <+> equals <+> ppr t2
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.
@@ -949,17 +1003,17 @@ reduce stack try_me wanted state
   | otherwise
   = case try_me wanted of {
 
-      DontReduce -> addIrred state wanted
+      DontReduce want_scs -> addIrred want_scs state 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
-       try_simple addIrred
+       try_simple (addIrred AddSCs)    -- Assume want superclasses
 
     ; Free ->  -- It's free so just chuck it upstairs
                -- First, see if the inst can be reduced to a constant in one step
        try_simple addFree
 
-    ; ReduceMe no_instance_action ->   -- It should be reduced
+    ; ReduceMe ->              -- It should be reduced
        lookupInst wanted             `thenNF_Tc` \ lookup_result ->
        case lookup_result of
            GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' -> 
@@ -967,9 +1021,8 @@ reduce stack try_me wanted state
            SimpleInst rhs       -> addWanted state wanted rhs []
 
            NoInstance ->    -- No such instance! 
-                   case no_instance_action of
-                       Stop        -> failTc           
-                       AddToIrreds -> addIrred state wanted
+                            -- Add it and its superclasses
+                            addIrred AddSCs state wanted
 
     }
   where
@@ -1046,32 +1099,33 @@ addWanted state@(avails, frees) wanted rhs_expr wanteds
          | otherwise                  = ASSERT( null wanteds ) NoRhs
 
 addGiven :: RedState -> Inst -> NF_TcM RedState
-addGiven state given = add_avail state given (BoundTo (instToId given))
+addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
 
-addIrred :: RedState -> Inst -> NF_TcM RedState
-addIrred state irred = add_avail state irred Irred
+addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
+addIrred NoSCs  (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
+addIrred AddSCs state         irred = addAvailAndSCs state irred Irred
 
-add_avail :: RedState -> Inst -> Avail -> NF_TcM RedState
-add_avail (avails, frees) wanted avail
-  = addAvail avails wanted avail       `thenNF_Tc` \ avails' ->
+addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
+addAvailAndSCs (avails, frees) wanted avail
+  = add_avail_and_scs avails wanted avail      `thenNF_Tc` \ avails' ->
     returnNF_Tc (avails', frees)
 
 ---------------------
-addAvail :: Avails -> Inst -> Avail -> NF_TcM Avails
-addAvail avails wanted avail
-  = addSuperClasses (addToFM avails wanted avail) wanted
+add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
+add_avail_and_scs avails wanted avail
+  = add_scs (addToFM avails wanted avail) wanted
 
-addSuperClasses :: Avails -> Inst -> NF_TcM Avails
+add_scs :: Avails -> Inst -> NF_TcM Avails
        -- Add all the superclasses of the Inst to Avails
        -- Invariant: the Inst is already in Avails.
 
-addSuperClasses avails dict
+add_scs avails dict
   | not (isClassDict dict)
   = returnNF_Tc avails
 
   | otherwise  -- It is a dictionary
   = newDictsFromOld dict sc_theta'     `thenNF_Tc` \ sc_dicts ->
-    foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_dicts sc_sels)
+    foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
@@ -1080,7 +1134,7 @@ addSuperClasses avails dict
     add_sc avails (sc_dict, sc_sel)    -- Add it, and its superclasses
       = case lookupFM avails sc_dict of
          Just (BoundTo _) -> returnNF_Tc avails        -- See Note [SUPER] below
-         other            -> addAvail avails sc_dict avail
+         other            -> add_avail_and_scs avails sc_dict avail
       where
        sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
        avail      = Rhs sc_sel_rhs [dict]
@@ -1168,12 +1222,16 @@ tcSimplifyTop wanted_lie
     mapTc disambigGroup std_oks                `thenTc` \ binds_ambig ->
 
        -- And complain about the ones that don't
+       -- This group includes both non-existent instances 
+       --      e.g. Num (IO a) and Eq (Int -> Int)
+       -- and ambiguous dictionaries
+       --      e.g. Num a
     addTopAmbigErrs bad_guys           `thenNF_Tc_`
 
     returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
   where
     wanteds    = lieToList wanted_lie
-    try_me inst        = ReduceMe AddToIrreds
+    try_me inst        = ReduceMe
 
     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
@@ -1227,7 +1285,8 @@ disambigGroup dicts
     in
        -- See if any default works, and if so bind the type variable to it
        -- If not, add an AmbigErr
-    recoverTc (addAmbigErrs dicts `thenNF_Tc_` returnTc EmptyMonoBinds)        $
+    recoverTc (addAmbigErrs dicts                      `thenNF_Tc_` 
+              returnTc EmptyMonoBinds) $
 
     try_default default_tys                    `thenTc` \ chosen_default_ty ->
 
@@ -1250,7 +1309,7 @@ disambigGroup dicts
     returnTc EmptyMonoBinds
 
   where
-    try_me inst = ReduceMe AddToIrreds         -- This reduce should not fail
+    try_me inst = ReduceMe                     -- This reduce should not fail
     tyvar       = get_tv (head dicts)          -- Should be non-empty
     classes     = map get_clas dicts
 \end{code}
@@ -1431,7 +1490,8 @@ addTopAmbigErrs dicts
     fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
     (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
     complain d | not (null (getIPs d))               = addTopIPErr tidy_env d
-              | tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
+              | not (isTyVarDict d) ||
+                tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
               | otherwise                            = addAmbigErr tidy_env d
 
 addTopIPErr tidy_env tidy_dict