Rollback INLINE patches
[ghc-hetmet.git] / compiler / typecheck / TcInstDcls.lhs
index 203ffe4..e7c472b 100644 (file)
@@ -6,13 +6,6 @@
 TcInstDecls: Typechecking instance declarations
 
 \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 TcInstDcls ( tcInstDecls1, tcInstDecls2 ) where
 
 import HsSyn
@@ -28,6 +21,7 @@ import FamInst
 import FamInstEnv
 import TcDeriv
 import TcEnv
+import RnEnv   ( lookupImportedName )
 import TcHsType
 import TcUnify
 import TcSimplify
@@ -38,12 +32,12 @@ import TypeRep
 import DataCon
 import Class
 import Var
+import Id
 import MkId
 import Name
 import NameSet
 import DynFlags
 import SrcLoc
-import ListSetOps
 import Util
 import Outputable
 import Bag
@@ -54,6 +48,8 @@ import FastString
 import Data.Maybe
 import Control.Monad
 import Data.List
+
+#include "HsVersions.h"
 \end{code}
 
 Typechecking instance declarations is done in two passes. The first
@@ -66,67 +62,232 @@ pass, when the class-instance envs and GVE contain all the info from
 all the instance and value decls.  Indeed that's the reason we need
 two passes over the instance decls.
 
-Here is the overall algorithm.
-Assume that we have an instance declaration
-
-    instance c => k (t tvs) where b
-
-\begin{enumerate}
-\item
-$LIE_c$ is the LIE for the context of class $c$
-\item
-$betas_bar$ is the free variables in the class method type, excluding the
-   class variable
-\item
-$LIE_cop$ is the LIE constraining a particular class method
-\item
-$tau_cop$ is the tau type of a class method
-\item
-$LIE_i$ is the LIE for the context of instance $i$
-\item
-$X$ is the instance constructor tycon
-\item
-$gammas_bar$ is the set of type variables of the instance
-\item
-$LIE_iop$ is the LIE for a particular class method instance
-\item
-$tau_iop$ is the tau type for this instance of a class method
-\item
-$alpha$ is the class variable
-\item
-$LIE_cop' = LIE_cop [X gammas_bar / alpha, fresh betas_bar]$
-\item
-$tau_cop' = tau_cop [X gammas_bar / alpha, fresh betas_bar]$
-\end{enumerate}
-
-ToDo: Update the list above with names actually in the code.
-
-\begin{enumerate}
-\item
-First, make the LIEs for the class and instance contexts, which means
-instantiate $thetaC [X inst_tyvars / alpha ]$, yielding LIElistC' and LIEC',
-and make LIElistI and LIEI.
-\item
-Then process each method in turn.
-\item
-order the instance methods according to the ordering of the class methods
-\item
-express LIEC' in terms of LIEI, yielding $dbinds_super$ or an error
-\item
-Create final dictionary function from bindings generated already
-\begin{pseudocode}
-df = lambda inst_tyvars
-       lambda LIEI
-         let Bop1
-             Bop2
-             ...
-             Bopn
-         and dbinds_super
-              in <op1,op2,...,opn,sd1,...,sdm>
-\end{pseudocode}
-Here, Bop1 \ldots Bopn bind the methods op1 \ldots opn,
-and $dbinds_super$ bind the superclass dictionaries sd1 \ldots sdm.
-\end{enumerate}
+
+Note [How instance declarations are translated]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is how we translation instance declarations into Core
+
+Running example:
+       class C a where
+          op1, op2 :: Ix b => a -> b -> b
+          op2 = <dm-rhs>
+
+       instance C a => C [a]
+          {-# INLINE [2] op1 #-}
+          op1 = <rhs>
+===>
+       -- Method selectors
+       op1,op2 :: forall a. C a => forall b. Ix b => a -> b -> b
+       op1 = ...
+       op2 = ...
+
+       -- Default methods get the 'self' dictionary as argument
+       -- so they can call other methods at the same type
+       -- Default methods get the same type as their method selector
+       $dmop2 :: forall a. C a => forall b. Ix b => a -> b -> b
+       $dmop2 = /\a. \(d:C a). /\b. \(d2: Ix b). <dm-rhs>
+              -- NB: type variables 'a' and 'b' are *both* in scope in <dm-rhs>
+              -- Note [Tricky type variable scoping]
+
+       -- A top-level definition for each instance method
+       -- Here op1_i, op2_i are the "instance method Ids"
+       {-# INLINE [2] op1_i #-}  -- From the instance decl bindings
+       op1_i, op2_i :: forall a. C a => forall b. Ix b => [a] -> b -> b
+       op1_i = /\a. \(d:C a). 
+              let this :: C [a]
+                  this = df_i a d
+                    -- Note [Subtle interaction of recursion and overlap]
+
+                  local_op1 :: forall b. Ix b => [a] -> b -> b
+                  local_op1 = <rhs>
+                    -- Source code; run the type checker on this
+                    -- NB: Type variable 'a' (but not 'b') is in scope in <rhs>
+                    -- Note [Tricky type variable scoping]
+
+              in local_op1 a d
+
+       op2_i = /\a \d:C a. $dmop2 [a] (df_i a d) 
+
+       -- The dictionary function itself
+       {-# INLINE df_i #-}     -- Always inline dictionary functions
+       df_i :: forall a. C a -> C [a]
+       df_i = /\a. \d:C a. letrec d' = MkC (op1_i  a   d)
+                                            ($dmop2 [a] d')
+                           in d'
+               -- But see Note [Default methods in instances]
+               -- We can't apply the type checker to the default-method call
+
+* The dictionary function itself is inlined as vigorously as we
+  possibly can, so that we expose that dictionary constructor to
+  selectors as much as poss.  That is why the op_i stuff is in 
+  *separate* bindings, so that the df_i binding is small enough
+  to inline.  See Note [Inline dfuns unconditionally].
+
+* Note that df_i may be mutually recursive with both op1_i and op2_i.
+  It's crucial that df_i is not chosen as the loop breaker, even 
+  though op1_i has a (user-specified) INLINE pragma.
+  Not even once!  Else op1_i, op2_i may be inlined into df_i.
+
+* Instead the idea is to inline df_i into op1_i, which may then select
+  methods from the MkC record, and thereby break the recursion with
+  df_i, leaving a *self*-recurisve op1_i.  (If op1_i doesn't call op at
+  the same type, it won't mention df_i, so there won't be recursion in
+  the first place.)  
+
+* If op1_i is marked INLINE by the user there's a danger that we won't
+  inline df_i in it, and that in turn means that (since it'll be a
+  loop-breaker because df_i isn't), op1_i will ironically never be 
+  inlined.  We need to fix this somehow -- perhaps allowing inlining
+  of INLINE funcitons inside other INLINE functions.
+
+Note [Subtle interaction of recursion and overlap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+  class C a where { op1,op2 :: a -> a }
+  instance C a => C [a] where
+    op1 x = op2 x ++ op2 x
+    op2 x = ...
+  intance C [Int] where
+    ...
+
+When type-checking the C [a] instance, we need a C [a] dictionary (for
+the call of op2).  If we look up in the instance environment, we find
+an overlap.  And in *general* the right thing is to complain (see Note
+[Overlapping instances] in InstEnv).  But in *this* case it's wrong to
+complain, because we just want to delegate to the op2 of this same
+instance.  
+
+Why is this justified?  Because we generate a (C [a]) constraint in 
+a context in which 'a' cannot be instantiated to anything that matches
+other overlapping instances, or else we would not be excecuting this
+version of op1 in the first place.
+
+It might even be a bit disguised:
+
+  nullFail :: C [a] => [a] -> [a]
+  nullFail x = op2 x ++ op2 x
+
+  instance C a => C [a] where
+    op1 x = nullFail x
+
+Precisely this is used in package 'regex-base', module Context.hs.
+See the overlapping instances for RegexContext, and the fact that they
+call 'nullFail' just like the example above.  The DoCon package also
+does the same thing; it shows up in module Fraction.hs
+
+Conclusion: when typechecking the methods in a C [a] instance, we want
+to have C [a] available.  That is why we have the strange local
+definition for 'this' in the definition of op1_i in the example above.
+We can typecheck the defintion of local_op1, and when doing tcSimplifyCheck
+we supply 'this' as a given dictionary.  Only needed, though, if there
+are some type variales involved; otherwise there can be no overlap and
+none of this arises.
+
+Note [Tricky type variable scoping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In our example
+       class C a where
+          op1, op2 :: Ix b => a -> b -> b
+          op2 = <dm-rhs>
+
+       instance C a => C [a]
+          {-# INLINE [2] op1 #-}
+          op1 = <rhs>
+
+note that 'a' and 'b' are *both* in scope in <dm-rhs>, but only 'a' is
+in scope in <rhs>.  In particular, we must make sure that 'b' is in
+scope when typechecking <dm-rhs>.  This is achieved by subFunTys,
+which brings appropriate tyvars into scope. This happens for both
+<dm-rhs> and for <rhs>, but that doesn't matter: the *renamer* will have
+complained if 'b' is mentioned in <rhs>.
+
+Note [Inline dfuns unconditionally]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The code above unconditionally inlines dict funs.  Here's why.
+Consider this program:
+
+    test :: Int -> Int -> Bool
+    test x y = (x,y) == (y,x) || test y x
+    -- Recursive to avoid making it inline.
+
+This needs the (Eq (Int,Int)) instance.  If we inline that dfun
+the code we end up with is good:
+
+    Test.$wtest =
+        \r -> case ==# [ww ww1] of wild {
+                PrelBase.False -> Test.$wtest ww1 ww;
+                PrelBase.True ->
+                  case ==# [ww1 ww] of wild1 {
+                    PrelBase.False -> Test.$wtest ww1 ww;
+                    PrelBase.True -> PrelBase.True [];
+                  };
+            };
+    Test.test = \r [w w1]
+            case w of w2 {
+              PrelBase.I# ww ->
+                  case w1 of w3 { PrelBase.I# ww1 -> Test.$wtest ww ww1; };
+            };
+
+If we don't inline the dfun, the code is not nearly as good:
+
+    (==) = case PrelTup.$fEq(,) PrelBase.$fEqInt PrelBase.$fEqInt of tpl {
+              PrelBase.:DEq tpl1 tpl2 -> tpl2;
+            };
+
+    Test.$wtest =
+        \r [ww ww1]
+            let { y = PrelBase.I#! [ww1]; } in
+            let { x = PrelBase.I#! [ww]; } in
+            let { sat_slx = PrelTup.(,)! [y x]; } in
+            let { sat_sly = PrelTup.(,)! [x y];
+            } in
+              case == sat_sly sat_slx of wild {
+                PrelBase.False -> Test.$wtest ww1 ww;
+                PrelBase.True -> PrelBase.True [];
+              };
+
+    Test.test =
+        \r [w w1]
+            case w of w2 {
+              PrelBase.I# ww ->
+                  case w1 of w3 { PrelBase.I# ww1 -> Test.$wtest ww ww1; };
+            };
+
+Why didn't GHC inline $fEq in those days?  Because it looked big:
+
+    PrelTup.zdfEqZ1T{-rcX-}
+        = \ @ a{-reT-} :: * @ b{-reS-} :: *
+            zddEq{-rf6-} _Ks :: {PrelBase.Eq{-23-} a{-reT-}}
+            zddEq1{-rf7-} _Ks :: {PrelBase.Eq{-23-} b{-reS-}} ->
+            let {
+              zeze{-rf0-} _Kl :: (b{-reS-} -> b{-reS-} -> PrelBase.Bool{-3c-})
+              zeze{-rf0-} = PrelBase.zeze{-01L-}@ b{-reS-} zddEq1{-rf7-} } in
+            let {
+              zeze1{-rf3-} _Kl :: (a{-reT-} -> a{-reT-} -> PrelBase.Bool{-3c-})
+              zeze1{-rf3-} = PrelBase.zeze{-01L-} @ a{-reT-} zddEq{-rf6-} } in
+            let {
+              zeze2{-reN-} :: ((a{-reT-}, b{-reS-}) -> (a{-reT-}, b{-reS-})-> PrelBase.Bool{-3c-})
+              zeze2{-reN-} = \ ds{-rf5-} _Ks :: (a{-reT-}, b{-reS-})
+                               ds1{-rf4-} _Ks :: (a{-reT-}, b{-reS-}) ->
+                             case ds{-rf5-}
+                             of wild{-reW-} _Kd { (a1{-rf2-} _Ks, a2{-reZ-} _Ks) ->
+                             case ds1{-rf4-}
+                             of wild1{-reX-} _Kd { (b1{-rf1-} _Ks, b2{-reY-} _Ks) ->
+                             PrelBase.zaza{-r4e-}
+                               (zeze1{-rf3-} a1{-rf2-} b1{-rf1-})
+                               (zeze{-rf0-} a2{-reZ-} b2{-reY-})
+                             }
+                             } } in
+            let {
+              a1{-reR-} :: ((a{-reT-}, b{-reS-})-> (a{-reT-}, b{-reS-})-> PrelBase.Bool{-3c-})
+              a1{-reR-} = \ a2{-reV-} _Ks :: (a{-reT-}, b{-reS-})
+                            b1{-reU-} _Ks :: (a{-reT-}, b{-reS-}) ->
+                          PrelBase.not{-r6I-} (zeze2{-reN-} a2{-reV-} b1{-reU-})
+            } in
+              PrelBase.zdwZCDEq{-r8J-} @ (a{-reT-}, b{-reS-}) a1{-reR-} zeze2{-reN-})
+
+and it's not as bad as it seems, because it's further dramatically
+simplified: only zeze2 is extracted and its body is simplified.
 
 
 %************************************************************************
@@ -143,7 +304,7 @@ tcInstDecls1    -- Deal with both source-code and imported instance decls
    -> [LInstDecl Name]          -- Source code instance decls
    -> [LDerivDecl Name]         -- Source code stand-alone deriving decls
    -> TcM (TcGblEnv,            -- The full inst env
-           [InstInfo],          -- Source-code instance decls to process;
+           [InstInfo Name],     -- Source-code instance decls to process;
                                 -- contains all dfuns for this module
            HsValBinds Name)     -- Supporting bindings for derived instances
 
@@ -155,13 +316,12 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
 
                 -- (1) Do class and family instance declarations
        ; let { idxty_decls = filter (isFamInstDecl . unLoc) tycl_decls }
-       ; local_info_tycons <- mapM tcLocalInstDecl1  inst_decls
-       ; idx_tycons        <- mapM tcIdxTyInstDeclTL idxty_decls
+       ; local_info_tycons <- mapAndRecoverM tcLocalInstDecl1  inst_decls
+       ; idx_tycons        <- mapAndRecoverM tcIdxTyInstDeclTL idxty_decls
 
-       ; let { (local_infos,
-                at_tycons)     = unzip local_info_tycons
-             ; local_info      = concat local_infos
-             ; at_idx_tycon    = concat at_tycons ++ catMaybes idx_tycons
+       ; let { (local_info,
+                at_tycons_s)   = unzip local_info_tycons
+             ; at_idx_tycon    = concat at_tycons_s ++ idx_tycons
              ; clas_decls      = filter (isClassDecl.unLoc) tycl_decls
              ; implicit_things = concatMap implicitTyThings at_idx_tycon
              }
@@ -187,6 +347,9 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
                 -- decl, so it needs to know about all the instances possible
                 -- NB: class instance declarations can contain derivings as
                 --     part of associated data type declarations
+        failIfErrsM            -- If the addInsts stuff gave any errors, don't
+                               -- try the deriving stuff, becuase that may give
+                               -- more errors still
        ; (deriv_inst_info, deriv_binds) <- tcDeriving tycl_decls inst_decls
                                                       deriv_decls
        ; addInsts deriv_inst_info   $ do {
@@ -207,18 +370,18 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
                addErr $ assocInClassErr (tcdName decl)
          ; return tything
          }
-    isAssocFamily (Just (ATyCon tycon)) =
+    isAssocFamily (ATyCon tycon) =
       case tyConFamInst_maybe tycon of
         Nothing       -> panic "isAssocFamily: no family?!?"
         Just (fam, _) -> isTyConAssoc fam
-    isAssocFamily (Just _             ) = panic "isAssocFamily: no tycon?!?"
-    isAssocFamily Nothing               = False
+    isAssocFamily _ = panic "isAssocFamily: no tycon?!?"
 
+assocInClassErr :: Name -> SDoc
 assocInClassErr name =
   ptext (sLit "Associated type") <+> quotes (ppr name) <+>
   ptext (sLit "must be inside a class instance")
 
-addInsts :: [InstInfo] -> TcM a -> TcM a
+addInsts :: [InstInfo Name] -> TcM a -> TcM a
 addInsts infos thing_inside
   = tcExtendLocalInstEnv (map iSpec infos) thing_inside
 
@@ -233,15 +396,13 @@ addFamInsts tycons thing_inside
 
 \begin{code}
 tcLocalInstDecl1 :: LInstDecl Name
-                 -> TcM ([InstInfo], [TyThing]) -- [] if there was an error
+                 -> TcM (InstInfo Name, [TyThing])
         -- A source-file instance declaration
         -- Type-check all the stuff before the "where"
         --
         -- We check for respectable instance type, and context
-tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats))
-  = -- Prime error recovery, set source location
-    recoverM (return ([], []))          $
-    setSrcSpan loc                      $
+tcLocalInstDecl1 (L loc (InstDecl poly_ty binds uprags ats))
+  = setSrcSpan loc                     $
     addErrCtxt (instDeclCtxt1 poly_ty)  $
 
     do  { is_boot <- tcIsHsBoot
@@ -250,27 +411,30 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats))
 
         ; (tyvars, theta, tau) <- tcHsInstHead poly_ty
 
-        -- Next, process any associated types.
-        ; idx_tycons <- mapM tcFamInstDecl ats
-
         -- Now, check the validity of the instance.
         ; (clas, inst_tys) <- checkValidInstHead tau
         ; checkValidInstance tyvars theta clas inst_tys
-        ; checkValidAndMissingATs clas (tyvars, inst_tys)
-                                  (zip ats idx_tycons)
+
+        -- Next, process any associated types.
+        ; idx_tycons <- recoverM (return []) $
+                    do { idx_tycons <- checkNoErrs $ mapAndRecoverM tcFamInstDecl ats
+                       ; checkValidAndMissingATs clas (tyvars, inst_tys)
+                                                 (zip ats idx_tycons)
+                       ; return idx_tycons }
 
         -- Finally, construct the Core representation of the instance.
         -- (This no longer includes the associated types.)
-        ; dfun_name <- newDFunName clas inst_tys loc
+        ; dfun_name <- newDFunName clas inst_tys (getLoc poly_ty)
+               -- Dfun location is that of instance *header*
         ; overlap_flag <- getOverlapFlag
         ; let (eq_theta,dict_theta) = partition isEqPred theta
               theta'         = eq_theta ++ dict_theta
               dfun           = mkDictFunId dfun_name tyvars theta' clas inst_tys
               ispec          = mkLocalInstance dfun overlap_flag
 
-        ; return ([InstInfo { iSpec  = ispec,
-                              iBinds = VanillaInst binds uprags }],
-                  catMaybes idx_tycons)
+        ; return (InstInfo { iSpec  = ispec,
+                              iBinds = VanillaInst binds uprags },
+                  idx_tycons)
         }
   where
     -- We pass in the source form and the type checked form of the ATs.  We
@@ -279,7 +443,7 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats))
     checkValidAndMissingATs :: Class
                             -> ([TyVar], [TcType])     -- instance types
                             -> [(LTyClDecl Name,       -- source form of AT
-                                 Maybe TyThing)]       -- Core form of AT
+                                 TyThing)]            -- Core form of AT
                             -> TcM ()
     checkValidAndMissingATs clas inst_tys ats
       = do { -- Issue a warning for each class AT that is not defined in this
@@ -297,9 +461,7 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats))
            ; mapM_ (checkIndexes clas inst_tys) ats
            }
 
-    checkIndexes _    _        (hsAT, Nothing)             =
-      return () -- skip, we already had an error here
-    checkIndexes clas inst_tys (hsAT, Just (ATyCon tycon)) =
+    checkIndexes clas inst_tys (hsAT, ATyCon tycon) =
 -- !!!TODO: check that this does the Right Thing for indexed synonyms, too!
       checkIndexes' clas inst_tys hsAT
                     (tyConTyVars tycon,
@@ -369,12 +531,12 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats))
 
 %************************************************************************
 %*                                                                      *
-\subsection{Type-checking instance declarations, pass 2}
+      Type-checking instance declarations, pass 2
 %*                                                                      *
 %************************************************************************
 
 \begin{code}
-tcInstDecls2 :: [LTyClDecl Name] -> [InstInfo]
+tcInstDecls2 :: [LTyClDecl Name] -> [InstInfo Name]
              -> TcM (LHsBinds Id, TcLclEnv)
 -- (a) From each class declaration,
 --      generate any default-method bindings
@@ -397,70 +559,9 @@ tcInstDecls2 tycl_decls inst_decls
         ; return (binds, tcl_env) }
 \end{code}
 
-======= New documentation starts here (Sept 92) ==============
-
-The main purpose of @tcInstDecl2@ is to return a @HsBinds@ which defines
-the dictionary function for this instance declaration. For example
-
-        instance Foo a => Foo [a] where
-                op1 x = ...
-                op2 y = ...
-
-might generate something like
-
-        dfun.Foo.List dFoo_a = let op1 x = ...
-                                   op2 y = ...
-                               in
-                                   Dict [op1, op2]
-
-HOWEVER, if the instance decl has no context, then it returns a
-bigger @HsBinds@ with declarations for each method.  For example
-
-        instance Foo [a] where
-                op1 x = ...
-                op2 y = ...
-
-might produce
-
-        dfun.Foo.List a = Dict [Foo.op1.List a, Foo.op2.List a]
-        const.Foo.op1.List a x = ...
-        const.Foo.op2.List a y = ...
-
-This group may be mutually recursive, because (for example) there may
-be no method supplied for op2 in which case we'll get
-
-        const.Foo.op2.List a = default.Foo.op2 (dfun.Foo.List a)
-
-that is, the default method applied to the dictionary at this type.
-What we actually produce in either case is:
-
-        AbsBinds [a] [dfun_theta_dicts]
-                 [(dfun.Foo.List, d)] ++ (maybe) [(const.Foo.op1.List, op1), ...]
-                 { d = (sd1,sd2, ..., op1, op2, ...)
-                   op1 = ...
-                   op2 = ...
-                 }
-
-The "maybe" says that we only ask AbsBinds to make global constant methods
-if the dfun_theta is empty.
-
-For an instance declaration, say,
-
-        instance (C1 a, C2 b) => C (T a b) where
-                ...
-
-where the {\em immediate} superclasses of C are D1, D2, we build a dictionary
-function whose type is
-
-        (C1 a, C2 b, D1 (T a b), D2 (T a b)) => C (T a b)
-
-Notice that we pass it the superclass dictionaries at the instance type; this
-is the ``Mark Jones optimisation''.  The stuff before the "=>" here
-is the @dfun_theta@ below.
-
 
 \begin{code}
-tcInstDecl2 :: InstInfo -> TcM (LHsBinds Id)
+tcInstDecl2 :: InstInfo Name -> TcM (LHsBinds Id)
 -- Returns a binding for the dfun
 
 ------------------------
@@ -470,7 +571,7 @@ tcInstDecl2 :: InstInfo -> TcM (LHsBinds Id)
 --      newtype N a = MkN (Tree [a]) deriving( Foo Int )
 --
 -- The newtype gives an FC axiom looking like
---      axiom CoN a ::  N a :=: Tree [a]
+--      axiom CoN a ::  N a ~ Tree [a]
 --   (see Note [Newtype coercions] in TyCon for this unusual form of axiom)
 --
 -- So all need is to generate a binding looking like:
@@ -487,11 +588,11 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived })
               rigid_info   = InstSkol
               origin       = SigOrigin rigid_info
               inst_ty      = idType dfun_id
-        ; (tvs, theta, inst_head_ty) <- tcSkolSigType rigid_info inst_ty
+        ; (inst_tvs', theta, inst_head_ty) <- tcSkolSigType rigid_info inst_ty
                 -- inst_head_ty is a PredType
 
         ; let (cls, cls_inst_tys) = tcSplitDFunHead inst_head_ty
-              (class_tyvars, sc_theta, _, op_items) = classBigSig cls
+              (class_tyvars, sc_theta, _, _) = classBigSig cls
               cls_tycon = classTyCon cls
               sc_theta' = substTheta (zipOpenTvSubst class_tyvars cls_inst_tys) sc_theta
 
@@ -504,34 +605,39 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived })
               the_coercion = make_coercion cls_tycon initial_cls_inst_tys nt_tycon tc_args
                                 -- Coercion of kind (Foo Int (Tree [a]) ~ Foo Int (N a)
 
-        ; inst_loc   <- getInstLoc origin
         ; sc_loc     <- getInstLoc InstScOrigin
-        ; dfun_dicts <- newDictBndrs inst_loc theta
         ; sc_dicts   <- newDictBndrs sc_loc sc_theta'
+        ; inst_loc   <- getInstLoc origin
+        ; dfun_dicts <- newDictBndrs inst_loc theta
         ; this_dict  <- newDictBndr inst_loc (mkClassPred cls cls_inst_tys)
         ; rep_dict   <- newDictBndr inst_loc rep_pred
 
         -- Figure out bindings for the superclass context from dfun_dicts
         -- Don't include this_dict in the 'givens', else
-        -- wanted_sc_insts get bound by just selecting from this_dict!!
+        -- sc_dicts get bound by just selecting from this_dict!!
         ; sc_binds <- addErrCtxt superClassCtxt $
-                      tcSimplifySuperClasses inst_loc dfun_dicts (rep_dict:sc_dicts)
+                      tcSimplifySuperClasses inst_loc this_dict dfun_dicts 
+                                            (rep_dict:sc_dicts)
 
-        ; let coerced_rep_dict = mkHsWrap the_coercion (HsVar (instToId rep_dict))
+       -- It's possible that the superclass stuff might unified something
+       -- in the envt with one of the clas_tyvars
+       ; checkSigTyVars inst_tvs'
+
+        ; let coerced_rep_dict = wrapId the_coercion (instToId rep_dict)
 
         ; body <- make_body cls_tycon cls_inst_tys sc_dicts coerced_rep_dict
         ; let dict_bind = noLoc $ VarBind (instToId this_dict) (noLoc body)
 
         ; return (unitBag $ noLoc $
-                  AbsBinds  tvs (map instToVar dfun_dicts)
-                            [(tvs, dfun_id, instToId this_dict, [])]
+                  AbsBinds inst_tvs' (map instToVar dfun_dicts)
+                            [(inst_tvs', dfun_id, instToId this_dict, [])]
                             (dict_bind `consBag` sc_binds)) }
   where
       -----------------------
       --        make_coercion
       -- The inst_head looks like (C s1 .. sm (T a1 .. ak))
       -- But we want the coercion (C s1 .. sm (sym (CoT a1 .. ak)))
-      --        with kind (C s1 .. sm (T a1 .. ak)  :=:  C s1 .. sm <rep_ty>)
+      --        with kind (C s1 .. sm (T a1 .. ak)  ~  C s1 .. sm <rep_ty>)
       --        where rep_ty is the (eta-reduced) type rep of T
       -- So we just replace T with CoT, and insert a 'sym'
       -- NB: we know that k will be >= arity of CoT, because the latter fully eta-reduced
@@ -585,7 +691,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
         dfun_id    = instanceDFunId ispec
         rigid_info = InstSkol
         inst_ty    = idType dfun_id
-        loc        = srcLocSpan (getSrcLoc dfun_id)
+        loc        = getSrcSpan dfun_id
     in
          -- Prime error recovery
     recoverM (return emptyLHsBinds)             $
@@ -603,43 +709,38 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
 
         -- Instantiate the super-class context with inst_tys
         sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys') sc_theta
-        (eq_sc_theta',dict_sc_theta')     = partition isEqPred sc_theta'
         origin    = SigOrigin rigid_info
-        (eq_dfun_theta',dict_dfun_theta') = partition isEqPred dfun_theta'
 
          -- Create dictionary Ids from the specified instance contexts.
-    sc_loc        <- getInstLoc InstScOrigin
-    sc_dicts      <- newDictBndrs sc_loc dict_sc_theta'
-    inst_loc      <- getInstLoc origin
-    sc_covars     <- mkMetaCoVars eq_sc_theta'
-    wanted_sc_eqs <- mkEqInsts eq_sc_theta' (map mkWantedCo sc_covars)
-    dfun_covars   <- mkCoVars eq_dfun_theta'
-    dfun_eqs      <- mkEqInsts eq_dfun_theta' (map mkGivenCo $ mkTyVarTys dfun_covars)
-    dfun_dicts    <- newDictBndrs inst_loc dict_dfun_theta'
-    this_dict     <- newDictBndr inst_loc (mkClassPred clas inst_tys')
+    sc_loc      <- getInstLoc InstScOrigin
+    sc_dicts    <- newDictOccs sc_loc sc_theta'                -- These are wanted
+    inst_loc    <- getInstLoc origin
+    dfun_dicts  <- newDictBndrs inst_loc dfun_theta'   -- Includes equalities
+    this_dict   <- newDictBndr inst_loc (mkClassPred clas inst_tys')
                 -- Default-method Ids may be mentioned in synthesised RHSs,
                 -- but they'll already be in the environment.
 
         -- Typecheck the methods
-    let -- These insts are in scope; quite a few, eh?
-        dfun_insts      = dfun_eqs ++ dfun_dicts
-        wanted_sc_insts = wanted_sc_eqs   ++ sc_dicts
-        given_sc_eqs    = map (updateEqInstCoercion (mkGivenCo . TyVarTy . fromWantedCo "tcInstDecl2") ) wanted_sc_eqs
-        given_sc_insts  = given_sc_eqs   ++ sc_dicts
-        avail_insts     = dfun_insts ++ given_sc_insts
-
-    (meth_ids, meth_binds) <- tcMethods origin clas inst_tyvars'
-                                 dfun_theta' inst_tys' this_dict avail_insts
-                                 op_items monobinds uprags
+    let this_dict_id   = instToId this_dict
+       dfun_lam_vars   = map instToVar dfun_dicts      -- Includes equalities
+       prag_fn = mkPragFun uprags 
+       tc_meth = tcInstanceMethod loc clas inst_tyvars'
+                                  dfun_dicts
+                                  dfun_theta' inst_tys'
+                                  this_dict dfun_id
+                                  prag_fn monobinds
+    (meth_exprs, meth_binds) <- tcExtendTyVarEnv inst_tyvars'  $
+                               mapAndUnzipM tc_meth op_items 
 
     -- Figure out bindings for the superclass context
     -- Don't include this_dict in the 'givens', else
-    -- wanted_sc_insts get bound by just selecting  from this_dict!!
-    sc_binds <- addErrCtxt superClassCtxt
-                   (tcSimplifySuperClasses inst_loc dfun_insts wanted_sc_insts)
+    -- sc_dicts get bound by just selecting  from this_dict!!
+    sc_binds <- addErrCtxt superClassCtxt $
+                tcSimplifySuperClasses inst_loc this_dict dfun_dicts sc_dicts
+               -- Note [Recursive superclasses]
 
-    -- It's possible that the superclass stuff might unified one
-    -- of the inst_tyavars' with something in the envt
+       -- It's possible that the superclass stuff might unified something
+       -- in the envt with one of the inst_tyvars'
     checkSigTyVars inst_tyvars'
 
     -- Deal with 'SPECIALISE instance' pragmas
@@ -648,9 +749,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
     -- Create the result bindings
     let
         dict_constr   = classDataCon clas
-        scs_and_meths = map instToId sc_dicts ++ meth_ids
-        this_dict_id  = instToId this_dict
-        inline_prag | null dfun_insts  = []
+        inline_prag | null dfun_dicts  = []
                     | otherwise        = [L loc (InlinePrag (Inline AlwaysActive True))]
                 -- Always inline the dfun; this is an experimental decision
                 -- because it makes a big performance difference sometimes.
@@ -663,8 +762,11 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
                 --
                 --      See Note [Inline dfuns] below
 
-        dict_rhs = mkHsConApp dict_constr (inst_tys' ++ mkTyVarTys sc_covars)
-                                          (map HsVar scs_and_meths)
+        sc_dict_vars  = map instToVar sc_dicts
+        dict_bind     = L loc (VarBind this_dict_id dict_rhs)
+        dict_rhs      = foldl (\ f a -> L loc (HsApp f (L loc a))) inst_constr meth_exprs
+       inst_constr   = L loc $ wrapId (mkWpApps sc_dict_vars <.> mkWpTyApps inst_tys')
+                                      (dataConWrapId dict_constr)
                 -- We don't produce a binding for the dict_constr; instead we
                 -- rely on the simplifier to unfold this saturated application
                 -- We do this rather than generate an HsCon directly, because
@@ -672,178 +774,154 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
                 -- member) are dealt with by the common MkId.mkDataConWrapId code rather
                 -- than needing to be repeated here.
 
-        dict_bind  = noLoc (VarBind this_dict_id dict_rhs)
-        all_binds  = dict_bind `consBag` (sc_binds `unionBags` meth_binds)
 
         main_bind = noLoc $ AbsBinds
-                            (inst_tyvars' ++ dfun_covars)
-                            (map instToId dfun_dicts)
-                            [(inst_tyvars' ++ dfun_covars, dfun_id, this_dict_id, inline_prag ++ prags)]
-                            all_binds
+                            inst_tyvars'
+                            dfun_lam_vars
+                            [(inst_tyvars', dfun_id, this_dict_id, inline_prag ++ prags)]
+                            (dict_bind `consBag` sc_binds)
 
     showLIE (text "instance")
-    return (unitBag main_bind)
+    return (main_bind `consBag` unionManyBags meth_binds)
+\end{code}
 
-mkCoVars :: [PredType] -> TcM [TyVar]
-mkCoVars = newCoVars . map unEqPred
-  where
-    unEqPred (EqPred ty1 ty2) = (ty1, ty2)
-    unEqPred _                = panic "TcInstDcls.mkCoVars"
+Note [Recursive superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See Trac #1470 for why we would *like* to add "this_dict" to the 
+available instances here.  But we can't do so because then the superclases
+get satisfied by selection from this_dict, and that leads to an immediate
+loop.  What we need is to add this_dict to Avails without adding its 
+superclasses, and we currently have no way to do that.
 
-mkMetaCoVars :: [PredType] -> TcM [TyVar]
-mkMetaCoVars = mapM eqPredToCoVar
-  where
-    eqPredToCoVar (EqPred ty1 ty2) = newMetaCoVar ty1 ty2
-    eqPredToCoVar _                = panic "TcInstDcls.mkMetaCoVars"
 
-tcMethods origin clas inst_tyvars' dfun_theta' inst_tys'
-          this_dict extra_insts op_items monobinds uprags = do
-    -- Check that all the method bindings come from this class
-    let
-        sel_names = [idName sel_id | (sel_id, _) <- op_items]
-        bad_bndrs = collectHsBindBinders monobinds `minusList` sel_names
+%************************************************************************
+%*                                                                      *
+      Type-checking an instance method
+%*                                                                      *
+%************************************************************************
 
-    mapM (addErrTc . badMethodErr clas) bad_bndrs
+tcInstanceMethod
+- Make the method bindings, as a [(NonRec, HsBinds)], one per method
+- Remembering to use fresh Name (the instance method Name) as the binder
+- Bring the instance method Ids into scope, for the benefit of tcInstSig
+- Use sig_fn mapping instance method Name -> instance tyvars
+- Ditto prag_fn
+- Use tcValBinds to do the checking
 
-    -- Make the method bindings
-    let
-        mk_method_id (sel_id, _) = mkMethId origin clas sel_id inst_tys'
-
-    (meth_insts, meth_ids) <- mapAndUnzipM mk_method_id op_items
-
-        -- And type check them
-        -- It's really worth making meth_insts available to the tcMethodBind
-        -- Consider     instance Monad (ST s) where
-        --                {-# INLINE (>>) #-}
-        --                (>>) = ...(>>=)...
-        -- If we don't include meth_insts, we end up with bindings like this:
-        --      rec { dict = MkD then bind ...
-        --            then = inline_me (... (GHC.Base.>>= dict) ...)
-        --            bind = ... }
-        -- The trouble is that (a) 'then' and 'dict' are mutually recursive,
-        -- and (b) the inline_me prevents us inlining the >>= selector, which
-        -- would unravel the loop.  Result: (>>) ends up as a loop breaker, and
-        -- is not inlined across modules. Rather ironic since this does not
-        -- happen without the INLINE pragma!
-        --
-        -- Solution: make meth_insts available, so that 'then' refers directly
-        --           to the local 'bind' rather than going via the dictionary.
-        --
-        -- BUT WATCH OUT!  If the method type mentions the class variable, then
-        -- this optimisation is not right.  Consider
-        --      class C a where
-        --        op :: Eq a => a
-        --
-        --      instance C Int where
-        --        op = op
-        -- The occurrence of 'op' on the rhs gives rise to a constraint
-        --      op at Int
-        -- The trouble is that the 'meth_inst' for op, which is 'available', also
-        -- looks like 'op at Int'.  But they are not the same.
-    let
-        prag_fn        = mkPragFun uprags
-        all_insts      = extra_insts ++ catMaybes meth_insts
-        sig_fn n       = Just []        -- No scoped type variables, but every method has
-                                        -- a type signature, in effect, so that we check
-                                        -- the method has the right type
-        tc_method_bind = tcMethodBind origin inst_tyvars' dfun_theta' this_dict 
-                                     all_insts sig_fn prag_fn monobinds
+\begin{code}
+tcInstanceMethod :: SrcSpan -> Class -> [TcTyVar] -> [Inst]
+                -> TcThetaType -> [TcType]
+                -> Inst -> Id
+                -> TcPragFun -> LHsBinds Name 
+                -> (Id, DefMeth)
+                -> TcM (HsExpr Id, LHsBinds Id)
+       -- The returned inst_meth_ids all have types starting
+       --      forall tvs. theta => ...
+
+tcInstanceMethod loc clas tyvars dfun_dicts theta inst_tys 
+                this_dict dfun_id prag_fn binds_in (sel_id, dm_info)
+  = do { cloned_this <- cloneDict this_dict
+               -- Need to clone the dict in case it is floated out, and
+               -- then clashes with its friends
+       ; uniq1 <- newUnique
+       ; let local_meth_name = mkInternalName uniq1 sel_occ loc   -- Same OccName
+             this_dict_bind  = L loc $ VarBind (instToId cloned_this) $ 
+                               L loc $ wrapId meth_wrapper dfun_id
+             mb_this_bind | null tyvars = Nothing
+                          | otherwise   = Just (cloned_this, this_dict_bind)
+               -- Only need the this_dict stuff if there are type variables
+               -- involved; otherwise overlap is not possible
+               -- See Note [Subtle interaction of recursion and overlap]       
+
+             tc_body rn_bind = do { (meth_id, tc_binds) <- tcInstanceMethodBody 
+                                               InstSkol clas tyvars dfun_dicts theta inst_tys
+                                               mb_this_bind sel_id 
+                                               local_meth_name
+                                               meth_sig_fn meth_prag_fn rn_bind
+                                  ; return (wrapId meth_wrapper meth_id, tc_binds) }
+
+       ; case (findMethodBind sel_name local_meth_name binds_in, dm_info) of
+               -- There is a user-supplied method binding, so use it
+           (Just user_bind, _) -> tc_body user_bind
+
+               -- The user didn't supply a method binding, so we have to make 
+               -- up a default binding, in a way depending on the default-method info
+
+           (Nothing, GenDefMeth) -> do         -- Derivable type classes stuff
+                       { meth_bind <- mkGenericDefMethBind clas inst_tys sel_id local_meth_name
+                       ; tc_body meth_bind }
+
+           (Nothing, NoDefMeth) -> do          -- No default method in the class
+                       { warn <- doptM Opt_WarnMissingMethods          
+                        ; warnTc (warn  -- Warn only if -fwarn-missing-methods
+                                 && reportIfUnused (getOccName sel_id))
+                                       -- Don't warn about _foo methods
+                                omitted_meth_warn
+                       ; return (error_rhs, emptyBag) }
+
+           (Nothing, DefMeth) -> do    -- An polymorphic default method
+                       {   -- Build the typechecked version directly, 
+                           -- without calling typecheck_method; 
+                           -- see Note [Default methods in instances]
+                         dm_name <- lookupImportedName (mkDefMethRdrName sel_name)
+                                       -- Might not be imported, but will be an OrigName
+                       ; dm_id   <- tcLookupId dm_name
+                       ; return (wrapId dm_wrapper dm_id, emptyBag) } }
+  where
+    sel_name = idName sel_id
+    sel_occ  = nameOccName sel_name
+    this_dict_id = instToId this_dict
 
-    meth_binds_s <- zipWithM tc_method_bind op_items meth_ids
+    meth_prag_fn _ = prag_fn sel_name
+    meth_sig_fn _  = Just []   -- The 'Just' says "yes, there's a type sig"
+                       -- But there are no scoped type variables from local_method_id
+                       -- Only the ones from the instance decl itself, which are already
+                       -- in scope.  Example:
+                       --      class C a where { op :: forall b. Eq b => ... }
+                       --      instance C [c] where { op = <rhs> }
+                       -- In <rhs>, 'c' is scope but 'b' is not!
 
-    return (meth_ids, unionManyBags meth_binds_s)
-\end{code}
+    error_rhs    = HsApp error_fun error_msg
+    error_fun    = L loc $ wrapId (WpTyApp meth_tau) nO_METHOD_BINDING_ERROR_ID
+    error_msg    = L loc (HsLit (HsStringPrim (mkFastString error_string)))
+    meth_tau     = funResultTy (applyTys (idType sel_id) inst_tys)
+    error_string = showSDoc (hcat [ppr loc, text "|", ppr sel_id ])
 
+    dm_wrapper   = WpApp this_dict_id <.> mkWpTyApps inst_tys 
 
-                ------------------------------
-        [Inline dfuns] Inlining dfuns unconditionally
-                ------------------------------
+    omitted_meth_warn :: SDoc
+    omitted_meth_warn = ptext (sLit "No explicit method nor default method for")
+                        <+> quotes (ppr sel_id)
 
-The code above unconditionally inlines dict funs.  Here's why.
-Consider this program:
+    dfun_lam_vars = map instToVar dfun_dicts
+    meth_wrapper = mkWpApps dfun_lam_vars <.> mkWpTyApps (mkTyVarTys tyvars)
 
-    test :: Int -> Int -> Bool
-    test x y = (x,y) == (y,x) || test y x
-    -- Recursive to avoid making it inline.
 
-This needs the (Eq (Int,Int)) instance.  If we inline that dfun
-the code we end up with is good:
+wrapId :: HsWrapper -> id -> HsExpr id
+wrapId wrapper id = mkHsWrap wrapper (HsVar id)
+\end{code}
 
-    Test.$wtest =
-        \r -> case ==# [ww ww1] of wild {
-                PrelBase.False -> Test.$wtest ww1 ww;
-                PrelBase.True ->
-                  case ==# [ww1 ww] of wild1 {
-                    PrelBase.False -> Test.$wtest ww1 ww;
-                    PrelBase.True -> PrelBase.True [];
-                  };
-            };
-    Test.test = \r [w w1]
-            case w of w2 {
-              PrelBase.I# ww ->
-                  case w1 of w3 { PrelBase.I# ww1 -> Test.$wtest ww ww1; };
-            };
+Note [Default methods in instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
 
-If we don't inline the dfun, the code is not nearly as good:
+   class Baz v x where
+      foo :: x -> x
+      foo y = y
 
-    (==) = case PrelTup.$fEq(,) PrelBase.$fEqInt PrelBase.$fEqInt of tpl {
-              PrelBase.:DEq tpl1 tpl2 -> tpl2;
-            };
+   instance Baz Int Int
 
-    Test.$wtest =
-        \r [ww ww1]
-            let { y = PrelBase.I#! [ww1]; } in
-            let { x = PrelBase.I#! [ww]; } in
-            let { sat_slx = PrelTup.(,)! [y x]; } in
-            let { sat_sly = PrelTup.(,)! [x y];
-            } in
-              case == sat_sly sat_slx of wild {
-                PrelBase.False -> Test.$wtest ww1 ww;
-                PrelBase.True -> PrelBase.True [];
-              };
+From the class decl we get
 
-    Test.test =
-        \r [w w1]
-            case w of w2 {
-              PrelBase.I# ww ->
-                  case w1 of w3 { PrelBase.I# ww1 -> Test.$wtest ww ww1; };
-            };
+   $dmfoo :: forall v x. Baz v x => x -> x
 
-Why doesn't GHC inline $fEq?  Because it looks big:
+Notice that the type is ambiguous.  That's fine, though. The instance decl generates
 
-    PrelTup.zdfEqZ1T{-rcX-}
-        = \ @ a{-reT-} :: * @ b{-reS-} :: *
-            zddEq{-rf6-} _Ks :: {PrelBase.Eq{-23-} a{-reT-}}
-            zddEq1{-rf7-} _Ks :: {PrelBase.Eq{-23-} b{-reS-}} ->
-            let {
-              zeze{-rf0-} _Kl :: (b{-reS-} -> b{-reS-} -> PrelBase.Bool{-3c-})
-              zeze{-rf0-} = PrelBase.zeze{-01L-}@ b{-reS-} zddEq1{-rf7-} } in
-            let {
-              zeze1{-rf3-} _Kl :: (a{-reT-} -> a{-reT-} -> PrelBase.Bool{-3c-})
-              zeze1{-rf3-} = PrelBase.zeze{-01L-} @ a{-reT-} zddEq{-rf6-} } in
-            let {
-              zeze2{-reN-} :: ((a{-reT-}, b{-reS-}) -> (a{-reT-}, b{-reS-})-> PrelBase.Bool{-3c-})
-              zeze2{-reN-} = \ ds{-rf5-} _Ks :: (a{-reT-}, b{-reS-})
-                               ds1{-rf4-} _Ks :: (a{-reT-}, b{-reS-}) ->
-                             case ds{-rf5-}
-                             of wild{-reW-} _Kd { (a1{-rf2-} _Ks, a2{-reZ-} _Ks) ->
-                             case ds1{-rf4-}
-                             of wild1{-reX-} _Kd { (b1{-rf1-} _Ks, b2{-reY-} _Ks) ->
-                             PrelBase.zaza{-r4e-}
-                               (zeze1{-rf3-} a1{-rf2-} b1{-rf1-})
-                               (zeze{-rf0-} a2{-reZ-} b2{-reY-})
-                             }
-                             } } in
-            let {
-              a1{-reR-} :: ((a{-reT-}, b{-reS-})-> (a{-reT-}, b{-reS-})-> PrelBase.Bool{-3c-})
-              a1{-reR-} = \ a2{-reV-} _Ks :: (a{-reT-}, b{-reS-})
-                            b1{-reU-} _Ks :: (a{-reT-}, b{-reS-}) ->
-                          PrelBase.not{-r6I-} (zeze2{-reN-} a2{-reV-} b1{-reU-})
-            } in
-              PrelBase.zdwZCDEq{-r8J-} @ (a{-reT-}, b{-reS-}) a1{-reR-} zeze2{-reN-})
+   $dBazIntInt = MkBaz ($dmfoo Int Int $dBazIntInt)
 
-and it's not as bad as it seems, because it's further dramatically
-simplified: only zeze2 is extracted and its body is simplified.
+BUT this does mean we must generate the dictionary translation directly, rather
+than generating source-code and type-checking it.  That was the bug ing
+Trac #1061. In any case it's less work to generate the translated version!
 
 
 %************************************************************************
@@ -853,29 +931,36 @@ simplified: only zeze2 is extracted and its body is simplified.
 %************************************************************************
 
 \begin{code}
+instDeclCtxt1 :: LHsType Name -> SDoc
 instDeclCtxt1 hs_inst_ty
   = inst_decl_ctxt (case unLoc hs_inst_ty of
                         HsForAllTy _ _ _ (L _ (HsPredTy pred)) -> ppr pred
                         HsPredTy pred                    -> ppr pred
-                        other                            -> ppr hs_inst_ty)     -- Don't expect this
+                        _                                -> ppr hs_inst_ty)     -- Don't expect this
+instDeclCtxt2 :: Type -> SDoc
 instDeclCtxt2 dfun_ty
   = inst_decl_ctxt (ppr (mkClassPred cls tys))
   where
     (_,_,cls,tys) = tcSplitDFunTy dfun_ty
 
+inst_decl_ctxt :: SDoc -> SDoc
 inst_decl_ctxt doc = ptext (sLit "In the instance declaration for") <+> quotes doc
 
+superClassCtxt :: SDoc
 superClassCtxt = ptext (sLit "When checking the super-classes of an instance declaration")
 
+atInstCtxt :: Name -> SDoc
 atInstCtxt name = ptext (sLit "In the associated type instance for") <+>
                   quotes (ppr name)
 
+mustBeVarArgErr :: Type -> SDoc
 mustBeVarArgErr ty =
   sep [ ptext (sLit "Arguments that do not correspond to a class parameter") <+>
         ptext (sLit "must be variables")
       , ptext (sLit "Instead of a variable, found") <+> ppr ty
       ]
 
+wrongATArgErr :: Type -> Type -> SDoc
 wrongATArgErr ty instTy =
   sep [ ptext (sLit "Type indexes must match class instance head")
       , ptext (sLit "Found") <+> ppr ty <+> ptext (sLit "but expected") <+>