Fix Trac #2985: generating superclasses and recursive dictionaries

[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index ee62c0e..071d4c0 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -6,13 +6,6 @@
 TcSimplify
 
 \begin{code}
 TcSimplify
 
 \begin{code}

-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-

 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,

@@ -23,6 +16,8 @@ module TcSimplify (
 
        tcSimplifyDeriv, tcSimplifyDefault,
        bindInstsOfLocalFuns, 
 
        tcSimplifyDeriv, tcSimplifyDefault,
        bindInstsOfLocalFuns, 

+       
+        tcSimplifyStagedExpr,

 
         misMatchMsg
     ) where
 
         misMatchMsg
     ) where

@@ -33,6 +28,7 @@ import {-# SOURCE #-} TcUnify( unifyType )
 import HsSyn
 
 import TcRnMonad
 import HsSyn
 
 import TcRnMonad

+import TcHsSyn ( hsLPatType )

 import Inst
 import TcEnv
 import InstEnv
 import Inst
 import TcEnv
 import InstEnv

@@ -40,8 +36,9 @@ import TcType
 import TcMType
 import TcIface
 import TcTyFuns
 import TcMType
 import TcIface
 import TcTyFuns

-import TypeRep
+import DsUtils -- Big-tuple functions

 import Var
 import Var

+import Id

 import Name
 import NameSet
 import Class
 import Name
 import NameSet
 import Class

@@ -54,14 +51,12 @@ import ErrUtils
 import BasicTypes
 import VarSet
 import VarEnv
 import BasicTypes
 import VarSet
 import VarEnv

-import Module

 import FiniteMap
 import Bag
 import Outputable
 import Maybes
 import ListSetOps
 import Util
 import FiniteMap
 import Bag
 import Outputable
 import Maybes
 import ListSetOps
 import Util

-import UniqSet

 import SrcLoc
 import DynFlags
 import FastString
 import SrcLoc
 import DynFlags
 import FastString

@@ -99,34 +94,36 @@ we reduce the (C a b1) constraint from the call of f to (D a b1).
 
 Here is a more complicated example:
 
 
 Here is a more complicated example:
 

-| > class Foo a b | a->b
-| >
-| > class Bar a b | a->b
-| >
-| > data Obj = Obj
-| >
-| > instance Bar Obj Obj
-| >
-| > instance (Bar a b) => Foo a b
-| >
-| > foo:: (Foo a b) => a -> String
-| > foo _ = "works"
-| >
-| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
-| > runFoo f = f Obj
-| 
-| *Test> runFoo foo
-| 
-| <interactive>:1:
-|     Could not deduce (Bar a b) from the context (Foo a b)
-|       arising from use of `foo' at <interactive>:1
-|     Probable fix:
-|         Add (Bar a b) to the expected type of an expression
-|     In the first argument of `runFoo', namely `foo'
-|     In the definition of `it': it = runFoo foo
-| 
-| Why all of the sudden does GHC need the constraint Bar a b? The
-| function foo didn't ask for that... 
+@
+  > class Foo a b | a->b
+  >
+  > class Bar a b | a->b
+  >
+  > data Obj = Obj
+  >
+  > instance Bar Obj Obj
+  >
+  > instance (Bar a b) => Foo a b
+  >
+  > foo:: (Foo a b) => a -> String
+  > foo _ = "works"
+  >
+  > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
+  > runFoo f = f Obj
+
+  *Test> runFoo foo
+
+  <interactive>:1:
+      Could not deduce (Bar a b) from the context (Foo a b)
+        arising from use of `foo' at <interactive>:1
+      Probable fix:
+          Add (Bar a b) to the expected type of an expression
+      In the first argument of `runFoo', namely `foo'
+      In the definition of `it': it = runFoo foo
+
+  Why all of the sudden does GHC need the constraint Bar a b? The
+  function foo didn't ask for that...
+@

 
 The trouble is that to type (runFoo foo), GHC has to solve the problem:
 
 
 The trouble is that to type (runFoo foo), GHC has to solve the problem:
 

@@ -867,7 +864,7 @@ Note [NO TYVARS]
 
 The excitement comes when simplifying the bindings for h.  Initially
 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
 
 The excitement comes when simplifying the bindings for h.  Initially
 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.

-From this we get t1:=:t2, but also various bindings.  We can't forget
+From this we get t1~t2, but also various bindings.  We can't forget

 the bindings (because of [LOOP]), but in fact t1 is what g is
 polymorphic in.  
 
 the bindings (because of [LOOP]), but in fact t1 is what g is
 polymorphic in.  
 

@@ -889,7 +886,9 @@ isFreeWhenChecking qtvs ips inst
   && isFreeWrtIPs    ips inst
 -}
 
   && isFreeWrtIPs    ips inst
 -}
 

+isFreeWrtTyVars :: VarSet -> Inst -> Bool

 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs

+isFreeWrtIPs :: NameSet -> Inst -> Bool

 isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
 \end{code}
 
 isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
 \end{code}
 

@@ -975,17 +974,17 @@ makeImplicationBind :: InstLoc -> [TcTyVar]
                    -> [Inst] -> [Inst]
                    -> TcM ([Inst], TcDictBinds)
 -- Make a binding that binds 'irreds', by generating an implication
                    -> [Inst] -> [Inst]
                    -> TcM ([Inst], TcDictBinds)
 -- Make a binding that binds 'irreds', by generating an implication

--- constraint for them, *and* throwing the constraint into the LIE
+-- constraint for them.
+--

 -- The binding looks like
 --     (ir1, .., irn) = f qtvs givens
 -- where f is (evidence for) the new implication constraint
 -- The binding looks like
 --     (ir1, .., irn) = f qtvs givens
 -- where f is (evidence for) the new implication constraint

---     f :: forall qtvs. {reft} givens => (ir1, .., irn)
+--     f :: forall qtvs. givens => (ir1, .., irn)

 -- qtvs includes coercion variables
 --
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs
 -- qtvs includes coercion variables
 --
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs

-                   givens      -- Guaranteed all Dicts
-                               -- or EqInsts
+                   givens      -- Guaranteed all Dicts or EqInsts

                    irreds
  | null irreds                 -- If there are no irreds, we are done
  = return ([], emptyBag)
                    irreds
  | null irreds                 -- If there are no irreds, we are done
  = return ([], emptyBag)

@@ -993,30 +992,38 @@ makeImplicationBind loc all_tvs
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
        ; let (eq_givens, dict_givens) = partition isEqInst givens
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
        ; let (eq_givens, dict_givens) = partition isEqInst givens

-             eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens)
-               -- Urgh! See line 2187 or thereabouts.  I believe that all these
-               -- 'givens' must be a simple CoVar.  This MUST be cleaned up.

 
 

-       ; let name = mkInternalName uniq (mkVarOcc "ic") span
+                -- extract equality binders
+              eq_cotvs = map eqInstType eq_givens
+
+                -- make the implication constraint instance
+             name = mkInternalName uniq (mkVarOcc "ic") span

              implic_inst = ImplicInst { tci_name = name,
                                         tci_tyvars = all_tvs, 
              implic_inst = ImplicInst { tci_name = name,
                                         tci_tyvars = all_tvs, 

-                                        tci_given = (eq_givens ++ dict_givens),
-                                        tci_wanted = irreds, tci_loc = loc }
-       ; let   -- only create binder for dict_irreds
-             (eq_irreds, dict_irreds) = partition isEqInst irreds
-              n_dict_irreds = length dict_irreds
+                                        tci_given = eq_givens ++ dict_givens,
+                                                       -- same order as binders
+                                        tci_wanted = irreds, 
+                                         tci_loc = loc }
+
+               -- create binders for the irreducible dictionaries
+             dict_irreds    = filter (not . isEqInst) irreds

              dict_irred_ids = map instToId dict_irreds
              dict_irred_ids = map instToId dict_irreds

-             tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
-             pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
-             rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
-             co  = mkWpApps (map instToId dict_givens)
-                   <.> mkWpTyApps eq_tyvar_cos
-                   <.> mkWpTyApps (mkTyVarTys all_tvs)
-             bind | [dict_irred_id] <- dict_irred_ids  = VarBind dict_irred_id rhs
-                  | otherwise        = PatBind { pat_lhs = L span pat, 
-                                                 pat_rhs = unguardedGRHSs rhs, 
-                                                 pat_rhs_ty = tup_ty,
-                                                 bind_fvs = placeHolderNames }
+             lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
+
+                -- create the binding
+             rhs  = L span (mkHsWrap co (HsVar (instToId implic_inst)))
+             co   =     mkWpApps (map instToId dict_givens)
+                    <.> mkWpTyApps eq_cotvs
+                    <.> mkWpTyApps (mkTyVarTys all_tvs)
+             bind | [dict_irred_id] <- dict_irred_ids  
+                   = VarBind dict_irred_id rhs
+                  | otherwise        
+                   = PatBind { pat_lhs = lpat
+                            , pat_rhs = unguardedGRHSs rhs 
+                            , pat_rhs_ty = hsLPatType lpat
+                            , bind_fvs = placeHolderNames 
+                             }
+

        ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
        ; return ([implic_inst], unitBag (L span bind)) 
         }
        ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
        ; return ([implic_inst], unitBag (L span bind)) 
         }

@@ -1027,11 +1034,11 @@ tryHardCheckLoop :: SDoc
             -> TcM ([Inst], TcDictBinds)
 
 tryHardCheckLoop doc wanteds
             -> TcM ([Inst], TcDictBinds)
 
 tryHardCheckLoop doc wanteds

-  = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds
+  = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds

        ; return (irreds,binds)
        }
   where
        ; return (irreds,binds)
        }
   where

-    try_me inst = ReduceMe AddSCs
+    try_me _ = ReduceMe

        -- Here's the try-hard bit
 
 -----------------------------------------------------------
        -- Here's the try-hard bit
 
 -----------------------------------------------------------

@@ -1047,7 +1054,7 @@ gentleCheckLoop inst_loc givens wanteds
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 

-    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+    try_me inst | isMethodOrLit inst = ReduceMe

                | otherwise          = Stop
        -- When checking against a given signature 
        -- we MUST be very gentle: Note [Check gently]
                | otherwise          = Stop
        -- When checking against a given signature 
        -- we MUST be very gentle: Note [Check gently]

@@ -1058,8 +1065,8 @@ gentleInferLoop doc wanteds
   = do         { (irreds, binds) <- checkLoop env wanteds
        ; return (irreds, binds) }
   where
   = do         { (irreds, binds) <- checkLoop env wanteds
        ; return (irreds, binds) }
   where

-    env = mkRedEnv doc try_me []
-    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+    env = mkInferRedEnv doc try_me
+    try_me inst | isMethodOrLit inst = ReduceMe

                | otherwise          = Stop
 \end{code}
 
                | otherwise          = Stop
 \end{code}
 

@@ -1096,18 +1103,16 @@ checkLoop :: RedEnv
 -- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds
 -- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds

-  = go env wanteds (return ())
-  where go env wanteds elim_skolems
+  = go env wanteds
+  where go env wanteds

          = do  {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
                 ; env'     <- zonkRedEnv env
                ; wanteds' <- zonkInsts  wanteds
        
          = do  {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
                 ; env'     <- zonkRedEnv env
                ; wanteds' <- zonkInsts  wanteds
        

-               ; (improved, binds, irreds, elim_more_skolems)
-                    <- reduceContext env' wanteds'
-                ; let elim_skolems' = elim_skolems >> elim_more_skolems
+               ; (improved, binds, irreds) <- reduceContext env' wanteds'

 
 

-               ; if not improved then
-                   elim_skolems' >> return (irreds, binds)
+               ; if null irreds || not improved then
+                   return (irreds, binds)

                  else do
        
                -- If improvement did some unification, we go round again.
                  else do
        
                -- If improvement did some unification, we go round again.

@@ -1116,7 +1121,7 @@ checkLoop env wanteds
                -- variable which might have been unified, so we'd get an 
                 -- infinite loop if we started again with wanteds!  
                 -- See Note [LOOP]
                -- variable which might have been unified, so we'd get an 
                 -- infinite loop if we started again with wanteds!  
                 -- See Note [LOOP]

-               { (irreds1, binds1) <- go env' irreds elim_skolems'
+               { (irreds1, binds1) <- go env' irreds

                ; return (irreds1, binds `unionBags` binds1) } }
 \end{code}
 
                ; return (irreds1, binds `unionBags` binds1) } }
 \end{code}
 

@@ -1209,30 +1214,104 @@ Alas!  Alack! We can do the same for (instance D Int):
        ds2 = $p1 dc
 
 And now we've defined the superclass in terms of itself.
        ds2 = $p1 dc
 
 And now we've defined the superclass in terms of itself.

-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-

 Two more nasty cases are in
        tcrun021
        tcrun033
 
 Two more nasty cases are in
        tcrun021
        tcrun033
 

+Solution: 
+  - Satisfy the superclass context *all by itself* 
+    (tcSimplifySuperClasses)
+  - And do so completely; i.e. no left-over constraints
+    to mix with the constraints arising from method declarations
+
+
+Note [Recursive instances and superclases]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this code, which arises in the context of "Scrap Your 
+Boilerplate with Class".  
+
+    class Sat a
+    class Data ctx a
+    instance  Sat (ctx Char)             => Data ctx Char
+    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
+
+    class Data Maybe a => Foo a
+
+    instance Foo t => Sat (Maybe t)
+
+    instance Data Maybe a => Foo a
+    instance Foo a        => Foo [a]
+    instance                 Foo [Char]
+
+In the instance for Foo [a], when generating evidence for the superclasses
+(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
+Using the instance for Data, we therefore need
+        (Sat (Maybe [a], Data Maybe a)
+But we are given (Foo a), and hence its superclass (Data Maybe a).
+So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
+we need (Foo [a]).  And that is the very dictionary we are bulding
+an instance for!  So we must put that in the "givens".  So in this
+case we have
+       Given:  Foo a, Foo [a]
+       Watend: Data Maybe [a]
+
+BUT we must *not not not* put the *superclasses* of (Foo [a]) in
+the givens, which is what 'addGiven' would normally do. Why? Because
+(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted 
+by selecting a superclass from Foo [a], which simply makes a loop.
+
+On the other hand we *must* put the superclasses of (Foo a) in
+the givens, as you can see from the derivation described above.
+
+Conclusion: in the very special case of tcSimplifySuperClasses
+we have one 'given' (namely the "this" dictionary) whose superclasses
+must not be added to 'givens' by addGiven.  
+
+There is a complication though.  Suppose there are equalities
+      instance (Eq a, a~b) => Num (a,b)
+Then we normalise the 'givens' wrt the equalities, so the original
+given "this" dictionary is cast to one of a different type.  So it's a
+bit trickier than before to identify the "special" dictionary whose
+superclasses must not be added. See test
+   indexed-types/should_run/EqInInstance
+
+We need a persistent property of the dictionary to record this
+special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
+but cool), which is maintained by dictionary normalisation.
+Specifically, the InstLocOrigin is
+            NoScOrigin
+then the no-superclass thing kicks in.  WATCH OUT if you fiddle
+with InstLocOrigin!
+

 \begin{code}
 \begin{code}

-tcSimplifySuperClasses 
+tcSimplifySuperClasses

        :: InstLoc 
        :: InstLoc 

+       -> Inst         -- The dict whose superclasses 
+                       -- are being figured out

        -> [Inst]       -- Given 
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds
        -> [Inst]       -- Given 
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds

-tcSimplifySuperClasses loc givens sc_wanteds
+tcSimplifySuperClasses loc this givens sc_wanteds

   = do { traceTc (text "tcSimplifySuperClasses")
   = do { traceTc (text "tcSimplifySuperClasses")

+
+             -- Note [Recursive instances and superclases]
+        ; no_sc_loc <- getInstLoc NoScOrigin
+       ; let no_sc_this = setInstLoc this no_sc_loc
+
+       ; let env =  RedEnv { red_doc = pprInstLoc loc, 
+                             red_try_me = try_me,
+                             red_givens = no_sc_this : givens, 
+                             red_stack = (0,[]),
+                             red_improve = False }  -- No unification vars
+
+

        ; (irreds,binds1) <- checkLoop env sc_wanteds
        ; let (tidy_env, tidy_irreds) = tidyInsts irreds
        ; (irreds,binds1) <- checkLoop env sc_wanteds
        ; let (tidy_env, tidy_irreds) = tidyInsts irreds

-       ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
+       ; reportNoInstances tidy_env (Just (loc, givens)) [] tidy_irreds

        ; return binds1 }
   where
        ; return binds1 }
   where

-    env = mkRedEnv (pprInstLoc loc) try_me givens
-    try_me inst = ReduceMe NoSCs
-       -- Like tryHardCheckLoop, but with NoSCs
+    try_me _ = ReduceMe  -- Try hard, so we completely solve the superclass 
+                        -- constraints right here. See Note [SUPERCLASS-LOOP 1]

 \end{code}
 
 
 \end{code}
 
 

@@ -1353,7 +1432,7 @@ tcSimplifyRestricted      -- Used for restricted binding groups
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Zonk everything in sight
   = do { traceTc (text "tcSimplifyRestricted")
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Zonk everything in sight
   = do { traceTc (text "tcSimplifyRestricted")

-       ; wanteds' <- zonkInsts wanteds
+       ; wanteds_z <- zonkInsts wanteds

 
        -- 'ReduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type
 
        -- 'ReduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type

@@ -1364,10 +1443,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- BUT do no improvement!  See Plan D above
        -- HOWEVER, some unification may take place, if we instantiate
        --          a method Inst with an equality constraint
        -- BUT do no improvement!  See Plan D above
        -- HOWEVER, some unification may take place, if we instantiate
        --          a method Inst with an equality constraint

-       ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
-       ; (_imp, _binds, constrained_dicts, elim_skolems) 
-            <- reduceContext env wanteds'
-        ; elim_skolems
+       ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
+       ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds_z

 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)

@@ -1395,6 +1472,13 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
                ppr _binds,
                ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
 
                ppr _binds,
                ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
 

+          -- Zonk wanteds again!  The first call to reduceContext may have
+          -- instantiated some variables. 
+          -- FIXME: If red_improve would work, we could propagate that into
+          --        the equality solver, too, to prevent instantating any
+          --        variables.
+       ; wanteds_zz <- zonkInsts wanteds_z
+

        -- The first step may have squashed more methods than
        -- necessary, so try again, this time more gently, knowing the exact
        -- set of type variables to quantify over.
        -- The first step may have squashed more methods than
        -- necessary, so try again, this time more gently, knowing the exact
        -- set of type variables to quantify over.

@@ -1414,10 +1498,9 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        ; let is_nested_group = isNotTopLevel top_lvl
              try_me inst | isFreeWrtTyVars qtvs inst,
                           (is_nested_group || isDict inst) = Stop
        ; let is_nested_group = isNotTopLevel top_lvl
              try_me inst | isFreeWrtTyVars qtvs inst,
                           (is_nested_group || isDict inst) = Stop

-                         | otherwise            = ReduceMe AddSCs
+                         | otherwise                       = ReduceMe 

              env = mkNoImproveRedEnv doc try_me
              env = mkNoImproveRedEnv doc try_me

-       ; (_imp, binds, irreds, elim_skolems) <- reduceContext env wanteds'
-        ; elim_skolems
+       ; (_imp, binds, irreds) <- reduceContext env wanteds_zz

 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured

@@ -1490,27 +1573,55 @@ Instead we want to quantify over the dictionaries separately.
 
 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
 all dicts unchanged, with absolutely no sharing.  It's simpler to do this
 
 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
 all dicts unchanged, with absolutely no sharing.  It's simpler to do this

-from scratch, rather than further parameterise simpleReduceLoop etc
+from scratch, rather than further parameterise simpleReduceLoop etc.
+Simpler, maybe, but alas not simple (see Trac #2494)
+
+* Type errors may give rise to an (unsatisfiable) equality constraint
+
+* Applications of a higher-rank function on the LHS may give
+  rise to an implication constraint, esp if there are unsatisfiable
+  equality constraints inside.

 
 \begin{code}
 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
 tcSimplifyRuleLhs wanteds
 
 \begin{code}
 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
 tcSimplifyRuleLhs wanteds

-  = go [] emptyBag wanteds
+  = do { wanteds' <- zonkInsts wanteds
+       ; (irreds, binds) <- go [] emptyBag wanteds'
+       ; let (dicts, bad_irreds) = partition isDict irreds
+       ; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds)
+       ; addNoInstanceErrs (nub bad_irreds)
+               -- The nub removes duplicates, which has
+               -- not happened otherwise (see notes above)
+       ; return (dicts, binds) }

   where
   where

-    go dicts binds []
-       = return (dicts, binds)
-    go dicts binds (w:ws)
+    go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds)
+    go irreds binds []
+       = return (irreds, binds)
+    go irreds binds (w:ws)

        | isDict w
        | isDict w

-       = go (w:dicts) binds ws
+       = go (w:irreds) binds ws
+       | isImplicInst w        -- Have a go at reducing the implication
+       = do { (binds1, irreds1) <- reduceImplication red_env w
+            ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1
+            ; go (bad_irreds ++ irreds) 
+                 (binds `unionBags` binds1) 
+                 (ok_irreds ++ ws)}

        | otherwise
        = do { w' <- zonkInst w  -- So that (3::Int) does not generate a call
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of
        | otherwise
        = do { w' <- zonkInst w  -- So that (3::Int) does not generate a call
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of

-                GenInst ws' rhs -> 
-                   go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
-                NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
+                NoInstance      -> go (w:irreds) binds ws
+                GenInst ws' rhs -> go irreds binds' (ws' ++ ws)
+                       where
+                         binds' = addInstToDictBind binds w rhs

          }
          }

+
+       -- Sigh: we need to reduce inside implications
+    red_env = mkInferRedEnv doc try_me
+    doc = ptext (sLit "Implication constraint in RULE lhs")
+    try_me inst | isMethodOrLit inst = ReduceMe
+               | otherwise          = Stop     -- Be gentle

 \end{code}
 
 tcSimplifyBracket is used when simplifying the constraints arising from
 \end{code}
 
 tcSimplifyBracket is used when simplifying the constraints arising from

@@ -1566,15 +1677,22 @@ tcSimplifyIPs given_ips wanteds
                -- Unusually for checking, we *must* zonk the given_ips
 
        ; let env = mkRedEnv doc try_me given_ips'
                -- Unusually for checking, we *must* zonk the given_ips
 
        ; let env = mkRedEnv doc try_me given_ips'

-       ; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds'
-        ; elim_skolems
+       ; (improved, binds, irreds) <- reduceContext env wanteds'

 
 

-       ; if not improved then 
+       ; if null irreds || not improved then 

                ASSERT( all is_free irreds )
                do { extendLIEs irreds
                   ; return binds }
                ASSERT( all is_free irreds )
                do { extendLIEs irreds
                   ; return binds }

-         else
-               tcSimplifyIPs given_ips wanteds }
+         else do
+        -- If improvement did some unification, we go round again.
+        -- 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 Note [LOOP]
+        { binds1 <- tcSimplifyIPs given_ips' irreds
+        ; return $ binds `unionBags` binds1
+        } }

   where
     doc           = text "tcSimplifyIPs" <+> ppr given_ips
     ip_set = mkNameSet (ipNamesOfInsts given_ips)
   where
     doc           = text "tcSimplifyIPs" <+> ppr given_ips
     ip_set = mkNameSet (ipNamesOfInsts given_ips)

@@ -1582,7 +1700,7 @@ tcSimplifyIPs given_ips wanteds
 
        -- Simplify any methods that mention the implicit parameter
     try_me inst | is_free inst = Stop
 
        -- Simplify any methods that mention the implicit parameter
     try_me inst | is_free inst = Stop

-               | otherwise    = ReduceMe NoSCs
+               | otherwise    = ReduceMe

 \end{code}
 
 
 \end{code}
 
 

@@ -1657,8 +1775,9 @@ data RedEnv
           , red_try_me :: Inst -> WhatToDo
           , red_improve :: Bool                -- True <=> do improvement
           , red_givens :: [Inst]               -- All guaranteed rigid
           , red_try_me :: Inst -> WhatToDo
           , red_improve :: Bool                -- True <=> do improvement
           , red_givens :: [Inst]               -- All guaranteed rigid

-                                               -- Always dicts
+                                               -- Always dicts & equalities

                                                -- but see Note [Rigidity]
                                                -- but see Note [Rigidity]

+ 

           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }

@@ -1684,6 +1803,14 @@ mkRedEnv doc try_me givens
             red_stack = (0,[]),
             red_improve = True }       
 
             red_stack = (0,[]),
             red_improve = True }       
 

+mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
+-- No givens at all
+mkInferRedEnv doc try_me
+  = RedEnv { red_doc = doc, red_try_me = try_me,
+            red_givens = [], 
+            red_stack = (0,[]),
+            red_improve = True }       
+

 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 -- Do not do improvement; no givens
 mkNoImproveRedEnv doc try_me
 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 -- Do not do improvement; no givens
 mkNoImproveRedEnv doc try_me

@@ -1693,11 +1820,11 @@ mkNoImproveRedEnv doc try_me
             red_improve = True }       
 
 data WhatToDo
             red_improve = True }       
 
 data WhatToDo

- = ReduceMe WantSCs    -- Try to reduce this
-                       -- If there's no instance, 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)!
+ = ReduceMe    -- Try to reduce this
+               -- If there's no instance, 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)!

 
  | Stop                -- Return as irreducible unless it can
                        -- be reduced to a constant in one step
 
  | Stop                -- Return as irreducible unless it can
                        -- be reduced to a constant in one step

@@ -1740,110 +1867,102 @@ reduceContext :: RedEnv
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings

-                     [Inst],           -- Irreducible
-                      TcM ())           -- Undo skolems from SkolemOccurs
+                     [Inst])           -- Irreducible

 
 

-reduceContext env wanteds
+reduceContext env wanteds0

   = do { traceTc (text "reduceContext" <+> (vcat [
             text "----------------------",
             red_doc env,
             text "given" <+> ppr (red_givens env),
   = do { traceTc (text "reduceContext" <+> (vcat [
             text "----------------------",
             red_doc env,
             text "given" <+> ppr (red_givens env),

-            text "wanted" <+> ppr wanteds,
+            text "wanted" <+> ppr wanteds0,

             text "----------------------"
             ]))
 
             text "----------------------"
             ]))
 

-
-       ; let givens                       = red_givens env
-             (given_eqs0, given_dicts0)   = partition isEqInst givens
-             (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds
-             (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs
-

           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
           -- See Note [Ancestor Equalities]
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
           -- See Note [Ancestor Equalities]

-       ; ancestor_eqs <- ancestorEqualities wanted_dicts
-        ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
+       ; ancestor_eqs <- ancestorEqualities wanteds0

        ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 
        ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 

-         -- 1. Normalise the *given* *equality* constraints
-       ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
-
-         -- 2. Normalise the *given* *dictionary* constraints
-         --    wrt. the toplevel and given equations
-       ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
-                                                            given_dicts0
-
-          -- 5. Build the Avail mapping from "given_dicts"
-       ; (init_state, extra_givens) <- getLIE $ do 
-               { init_state <- foldlM addGiven emptyAvails given_dicts
+          -- Normalise and solve all equality constraints as far as possible
+          -- and normalise all dictionary constraints wrt to the reduced
+          -- equalities.  The returned wanted constraints include the
+          -- irreducible wanted equalities.
+        ; let wanteds = wanteds0 ++ ancestor_eqs
+              givens  = red_givens env
+        ; (givens', 
+           wanteds', 
+           normalise_binds,
+           eq_improved)     <- tcReduceEqs givens wanteds
+       ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
+                     [ppr givens', ppr wanteds', ppr normalise_binds]
+
+          -- Build the Avail mapping from "given_dicts"
+       ; (init_state, _) <- getLIE $ do 
+               { init_state <- foldlM addGiven emptyAvails givens'

                ; return init_state
                 }
 
                ; return init_state
                 }
 

-       -- *** ToDo: what to do with the "extra_givens"?  For the
-       -- moment I'm simply discarding them, which is probably wrong
-
-          -- 6. Solve the *wanted* *dictionary* constraints (not implications)
-         --    This may expose some further equational constraints...
+          -- Solve the *wanted* *dictionary* constraints (not implications)
+         -- This may expose some further equational constraints in the course
+          -- of improvement due to functional dependencies if any of the
+          -- involved unifications gets deferred.
+       ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'

        ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
        ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)

-       ; (dict_binds, bound_dicts, dict_irreds) 
-            <- extractResults avails wanted_dicts
-       ; traceTc $ text "reduceContext extractresults" <+> vcat
+                  -- The getLIE is reqd because reduceList does improvement
+                  -- (via extendAvails) which may in turn do unification
+       ; (dict_binds, 
+           bound_dicts, 
+           dict_irreds)       <- extractResults avails wanted_dicts
+       ; traceTc $ text "reduceContext: extractResults" <+> vcat

                      [ppr avails, ppr wanted_dicts, ppr dict_binds]
 
          -- Solve the wanted *implications*.  In doing so, we can provide
          -- as "given"   all the dicts that were originally given, 
          --              *or* for which we now have bindings, 
          --              *or* which are now irreds
                      [ppr avails, ppr wanted_dicts, ppr dict_binds]
 
          -- Solve the wanted *implications*.  In doing so, we can provide
          -- as "given"   all the dicts that were originally given, 
          --              *or* for which we now have bindings, 
          --              *or* which are now irreds

-       ; let implic_env = env { red_givens = givens ++ bound_dicts 
-                                              ++ dict_irreds }
+          -- NB: Equality irreds need to be converted, as the recursive 
+          --     invocation of the solver will still treat them as wanteds
+          --     otherwise.
+       ; let implic_env = env { red_givens 
+                                   = givens ++ bound_dicts ++
+                                     map wantedToLocalEqInst dict_irreds }

        ; (implic_binds_s, implic_irreds_s) 
        ; (implic_binds_s, implic_irreds_s) 

-            <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0
+            <- mapAndUnzipM (reduceImplication implic_env) wanted_implics

        ; let implic_binds  = unionManyBags implic_binds_s
              implic_irreds = concat implic_irreds_s
 
        ; let implic_binds  = unionManyBags implic_binds_s
              implic_irreds = concat implic_irreds_s
 

-         -- Normalise the wanted equality constraints
-       ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs)
-
-         -- Normalise the wanted dictionaries
-       ; let irreds = dict_irreds ++ implic_irreds
-              eqs    = eq_irreds ++ given_eqs
-       ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds
-               
-         -- Figure out whether we should go round again.  We do so in either
-          -- two cases:
-          -- (1) If any of the mutable tyvars in givens or irreds has been
-          --     filled in by improvement, there is merit in going around 
-          --     again, because we may make further progress.
-          -- (2) If we managed to normalise any dicts, there is merit in going
-          --     around gain, because reduceList may be able to get further.
-         -- 
-         -- ToDo: We may have exposed new
-         --       equality constraints and should probably go round again
-         --       then as well.  But currently we are dropping them on the
-         --       floor anyway.
-
-       ; let all_irreds = norm_irreds ++ eq_irreds
-       ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $
-                           tyVarsOfInsts (givens ++ all_irreds)
-        ; let improvedDicts = not $ isEmptyBag normalise_binds
-              improved      = improvedMetaTy || improvedDicts
-
-       -- The old plan (fragile)
-       -- improveed   = availsImproved avails 
-       --               || (not $ isEmptyBag normalise_binds1)
-       --               || (not $ isEmptyBag normalise_binds2)
-       --               || (any isEqInst irreds)
+          -- Collect all irreducible instances, and determine whether we should
+          -- go round again.  We do so in either of two cases:
+          -- (1) If dictionary reduction or equality solving led to
+          --     improvement (i.e., instantiated type variables).
+          -- (2) If we reduced dictionaries (i.e., got dictionary bindings),
+          --     they may have exposed further opportunities to normalise
+          --     family applications.  See Note [Dictionary Improvement]
+          --
+          -- NB: We do *not* go around for new extra_eqs.  Morally, we should,
+          --     but we can't without risking non-termination (see #2688).  By
+          --     not going around, we miss some legal programs mixing FDs and
+          --     TFs, but we never claimed to support such programs in the
+          --     current implementation anyway.
+
+       ; let all_irreds       = dict_irreds ++ implic_irreds ++ extra_eqs
+             avails_improved  = availsImproved avails
+              improvedFlexible = avails_improved || eq_improved
+              reduced_dicts    = not (isEmptyBag dict_binds)
+              improved         = improvedFlexible || reduced_dicts
+              --
+              improvedHint  = (if avails_improved then " [AVAILS]" else "") ++
+                              (if eq_improved then " [EQ]" else "")

 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             red_doc env,
             text "given" <+> ppr givens,
 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             red_doc env,
             text "given" <+> ppr givens,

-            text "given_eqs" <+> ppr given_eqs,
-            text "wanted" <+> ppr wanteds,
-            text "wanted_dicts" <+> ppr wanted_dicts,
+            text "wanted" <+> ppr wanteds0,

             text "----",
             text "avails" <+> pprAvails avails,
             text "----",
             text "avails" <+> pprAvails avails,

-            text "improved =" <+> ppr improved,
+            text "improved =" <+> ppr improved <+> text improvedHint,

             text "(all) irreds = " <+> ppr all_irreds,
             text "dict-binds = " <+> ppr dict_binds,
             text "implic-binds = " <+> ppr implic_binds,
             text "(all) irreds = " <+> ppr all_irreds,
             text "dict-binds = " <+> ppr dict_binds,
             text "implic-binds = " <+> ppr implic_binds,

@@ -1851,11 +1970,9 @@ reduceContext env wanteds
             ]))
 
        ; return (improved, 
             ]))
 
        ; return (improved, 

-                  given_binds `unionBags` normalise_binds
-                              `unionBags` dict_binds 
-                              `unionBags` implic_binds, 
-                  all_irreds,
-                  eliminate_skolems) 
+                  normalise_binds `unionBags` dict_binds 
+                                  `unionBags` implic_binds, 
+                  all_irreds) 

         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone

@@ -1870,36 +1987,88 @@ tcImproveOne avails inst
                -- Avails has all the superclasses etc (good)
                -- It also has all the intermediates of the deduction (good)
                -- It does not have duplicates (good)
                -- 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
+               -- NB that (?x::t1) and (?x::t2) will be held separately in 
+                --    avails so that improve will see them separate

        ; traceTc (text "improveOne" <+> ppr inst)
        ; unifyEqns eqns }
 
        ; traceTc (text "improveOne" <+> ppr inst)
        ; unifyEqns eqns }
 

-unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))] 
+unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))] 

          -> TcM ImprovementDone
 unifyEqns [] = return False
 unifyEqns eqns
   = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
          -> TcM ImprovementDone
 unifyEqns [] = return False
 unifyEqns eqns
   = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))

-        ; mapM_ unify eqns
-       ; return True }
+        ; improved <- mapM unify eqns
+       ; return $ or improved
+        }

   where
     unify ((qtvs, pairs), what1, what2)
   where
     unify ((qtvs, pairs), what1, what2)

-         = addErrCtxtM (mkEqnMsg what1 what2) $ do
-           (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
-           mapM_ (unif_pr tenv) pairs
-    unif_pr tenv (ty1,ty2) =  unifyType (substTy tenv ty1) (substTy tenv ty2)
+         = addErrCtxtM (mkEqnMsg what1 what2) $ 
+             do { let freeTyVars = unionVarSets (map tvs_pr pairs) 
+                                   `minusVarSet` qtvs
+                ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+                ; mapM_ (unif_pr tenv) pairs
+                ; anyM isFilledMetaTyVar $ varSetElems freeTyVars
+                }
+
+    unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)

 
 

-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+    tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2

 
 

+pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
+pprEquationDoc (eqn, (p1, _), (p2, _)) 
+  = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+         -> TcM (TidyEnv, SDoc)

 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env

-  = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
-       ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
+  = do { pred1' <- zonkTcPredType pred1
+        ; pred2' <- zonkTcPredType pred2
+       ; let { pred1'' = tidyPred tidy_env pred1'
+              ; pred2'' = tidyPred tidy_env pred2' }

        ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
                          nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
                          nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
        ; return (tidy_env, msg) }
 \end{code}
 
        ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
                          nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
                          nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
        ; return (tidy_env, msg) }
 \end{code}
 

+Note [Dictionary Improvement]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reduceContext, we first reduce equalities and then class constraints.
+However, the letter may expose further opportunities for the former.  Hence,
+we need to go around again if dictionary reduction produced any dictionary
+bindings.  The following example demonstrated the point:
+
+  data EX _x _y (p :: * -> *)
+  data ANY
+
+  class Base p
+
+  class Base (Def p) => Prop p where
+   type Def p
+
+  instance Base ()
+  instance Prop () where
+   type Def () = ()
+
+  instance (Base (Def (p ANY))) => Base (EX _x _y p)
+  instance (Prop (p ANY)) => Prop (EX _x _y p) where
+   type Def (EX _x _y p) = EX _x _y p
+
+  data FOO x
+  instance Prop (FOO x) where
+   type Def (FOO x) = ()
+
+  data BAR
+  instance Prop BAR where
+   type Def BAR = EX () () FOO
+
+During checking the last instance declaration, we need to check the superclass
+cosntraint Base (Def BAR), which family normalisation reduced to 
+Base (EX () () FOO).  Chasing the instance for Base (EX _x _y p), gives us
+Base (Def (FOO ANY)), which again requires family normalisation of Def to
+Base () before we can finish.
+
+

 The main context-reduction function is @reduce@.  Here's its game plan.
 
 \begin{code}
 The main context-reduction function is @reduce@.  Here's its game plan.
 
 \begin{code}

@@ -1920,9 +2089,16 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
                         ; go ws state' }
 
     -- Base case: we're done!
                         ; go ws state' }
 
     -- Base case: we're done!

+reduce :: RedEnv -> Inst -> Avails -> TcM Avails

 reduce env wanted avails
 reduce env wanted avails

+
+    -- We don't reduce equalities here (and they must not end up as irreds
+    -- in the Avails!)
+  | isEqInst wanted
+  = return avails
+

     -- It's the same as an existing inst, or a superclass thereof
     -- It's the same as an existing inst, or a superclass thereof

-  | Just avail <- findAvail avails wanted
+  | Just _ <- findAvail avails wanted

   = do { traceTc (text "reduce: found " <+> ppr wanted)
        ; return avails
        }
   = do { traceTc (text "reduce: found " <+> ppr wanted)
        ; return avails
        }

@@ -1933,18 +2109,18 @@ reduce env wanted avails
            Stop -> try_simple (addIrred NoSCs);
                        -- See Note [No superclasses for Stop]
 
            Stop -> try_simple (addIrred NoSCs);
                        -- See Note [No superclasses for Stop]
 

-           ReduceMe want_scs -> do     -- It should be reduced
+           ReduceMe -> do      -- It should be reduced

                { (avails, lookup_result) <- reduceInst env avails wanted
                ; case lookup_result of
                { (avails, lookup_result) <- reduceInst env avails wanted
                ; case lookup_result of

-                   NoInstance -> addIrred want_scs avails wanted
+                   NoInstance -> addIrred AddSCs avails wanted

                             -- Add it and its superclasses
                             
                             -- Add it and its superclasses
                             

-                   GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+                   GenInst [] rhs -> addWanted AddSCs avails wanted rhs []

 
                    GenInst wanteds' rhs
                          -> do { avails1 <- addIrred NoSCs avails wanted
                                ; avails2 <- reduceList env wanteds' avails1
 
                    GenInst wanteds' rhs
                          -> do { avails1 <- addIrred NoSCs avails wanted
                                ; avails2 <- reduceList env wanteds' avails1

-                               ; addWanted want_scs avails2 wanted rhs wanteds' } }
+                               ; addWanted AddSCs avails2 wanted rhs wanteds' } }

                -- Temporarily do addIrred *before* the reduceList, 
                -- which has the effect of adding the thing we are trying
                -- to prove to the database before trying to prove the things it
                -- Temporarily do addIrred *before* the reduceList, 
                -- which has the effect of adding the thing we are trying
                -- to prove to the database before trying to prove the things it

@@ -1962,14 +2138,50 @@ reduce env wanted avails
       = do { res <- lookupSimpleInst wanted
           ; case res of
                GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
       = do { res <- lookupSimpleInst wanted
           ; case res of
                GenInst [] rhs -> addWanted AddSCs avails wanted rhs []

-               other          -> do_this_otherwise avails wanted }
+               _              -> do_this_otherwise avails wanted }

 \end{code}
 
 
 \end{code}
 
 

+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider 
+    data D r = ZeroD | SuccD (r (D r));
+    
+    instance (Eq (r (D r))) => Eq (D r) where
+        ZeroD     == ZeroD     = True
+        (SuccD a) == (SuccD b) = a == b
+        _         == _         = False;
+    
+    equalDC :: D [] -> D [] -> Bool;
+    equalDC = (==);
+
+We need to prove (Eq (D [])).  Here's how we go:
+
+       d1 : Eq (D [])
+
+by instance decl, holds if
+       d2 : Eq [D []]
+       where   d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+       d3 : D []
+       where   d2 = dfEqList d3
+               d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+       d3 = d1
+       d2 = dfEqList d3
+       d1 = dfEqD d2
+
+and it'll even run!  The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+       

 Note [SUPERCLASS-LOOP 2]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 Note [SUPERCLASS-LOOP 2]
 ~~~~~~~~~~~~~~~~~~~~~~~~

-But the above isn't enough.  Suppose we are *given* d1:Ord a,
-and want to deduce (d2:C [a]) where
+We need to be careful when adding "the constaint we are trying to prove".
+Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where

 
        class Ord a => C a where
        instance Ord [a] => C [a] where ...
 
        class Ord a => C a where
        instance Ord [a] => C [a] where ...

@@ -2007,42 +2219,6 @@ Now we implement the Right Solution, which is to check for loops directly
 when adding superclasses.  It's a bit like the occurs check in unification.
 
 
 when adding superclasses.  It's a bit like the occurs check in unification.
 
 

-Note [RECURSIVE DICTIONARIES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider 
-    data D r = ZeroD | SuccD (r (D r));
-    
-    instance (Eq (r (D r))) => Eq (D r) where
-        ZeroD     == ZeroD     = True
-        (SuccD a) == (SuccD b) = a == b
-        _         == _         = False;
-    
-    equalDC :: D [] -> D [] -> Bool;
-    equalDC = (==);
-
-We need to prove (Eq (D [])).  Here's how we go:
-
-       d1 : Eq (D [])
-
-by instance decl, holds if
-       d2 : Eq [D []]
-       where   d1 = dfEqD d2
-
-by instance decl of Eq, holds if
-       d3 : D []
-       where   d2 = dfEqList d3
-               d1 = dfEqD d2
-
-But now we can "tie the knot" to give
-
-       d3 = d1
-       d2 = dfEqList d3
-       d1 = dfEqD d2
-
-and it'll even run!  The trick is to put the thing we are trying to prove
-(in this case Eq (D []) into the database before trying to prove its
-contributing clauses.
-       

 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *

@@ -2053,7 +2229,7 @@ contributing clauses.
 \begin{code}
 ---------------------------------------------
 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
 \begin{code}
 ---------------------------------------------
 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)

-reduceInst env avails other_inst
+reduceInst _ avails other_inst

   = do { result <- lookupSimpleInst other_inst
        ; return (avails, result) }
 \end{code}
   = do { result <- lookupSimpleInst other_inst
        ; return (avails, result) }
 \end{code}

@@ -2111,20 +2287,32 @@ Note that
        --
        -- Note on coercion variables:
        --
        --
        -- Note on coercion variables:
        --

-       --      The extra given coercion variables are bound at two different sites:
+       --      The extra given coercion variables are bound at two different 
+        --      sites:
+        --

        --      -) in the creation context of the implication constraint        
        --              the solved equational constraints use these binders
        --
        --      -) at the solving site of the implication constraint
        --      -) in the creation context of the implication constraint        
        --              the solved equational constraints use these binders
        --
        --      -) at the solving site of the implication constraint

-       --              the solved dictionaries use these binders               
+       --              the solved dictionaries use these binders;

        --              these binders are generated by reduceImplication
        --
        --              these binders are generated by reduceImplication
        --

+        -- Note [Binders for equalities]
+        -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+        -- To reuse the binders of local/given equalities in the binders of 
+        -- implication constraints, it is crucial that these given equalities
+        -- always have the form
+        --   cotv :: t1 ~ t2
+        -- where cotv is a simple coercion type variable (and not a more
+        -- complex coercion term).  We require that the extra_givens always
+        -- have this form and exploit the special form when generating binders.

 reduceImplication env
        orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
                                  tci_tyvars = tvs,
 reduceImplication env
        orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
                                  tci_tyvars = tvs,

-                                 tci_given = extra_givens, tci_wanted = wanteds })
+                                 tci_given = extra_givens, tci_wanted = wanteds
+                                 })

   = do {       -- Solve the sub-problem
   = do {       -- Solve the sub-problem

-       ; let try_me inst = ReduceMe AddSCs  -- Note [Freeness and implications]
+       ; let try_me _ = ReduceMe  -- Note [Freeness and implications]

              env' = env { red_givens = extra_givens ++ red_givens env
                         , red_doc = sep [ptext (sLit "reduceImplication for") 
                                             <+> ppr name,
              env' = env { red_givens = extra_givens ++ red_givens env
                         , red_doc = sep [ptext (sLit "reduceImplication for") 
                                             <+> ppr name,

@@ -2136,13 +2324,6 @@ reduceImplication env
                        [ ppr (red_givens env), ppr extra_givens, 
                          ppr wanteds])
        ; (irreds, binds) <- checkLoop env' wanteds
                        [ ppr (red_givens env), ppr extra_givens, 
                          ppr wanteds])
        ; (irreds, binds) <- checkLoop env' wanteds

-       ; let   (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
-                       -- SLPJ Sept 07: I think this is bogus; currently
-                       -- there are no Eqinsts in extra_givens
-               dict_ids = map instToId extra_dict_givens 
-
-               -- Note [Reducing implication constraints]
-               -- Tom -- update note, put somewhere!

 
        ; traceTc (text "reduceImplication result" <+> vcat
                        [ppr irreds, ppr binds])
 
        ; traceTc (text "reduceImplication result" <+> vcat
                        [ppr irreds, ppr binds])

@@ -2156,11 +2337,17 @@ reduceImplication env
        -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
        -- Then we must iterate the outer loop too!
 
        -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
        -- Then we must iterate the outer loop too!
 

-       ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
+        ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+                                   -- we solve wanted eqs by side effect!

 
 

---     Progress is no longer measered by the number of bindings
-       ; if (isEmptyLHsBinds binds) && (not $ null irreds) then        -- No progress
-               -- If there are any irreds, we back off and do nothing
+            -- Progress is no longer measered by the number of bindings
+            -- If there are any irreds, but no bindings and no solved
+            -- equalities, we back off and do nothing
+        ; let backOff = isEmptyLHsBinds binds &&   -- no new bindings
+                        (not $ null irreds)   &&   -- but still some irreds
+                        didntSolveWantedEqs        -- no instantiated cotv
+
+       ; if backOff then       -- No progress

                return (emptyBag, [orig_implic])
          else do
        { (simpler_implic_insts, bind) 
                return (emptyBag, [orig_implic])
          else do
        { (simpler_implic_insts, bind) 

@@ -2170,36 +2357,39 @@ reduceImplication env
                -- case.  After all, we only try hard to reduce at top level, or
                -- when inferring types.
 
                -- case.  After all, we only try hard to reduce at top level, or
                -- when inferring types.
 

-       ; let   dict_wanteds = filter (not . isEqInst) wanteds
-               -- TOMDO: given equational constraints bug!
-               --  we need a different evidence for given
-               --  equations depending on whether we solve
-               --  dictionary constraints or equational constraints
-
-               eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
-                       -- SLPJ Sept07: this looks Utterly Wrong to me, but I think
-                       --              that current extra_givens has no EqInsts, so
-                       --              it makes no difference
-               co  = wrap_inline       -- Note [Always inline implication constraints]
-                     <.> mkWpTyLams tvs
-                     <.> mkWpLams eq_tyvars
-                     <.> mkWpLams dict_ids
-                     <.> WpLet (binds `unionBags` bind)
-               wrap_inline | null dict_ids = idHsWrapper
-                           | otherwise     = WpInline
-               rhs = mkHsWrap co payload
-               loc = instLocSpan inst_loc
-               payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
-                       | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
+       ; let   -- extract Id binders for dicts and CoTyVar binders for eqs;
+                -- see Note [Binders for equalities]
+             (extra_eq_givens, extra_dict_givens) = partition isEqInst 
+                                                               extra_givens
+              eq_cotvs = map instToVar extra_eq_givens
+             dict_ids = map instToId  extra_dict_givens 
+
+                        -- Note [Always inline implication constraints]
+              wrap_inline | null dict_ids = idHsWrapper
+                          | otherwise    = WpInline
+              co         = wrap_inline
+                           <.> mkWpTyLams tvs
+                           <.> mkWpTyLams eq_cotvs
+                           <.> mkWpLams dict_ids
+                           <.> WpLet (binds `unionBags` bind)
+              rhs        = mkLHsWrap co payload
+              loc        = instLocSpan inst_loc
+                            -- wanted equalities are solved by updating their
+                             -- cotv; we don't generate bindings for them
+              dict_bndrs =   map (L loc . HsVar . instToId) 
+                           . filter (not . isEqInst) 
+                           $ wanteds
+              payload    = mkBigLHsTup dict_bndrs

 
        
        ; traceTc (vcat [text "reduceImplication" <+> ppr name,
                         ppr simpler_implic_insts,
                         text "->" <+> ppr rhs])
 
        
        ; traceTc (vcat [text "reduceImplication" <+> ppr name,
                         ppr simpler_implic_insts,
                         text "->" <+> ppr rhs])

-       ; return (unitBag (L loc (VarBind (instToId orig_implic) (L loc rhs))),
+       ; return (unitBag (L loc (VarBind (instToId orig_implic) rhs)),

                  simpler_implic_insts)
        } 
     }
                  simpler_implic_insts)
        } 
     }

+reduceImplication _ i = pprPanic "reduceImplication" (ppr i)

 \end{code}
 
 Note [Always inline implication constraints]
 \end{code}
 
 Note [Always inline implication constraints]

@@ -2237,12 +2427,29 @@ We can satisfy the (C Int) from the superclass of D, so we don't want
 to float the (C Int) out, even though it mentions no type variable in
 the constraints!
 
 to float the (C Int) out, even though it mentions no type variable in
 the constraints!
 

+One more example: the constraint
+       class C a => D a b
+       instance (C a, E c) => E (a,c)
+
+       constraint: forall b. D Int b => E (Int,c)
+
+You might think that the (D Int b) can't possibly contribute
+to solving (E (Int,c)), since the latter mentions 'c'.  But 
+in fact it can, because solving the (E (Int,c)) constraint needs 
+dictionaries
+       C Int, E c
+and the (C Int) can be satisfied from the superclass of (D Int b).
+So we must still not float (E (Int,c)) out.
+
+To think about: special cases for unary type classes?
+

 Note [Pruning the givens in an implication constraint]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are about to form the implication constraint
        forall tvs.  Eq a => Ord b
 The (Eq a) cannot contribute to the (Ord b), because it has no access to
 the type variable 'b'.  So we could filter out the (Eq a) from the givens.
 Note [Pruning the givens in an implication constraint]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are about to form the implication constraint
        forall tvs.  Eq a => Ord b
 The (Eq a) cannot contribute to the (Ord b), because it has no access to
 the type variable 'b'.  So we could filter out the (Eq a) from the givens.

+But BE CAREFUL of the examples above in [Freeness and implications].

 
 Doing so would be a bit tidier, but all the implication constraints get
 simplified away by the optimiser, so it's no great win.   So I don't take
 
 Doing so would be a bit tidier, but all the implication constraints get
 simplified away by the optimiser, so it's no great win.   So I don't take

@@ -2280,6 +2487,7 @@ data AvailHow
 instance Outputable Avails where
   ppr = pprAvails
 
 instance Outputable Avails where
   ppr = pprAvails
 

+pprAvails :: Avails -> SDoc

 pprAvails (Avails imp avails)
   = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
         , nest 2 $ braces $ 
 pprAvails (Avails imp avails)
   = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
         , nest 2 $ braces $ 

@@ -2324,11 +2532,8 @@ extendAvails avails@(Avails imp env) inst avail
 availsInsts :: Avails -> [Inst]
 availsInsts (Avails _ avails) = keysFM avails
 
 availsInsts :: Avails -> [Inst]
 availsInsts (Avails _ avails) = keysFM avails
 

+availsImproved :: Avails -> ImprovementDone

 availsImproved (Avails imp _) = imp
 availsImproved (Avails imp _) = imp

-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1

 \end{code}
 
 Extracting the bindings from a bunch of Avails.
 \end{code}
 
 Extracting the bindings from a bunch of Avails.

@@ -2356,10 +2561,13 @@ extractResults (Avails _ avails) wanteds
        -> DoneEnv      -- Has an entry for each inst in the above three sets
        -> [Inst]       -- Wanted
        -> TcM (TcDictBinds, [Inst], [Inst])
        -> DoneEnv      -- Has an entry for each inst in the above three sets
        -> [Inst]       -- Wanted
        -> TcM (TcDictBinds, [Inst], [Inst])

-    go binds bound_dicts irreds done [] 
+    go binds bound_dicts irreds _ [] 

       = return (binds, bound_dicts, irreds)
 
     go binds bound_dicts irreds done (w:ws)
       = return (binds, bound_dicts, irreds)
 
     go binds bound_dicts irreds done (w:ws)

+      | isEqInst w
+      = go binds bound_dicts (w:irreds) done' ws
+

       | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
       = if w_id `elem` done_ids then
           go binds bound_dicts irreds done ws
       | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
       = if w_id `elem` done_ids then
           go binds bound_dicts irreds done ws

@@ -2406,12 +2614,18 @@ addWanted want_scs avails wanted rhs_expr wanteds
     avail = Rhs rhs_expr wanteds
 
 addGiven :: Avails -> Inst -> TcM Avails
     avail = Rhs rhs_expr wanteds
 
 addGiven :: Avails -> Inst -> TcM Avails

-addGiven avails given = addAvailAndSCs AddSCs avails given (Given given)
-       -- Always add superclasses for 'givens'
-       --
-       -- No ASSERT( not (given `elemAvails` avails) ) because in an instance
-       -- decl for Ord t we can add both Ord t and Eq t as 'givens', 
-       -- so the assert isn't true
+addGiven avails given 
+  = addAvailAndSCs want_scs avails given (Given given)
+  where
+    want_scs = case instLocOrigin (instLoc given) of
+                NoScOrigin -> NoSCs
+                _other     -> AddSCs
+       -- Conditionally add superclasses for 'given'
+       -- See Note [Recursive instances and superclases]
+
+  -- No ASSERT( not (given `elemAvails` avails) ) because in an
+  -- instance decl for Ord t we can add both Ord t and Eq t as
+  -- 'givens', so the assert isn't true

 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}

@@ -2438,7 +2652,7 @@ addAvailAndSCs want_scs avails inst avail
     -- Watch out, though.  Since the avails may contain loops 
     -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
     findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
     -- Watch out, though.  Since the avails may contain loops 
     -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
     findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids

-    findAllDeps so_far other       = so_far
+    findAllDeps so_far _            = so_far

 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid
 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid

@@ -2478,7 +2692,7 @@ addSCs is_loop avails dict
     is_given :: Inst -> Bool
     is_given sc_dict = case findAvail avails sc_dict of
                          Just (Given _) -> True        -- Given is cheaper than superclass selection
     is_given :: Inst -> Bool
     is_given sc_dict = case findAvail avails sc_dict of
                          Just (Given _) -> True        -- Given is cheaper than superclass selection

-                         other          -> False       
+                         _              -> False

 
 -- From the a set of insts obtain all equalities that (transitively) occur in
 -- superclass contexts of class constraints (aka the ancestor equalities). 
 
 -- From the a set of insts obtain all equalities that (transitively) occur in
 -- superclass contexts of class constraints (aka the ancestor equalities). 

@@ -2542,6 +2756,7 @@ tcSimplifyInteractive wanteds
 
 -- The TcLclEnv should be valid here, solely to improve
 -- error message generation for the monomorphism restriction
 
 -- The TcLclEnv should be valid here, solely to improve
 -- error message generation for the monomorphism restriction

+tc_simplify_top :: SDoc -> Bool -> [Inst] -> TcM (Bag (LHsBind TcId))

 tc_simplify_top doc interactive wanteds
   = do { dflags <- getDOpts
        ; wanteds <- zonkInsts wanteds
 tc_simplify_top doc interactive wanteds
   = do { dflags <- getDOpts
        ; wanteds <- zonkInsts wanteds

@@ -2551,7 +2766,7 @@ tc_simplify_top doc interactive wanteds
        ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
 --     ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
        ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
        ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
 --     ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
        ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)

-       ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
+       ; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1

        ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
 
                -- Use the defaulting rules to do extra unification
        ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
 
                -- Use the defaulting rules to do extra unification

@@ -2658,7 +2873,7 @@ disambiguate doc interactive dflags insts
        | extended_defaulting = any isInteractiveClass clss
        | otherwise           = all is_std_class clss && (any is_num_class clss)
 
        | extended_defaulting = any isInteractiveClass clss
        | otherwise           = all is_std_class clss && (any is_num_class clss)
 

-       -- In interactive mode, or with -fextended-default-rules,
+       -- In interactive mode, or with -XExtendedDefaultRules,

        -- we default Show a to Show () to avoid graututious errors on "show []"
    isInteractiveClass cls 
        = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
        -- we default Show a to Show () to avoid graututious errors on "show []"
    isInteractiveClass cls 
        = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])

@@ -2719,12 +2934,12 @@ getDefaultTys extended_deflts ovl_strings
                  opt_deflt ovl_strings string_ty) } } }
   where
     opt_deflt True  ty = [ty]
                  opt_deflt ovl_strings string_ty) } } }
   where
     opt_deflt True  ty = [ty]

-    opt_deflt False ty = []
+    opt_deflt False _  = []

 \end{code}
 
 Note [Default unitTy]
 ~~~~~~~~~~~~~~~~~~~~~
 \end{code}
 
 Note [Default unitTy]
 ~~~~~~~~~~~~~~~~~~~~~

-In interative mode (or with -fextended-default-rules) we add () as the first type we
+In interative mode (or with -XExtendedDefaultRules) we add () as the first type we

 try when defaulting.  This has very little real impact, except in the following case.
 Consider: 
        Text.Printf.printf "hello"
 try when defaulting.  This has very little real impact, except in the following case.
 Consider: 
        Text.Printf.printf "hello"

@@ -2781,7 +2996,8 @@ tcSimplifyDeriv orig tyvars theta
        ; (irreds, _) <- tryHardCheckLoop doc wanteds
 
        ; let (tv_dicts, others) = partition ok irreds
        ; (irreds, _) <- tryHardCheckLoop doc wanteds
 
        ; let (tv_dicts, others) = partition ok irreds

-       ; addNoInstanceErrs others
+             (tidy_env, tidy_insts) = tidyInsts others
+        ; reportNoInstances tidy_env Nothing [alt_fix] tidy_insts

        -- See Note [Exotic derived instance contexts] in TcMType
 
        ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
        -- See Note [Exotic derived instance contexts] in TcMType
 
        ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)

@@ -2795,6 +3011,8 @@ tcSimplifyDeriv orig tyvars theta
 
     ok dict | isDict dict = validDerivPred (dictPred dict)
            | otherwise   = False
 
     ok dict | isDict dict = validDerivPred (dictPred dict)
            | otherwise   = False

+    alt_fix = vcat [ptext (sLit "use a standalone 'deriving instance' declaration instead,"),
+                    ptext (sLit "so you can specify the instance context yourself")]

 \end{code}
 
 
 \end{code}
 
 

@@ -2809,7 +3027,7 @@ tcSimplifyDefault :: ThetaType    -- Wanted; has no type variables in it
 tcSimplifyDefault theta = do
     wanteds <- newDictBndrsO DefaultOrigin theta
     (irreds, _) <- tryHardCheckLoop doc wanteds
 tcSimplifyDefault theta = do
     wanteds <- newDictBndrsO DefaultOrigin theta
     (irreds, _) <- tryHardCheckLoop doc wanteds

-    addNoInstanceErrs  irreds
+    addNoInstanceErrs irreds

     if null irreds then
        return ()
      else
     if null irreds then
        return ()
      else

@@ -2818,6 +3036,26 @@ tcSimplifyDefault theta = do
     doc = ptext (sLit "default declaration")
 \end{code}
 
     doc = ptext (sLit "default declaration")
 \end{code}
 

+@tcSimplifyStagedExpr@ performs a simplification but does so at a new
+stage. This is used when typechecking annotations and splices.
+
+\begin{code}
+
+tcSimplifyStagedExpr :: ThStage -> TcM a -> TcM (a, TcDictBinds)
+-- Type check an expression that runs at a top level stage as if
+--   it were going to be spliced and then simplify it
+tcSimplifyStagedExpr stage tc_action
+  = setStage stage $ do { 
+        -- Typecheck the expression
+         (thing', lie) <- getLIE tc_action
+       
+       -- Solve the constraints
+       ; const_binds <- tcSimplifyTop lie
+       
+       ; return (thing', const_binds) }
+
+\end{code}
+

 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *

@@ -2836,7 +3074,7 @@ groupErrs :: ([Inst] -> TcM ())   -- Deal with one group
 -- Group together insts with the same origin
 -- We want to report them together in error messages
 
 -- Group together insts with the same origin
 -- We want to report them together in error messages
 

-groupErrs report_err [] 
+groupErrs _ [] 

   = return ()
 groupErrs report_err (inst:insts)
   = do { do_one (inst:friends)
   = return ()
 groupErrs report_err (inst:insts)
   = do { do_one (inst:friends)

@@ -2856,7 +3094,7 @@ addInstLoc :: [Inst] -> Message -> Message
 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
 
 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
 
 addTopIPErrs :: [Name] -> [Inst] -> TcM ()

-addTopIPErrs bndrs [] 
+addTopIPErrs _ [] 

   = return ()
 addTopIPErrs bndrs ips
   = do { dflags <- getDOpts
   = return ()
 addTopIPErrs bndrs ips
   = do { dflags <- getDOpts

@@ -2885,7 +3123,7 @@ addNoInstanceErrs :: [Inst]       -- Wanted (can include implications)
                  -> TcM ()     
 addNoInstanceErrs insts
   = do { let (tidy_env, tidy_insts) = tidyInsts insts
                  -> TcM ()     
 addNoInstanceErrs insts
   = do { let (tidy_env, tidy_insts) = tidyInsts insts

-       ; reportNoInstances tidy_env Nothing tidy_insts }
+       ; reportNoInstances tidy_env Nothing [] tidy_insts }

 
 reportNoInstances 
        :: TidyEnv
 
 reportNoInstances 
        :: TidyEnv

@@ -2893,13 +3131,15 @@ reportNoInstances
                        -- Nothing => top level
                        -- Just (d,g) => d describes the construct
                        --               with givens g
                        -- Nothing => top level
                        -- Just (d,g) => d describes the construct
                        --               with givens g

+        -> [SDoc]      -- Alternative fix for no-such-instance

        -> [Inst]       -- What is wanted (can include implications)
        -> TcM ()       
 
        -> [Inst]       -- What is wanted (can include implications)
        -> TcM ()       
 

-reportNoInstances tidy_env mb_what insts 
-  = groupErrs (report_no_instances tidy_env mb_what) insts
+reportNoInstances tidy_env mb_what alt_fix insts 
+  = groupErrs (report_no_instances tidy_env mb_what alt_fix) insts

 
 

-report_no_instances tidy_env mb_what insts
+report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [SDoc] -> [Inst] -> TcM ()
+report_no_instances tidy_env mb_what alt_fixes insts

   = do { inst_envs <- tcGetInstEnvs
        ; let (implics, insts1)  = partition isImplicInst insts
             (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
   = do { inst_envs <- tcGetInstEnvs
        ; let (implics, insts1)  = partition isImplicInst insts
             (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1

@@ -2917,7 +3157,7 @@ report_no_instances tidy_env mb_what insts
     complain_implic inst       -- Recurse!
       = reportNoInstances tidy_env 
                          (Just (tci_loc inst, tci_given inst)) 
     complain_implic inst       -- Recurse!
       = reportNoInstances tidy_env 
                          (Just (tci_loc inst, tci_given inst)) 

-                         (tci_wanted inst)
+                         alt_fixes (tci_wanted inst)

 
     check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
        -- Right msg  => overlap message
 
     check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
        -- Right msg  => overlap message

@@ -2930,7 +3170,7 @@ report_no_instances tidy_env mb_what insts
                -- The case of exactly one match and no unifiers means a
                -- successful lookup.  That can't happen here, because dicts
                -- only end up here if they didn't match in Inst.lookupInst
                -- The case of exactly one match and no unifiers means a
                -- successful lookup.  That can't happen here, because dicts
                -- only end up here if they didn't match in Inst.lookupInst

-               ([m],[])
+               ([_],[])

                 | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
                res -> Right (mk_overlap_msg wanted res)
          where
                 | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
                res -> Right (mk_overlap_msg wanted res)
          where

@@ -2949,7 +3189,7 @@ report_no_instances tidy_env mb_what insts
                ASSERT( not (null unifiers) )
                parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
                ASSERT( not (null unifiers) )
                parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),

-                             ptext (sLit "To pick the first instance above, use -fallow-incoherent-instances"),
+                             ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),

                              ptext (sLit "when compiling the other instance declarations")])]
       where
        ispecs = [ispec | (ispec, _) <- matches]
                              ptext (sLit "when compiling the other instance declarations")])]
       where
        ispecs = [ispec | (ispec, _) <- matches]

@@ -2965,13 +3205,13 @@ report_no_instances tidy_env mb_what insts
       = vcat [ addInstLoc insts $
               sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts
                   , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens]
       = vcat [ addInstLoc insts $
               sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts
                   , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens]

-            , show_fixes (fix1 loc : fixes2) ]
+            , show_fixes (fix1 loc : fixes2 ++ alt_fixes) ]

 
       | otherwise      -- Top level 
       = vcat [ addInstLoc insts $
               ptext (sLit "No instance") <> plural insts
                    <+> ptext (sLit "for") <+> pprDictsTheta insts
 
       | otherwise      -- Top level 
       = vcat [ addInstLoc insts $
               ptext (sLit "No instance") <> plural insts
                    <+> ptext (sLit "for") <+> pprDictsTheta insts

-            , show_fixes fixes2 ]
+            , show_fixes (fixes2 ++ alt_fixes) ]

 
       where
        fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts
 
       where
        fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts

@@ -2992,6 +3232,7 @@ report_no_instances tidy_env mb_what insts
        show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"), 
                                 nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
 
        show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"), 
                                 nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
 

+addTopAmbigErrs :: [Inst] -> TcRn ()

 addTopAmbigErrs dicts
 -- Divide into groups that share a common set of ambiguous tyvars
   = ifErrsM (return ()) $      -- Only report ambiguity if no other errors happened
 addTopAmbigErrs dicts
 -- Divide into groups that share a common set of ambiguous tyvars
   = ifErrsM (return ()) $      -- Only report ambiguity if no other errors happened

@@ -3047,10 +3288,11 @@ monomorphism_fix dflags
   = ptext (sLit "Probable fix:") <+> vcat
        [ptext (sLit "give these definition(s) an explicit type signature"),
         if dopt Opt_MonomorphismRestriction dflags
   = ptext (sLit "Probable fix:") <+> vcat
        [ptext (sLit "give these definition(s) an explicit type signature"),
         if dopt Opt_MonomorphismRestriction dflags

-           then ptext (sLit "or use -fno-monomorphism-restriction")
-           else empty] -- Only suggest adding "-fno-monomorphism-restriction"
+           then ptext (sLit "or use -XNoMonomorphismRestriction")
+           else empty] -- Only suggest adding "-XNoMonomorphismRestriction"

                        -- if it is not already set!
     
                        -- if it is not already set!
     

+warnDefault :: [(Inst, Class, Var)] -> Type -> TcM ()

 warnDefault ups default_ty = do
     warn_flag <- doptM Opt_WarnTypeDefaults
     addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
 warnDefault ups default_ty = do
     warn_flag <- doptM Opt_WarnTypeDefaults
     addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)

@@ -3063,10 +3305,12 @@ warnDefault ups default_ty = do
                                quotes (ppr default_ty),
                      pprDictsInFull tidy_dicts]
 
                                quotes (ppr default_ty),
                      pprDictsInFull tidy_dicts]
 

+reduceDepthErr :: Int -> [Inst] -> SDoc

 reduceDepthErr n stack
   = vcat [ptext (sLit "Context reduction stack overflow; size =") <+> int n,
          ptext (sLit "Use -fcontext-stack=N to increase stack size to N"),
          nest 4 (pprStack stack)]
 
 reduceDepthErr n stack
   = vcat [ptext (sLit "Context reduction stack overflow; size =") <+> int n,
          ptext (sLit "Use -fcontext-stack=N to increase stack size to N"),
          nest 4 (pprStack stack)]
 

+pprStack :: [Inst] -> SDoc

 pprStack stack = vcat (map pprInstInFull stack)
 \end{code}
 pprStack stack = vcat (map pprInstInFull stack)
 \end{code}