Overhaul of the rewrite rules
[ghc-hetmet.git] / compiler / typecheck / TcInstDcls.lhs
index 32b51d0..5d1e63a 100644 (file)
@@ -1,64 +1,61 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
-\section[TcInstDecls]{Typechecking instance declarations}
+
+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
 
 #include "HsVersions.h"
 
 import HsSyn
-import TcBinds         ( mkPragFun, tcPrags, badBootDeclErr )
-import TcTyClsDecls     ( tcIdxTyInstDecl )
-import TcClassDcl      ( tcMethodBind, mkMethodBind, badMethodErr, badATErr,
-                         omittedATWarn, tcClassDecl2, getGenericInstances )
+import TcBinds
+import TcTyClsDecls
+import TcClassDcl
 import TcRnMonad       
-import TcMType         ( tcSkolSigType, checkValidInstance,
-                         checkValidInstHead )
-import TcType          ( TcType, mkClassPred, tcSplitSigmaTy,
-                         tcSplitDFunHead,  SkolemInfo(InstSkol),
-                         tcSplitTyConApp, 
-                         tcSplitDFunTy, mkFunTy ) 
-import Inst            ( newDictBndr, newDictBndrs, instToId, showLIE, 
-                         getOverlapFlag, tcExtendLocalInstEnv )
-import InstEnv         ( mkLocalInstance, instanceDFunId )
-import FamInst         ( tcExtendLocalFamInstEnv )
-import FamInstEnv      ( extractFamInsts )
-import TcDeriv         ( tcDeriving )
-import TcEnv           ( InstInfo(..), InstBindings(..), 
-                         newDFunName, tcExtendIdEnv, tcExtendGlobalEnv
-                       )
-import TcHsType                ( kcHsSigType, tcHsKindedType )
-import TcUnify         ( checkSigTyVars )
-import TcSimplify      ( tcSimplifySuperClasses )
-import Type            ( zipOpenTvSubst, substTheta, mkTyConApp, mkTyVarTy,
-                          TyThing(ATyCon), isTyVarTy, tcEqType,
-                          substTys, emptyTvSubst, extendTvSubst )
-import Coercion         ( mkSymCoercion )
-import TyCon            ( TyCon, tyConName, newTyConCo_maybe, tyConTyVars,
-                         isTyConAssoc, tyConFamInst_maybe,
-                         assocTyConArgPoss_maybe )
-import DataCon         ( classDataCon, dataConInstArgTys )
-import Class           ( Class, classTyCon, classBigSig, classATs )
-import Var             ( TyVar, Id, idName, idType, tyVarName )
-import MkId            ( mkDictFunId )
-import Name            ( Name, getSrcLoc, nameOccName )
-import NameSet         ( addListToNameSet, emptyNameSet, minusNameSet,
-                         nameSetToList ) 
-import Maybe           ( fromJust, catMaybes )
-import Monad           ( when )
-import List            ( find )
-import DynFlags                ( DynFlag(Opt_WarnMissingMethods) )
-import SrcLoc          ( srcLocSpan, unLoc, noLoc, Located(..), srcSpanStart,
-                         getLoc)
-import ListSetOps      ( minusList )
-import Util            ( snocView, dropList )
+import TcMType
+import TcType
+import Inst
+import InstEnv
+import FamInst
+import FamInstEnv
+import TcDeriv
+import TcEnv
+import TcHsType
+import TcUnify
+import TcSimplify
+import Type
+import Coercion
+import TyCon
+import TypeRep
+import DataCon
+import Class
+import Var
+import MkId
+import Name
+import NameSet
+import DynFlags
+import SrcLoc
+import ListSetOps
+import Util
 import Outputable
 import Bag
-import BasicTypes      ( Activation( AlwaysActive ), InlineSpec(..) )
-import HscTypes                ( implicitTyThings )
+import BasicTypes
+import HscTypes
 import FastString
+
+import Data.Maybe
+import Control.Monad hiding (zipWithM_, mapAndUnzipM)
+import Data.List
 \end{code}
 
 Typechecking instance declarations is done in two passes. The first
@@ -146,20 +143,20 @@ Gather up the instance declarations from their various sources
 tcInstDecls1   -- Deal with both source-code and imported instance decls
    :: [LTyClDecl Name]         -- For deriving stuff
    -> [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; 
                                -- contains all dfuns for this module
           HsValBinds Name)     -- Supporting bindings for derived instances
 
-tcInstDecls1 tycl_decls inst_decls
+tcInstDecls1 tycl_decls inst_decls deriv_decls
   = checkNoErrs $
     do {        -- Stop if addInstInfos etc discovers any errors
                -- (they recover, so that we get more than one error each
                -- round) 
 
-               -- (1) Do class instance declarations and instances of indexed
-               --     types 
-       ; let { idxty_decls = filter (isIdxTyDecl . unLoc) tycl_decls }
+               -- (1) Do class and family instance declarations
+       ; let { idxty_decls = filter (isFamInstDecl . unLoc) tycl_decls }
        ; local_info_tycons <- mappM tcLocalInstDecl1  inst_decls
        ; idx_tycons        <- mappM tcIdxTyInstDeclTL idxty_decls
 
@@ -190,7 +187,10 @@ tcInstDecls1 tycl_decls inst_decls
                -- (4) Compute instances from "deriving" clauses; 
                -- This stuff computes a context for the derived instance
                -- decl, so it needs to know about all the instances possible
-       ; (deriv_inst_info, deriv_binds) <- tcDeriving tycl_decls
+                -- NB: class instance declarations can contain derivings as
+                --     part of associated data type declarations
+       ; (deriv_inst_info, deriv_binds) <- tcDeriving tycl_decls inst_decls 
+                                                      deriv_decls
        ; addInsts deriv_inst_info   $ do {
 
        ; gbl_env <- getGblEnv
@@ -203,7 +203,7 @@ tcInstDecls1 tycl_decls inst_decls
     -- !!!TODO: Need to perform this check for the TyThing of type functions,
     --         too.
     tcIdxTyInstDeclTL ldecl@(L loc decl) =
-      do { tything <- tcIdxTyInstDecl ldecl
+      do { tything <- tcFamInstDecl ldecl
         ; setSrcSpan loc $
             when (isAssocFamily tything) $
               addErr $ assocInClassErr (tcdName decl)
@@ -226,8 +226,12 @@ addInsts infos thing_inside
 
 addFamInsts :: [TyThing] -> TcM a -> TcM a
 addFamInsts tycons thing_inside
-  = tcExtendLocalFamInstEnv (extractFamInsts tycons) thing_inside
-\end{code} 
+  = tcExtendLocalFamInstEnv (map mkLocalFamInstTyThing tycons) thing_inside
+  where
+    mkLocalFamInstTyThing (ATyCon tycon) = mkLocalFamInst tycon
+    mkLocalFamInstTyThing tything       = pprPanic "TcInstDcls.addFamInsts"
+                                                   (ppr tything)
+\end{code}
 
 \begin{code}
 tcLocalInstDecl1 :: LInstDecl Name 
@@ -246,14 +250,10 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats))
        ; checkTc (not is_boot || (isEmptyLHsBinds binds && null uprags))
                  badBootDeclErr
 
-       -- Typecheck the instance type itself.  We can't use 
-       -- tcHsSigType, because it's not a valid user type.
-       ; kinded_ty <- kcHsSigType poly_ty
-       ; poly_ty'  <- tcHsKindedType kinded_ty
-       ; let (tyvars, theta, tau) = tcSplitSigmaTy poly_ty'
+       ; (tyvars, theta, tau) <- tcHsInstHead poly_ty
        
        -- Next, process any associated types.
-       ; idx_tycons <- mappM tcIdxTyInstDecl ats
+       ; idx_tycons <- mappM tcFamInstDecl ats
 
        -- Now, check the validity of the instance.
        ; (clas, inst_tys) <- checkValidInstHead tau
@@ -263,9 +263,11 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats))
 
        -- Finally, construct the Core representation of the instance.
        -- (This no longer includes the associated types.)
-       ; dfun_name <- newDFunName clas inst_tys (srcSpanStart loc)
+       ; dfun_name <- newDFunName clas inst_tys loc
        ; overlap_flag <- getOverlapFlag
-       ; let dfun           = mkDictFunId dfun_name tyvars theta clas inst_tys
+       ; 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, 
@@ -284,11 +286,11 @@ tcLocalInstDecl1 decl@(L loc (InstDecl poly_ty binds uprags ats))
     checkValidAndMissingATs clas inst_tys ats
       = do { -- Issue a warning for each class AT that is not defined in this
             -- instance.
-          ; let classDefATs = listToNameSet . map tyConName . classATs $ clas
-                 definedATs  = listToNameSet . map (tcdName.unLoc.fst)  $ ats
-                omitted     = classDefATs `minusNameSet` definedATs
+          ; let class_ats   = map tyConName (classATs clas)
+                 defined_ats = listToNameSet . map (tcdName.unLoc.fst)  $ ats
+                omitted     = filterOut (`elemNameSet` defined_ats) class_ats
           ; warn <- doptM Opt_WarnMissingMethods
-          ; mapM_ (warnTc warn . omittedATWarn) (nameSetToList omitted)
+          ; mapM_ (warnTc warn . omittedATWarn) omitted
           
             -- Ensure that all AT indexes that correspond to class parameters
             -- coincide with the types in the instance head.  All remaining
@@ -401,39 +403,37 @@ tcInstDecls2 tycl_decls inst_decls
 
 The main purpose of @tcInstDecl2@ is to return a @HsBinds@ which defines
 the dictionary function for this instance declaration. For example
-\begin{verbatim}
+
        instance Foo a => Foo [a] where
                op1 x = ...
                op2 y = ...
-\end{verbatim}
+
 might generate something like
-\begin{verbatim}
+
        dfun.Foo.List dFoo_a = let op1 x = ...
                                   op2 y = ...
                               in
                                   Dict [op1, op2]
-\end{verbatim}
 
 HOWEVER, if the instance decl has no context, then it returns a
 bigger @HsBinds@ with declarations for each method.  For example
-\begin{verbatim}
+
        instance Foo [a] where
                op1 x = ...
                op2 y = ...
-\end{verbatim}
+
 might produce
-\begin{verbatim}
+
        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 = ...
-\end{verbatim}
+
 This group may be mutually recursive, because (for example) there may
 be no method supplied for op2 in which case we'll get
-\begin{verbatim}
+
        const.Foo.op2.List a = default.Foo.op2 (dfun.Foo.List a)
-\end{verbatim}
-that is, the default method applied to the dictionary at this type.
 
+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]
@@ -445,7 +445,6 @@ What we actually produce in either case is:
 
 The "maybe" says that we only ask AbsBinds to make global constant methods
 if the dfun_theta is empty.
-
                
 For an instance declaration, say,
 
@@ -461,75 +460,75 @@ 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.
 
-First comes the easy case of a non-local instance decl.
-
 
 \begin{code}
 tcInstDecl2 :: InstInfo -> TcM (LHsBinds Id)
 -- Returns a binding for the dfun
 
 ------------------------
--- Derived newtype instances
+-- Derived newtype instances; surprisingly tricky!
 --
--- In the case of a newtype, things are rather easy
 --     class Show a => Foo a b where ...
---     newtype T a = MkT (Tree [a]) deriving( Foo Int )
+--     newtype N a = MkN (Tree [a]) deriving( Foo Int )
+--
 -- The newtype gives an FC axiom looking like
---     axiom CoT a ::  T 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: 
---     dfunFooT :: forall a. (Foo Int (Tree [a], Show (T a)) => Foo Int (T a)
---     dfunFooT = /\a. \(ds:Show (T a)) (df:Foo (Tree [a])).
---               case df `cast` (Foo Int (sym (CoT a))) of
+--     dfunFooT :: forall a. (Foo Int (Tree [a], Show (N a)) => Foo Int (N a)
+--     dfunFooT = /\a. \(ds:Show (N a)) (df:Foo (Tree [a])).
+--               case df `cast` (Foo Int (sym (CoN a))) of
 --                  Foo _ op1 .. opn -> Foo ds op1 .. opn
 --
 -- If there are no superclasses, matters are simpler, because we don't need the case
 -- see Note [Newtype deriving superclasses] in TcDeriv.lhs
 
-tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived mb_preds })
+tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived })
   = do { let dfun_id      = instanceDFunId ispec 
-             rigid_info   = InstSkol dfun_id
+             rigid_info   = InstSkol
              origin       = SigOrigin rigid_info
              inst_ty      = idType dfun_id
        ; (tvs, theta, inst_head_ty) <- tcSkolSigType rigid_info inst_ty
                -- inst_head_ty is a PredType
 
-       ; inst_loc <- getInstLoc origin
-       ; (rep_dict_id : sc_dict_ids, wrap_fn)
-               <- make_wrapper inst_loc tvs theta mb_preds
-               -- Here, we are relying on the order of dictionary 
-               -- arguments built by NewTypeDerived in TcDeriv; 
-               -- namely, that the rep_dict_id comes first
-          
         ; let (cls, cls_inst_tys) = tcSplitDFunHead inst_head_ty
-             the_coercion     = make_coercion cls cls_inst_tys
-              coerced_rep_dict = mkHsCoerce the_coercion (HsVar rep_dict_id)
-
-       ; body <- make_body cls cls_inst_tys inst_head_ty sc_dict_ids coerced_rep_dict
+             (class_tyvars, sc_theta, _, op_items) = classBigSig cls
+             cls_tycon = classTyCon cls
+             sc_theta' = substTheta (zipOpenTvSubst class_tyvars cls_inst_tys) sc_theta
+
+             Just (initial_cls_inst_tys, last_ty) = snocView cls_inst_tys
+             (nt_tycon, tc_args) = tcSplitTyConApp last_ty     -- Can't fail
+             rep_ty              = newTyConInstRhs nt_tycon tc_args
+
+             rep_pred     = mkClassPred cls (initial_cls_inst_tys ++ [rep_ty])
+                               -- In our example, rep_pred is (Foo Int (Tree [a]))
+             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)
               
-        ; return (unitBag (noLoc $ VarBind dfun_id $ noLoc $ mkHsCoerce wrap_fn body)) }
+       ; inst_loc   <- getInstLoc origin
+       ; sc_loc     <- getInstLoc InstScOrigin
+       ; dfun_dicts <- newDictBndrs inst_loc theta
+       ; sc_dicts   <- newDictBndrs sc_loc sc_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_binds <- addErrCtxt superClassCtxt $
+                     tcSimplifySuperClasses inst_loc dfun_dicts (rep_dict:sc_dicts)
+
+       ; let coerced_rep_dict = mkHsWrap the_coercion (HsVar (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 instToId dfun_dicts)
+                           [(tvs, dfun_id, instToId this_dict, [])] 
+                           (dict_bind `consBag` sc_binds)) }
   where
-
-      -----------------------
-      --       make_wrapper
-      -- We distinguish two cases:
-      -- (a) there is no tyvar abstraction in the dfun, so all dicts are constant,
-      --     and the new dict can just be a constant
-      --       (mb_preds = Just preds)
-      -- (b) there are tyvars, so we must make a dict *fun*
-      --       (mb_preds = Nothing)
-      -- See the defn of NewTypeDerived for the meaning of mb_preds
-    make_wrapper inst_loc tvs theta (Just preds)       -- Case (a)
-      = ASSERT( null tvs && null theta )
-       do { dicts <- newDictBndrs inst_loc preds
-          ; extendLIEs dicts
-          ; return (map instToId dicts, idCoercion) }
-    make_wrapper inst_loc tvs theta Nothing    -- Case (b)
-      = do { dicts <- newDictBndrs inst_loc theta
-          ; let dict_ids = map instToId dicts
-          ; return (dict_ids, mkCoTyLams tvs <.> mkCoLams dict_ids) }
-
       -----------------------
       --       make_coercion
       -- The inst_head looks like (C s1 .. sm (T a1 .. ak))
@@ -539,42 +538,44 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived mb_preds })
       -- 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
 
-    make_coercion cls cls_inst_tys
-       | Just (all_tys_but_last, last_ty) <- snocView cls_inst_tys
-       , (tycon, tc_args) <- tcSplitTyConApp last_ty   -- Should not fail
-       , Just co_con <- newTyConCo_maybe tycon
+    make_coercion cls_tycon initial_cls_inst_tys nt_tycon tc_args
+       | Just co_con <- newTyConCo_maybe nt_tycon
        , let co = mkSymCoercion (mkTyConApp co_con tc_args)
-        = ExprCoFn (mkTyConApp cls_tycon (all_tys_but_last ++ [co]))
+        = WpCo (mkTyConApp cls_tycon (initial_cls_inst_tys ++ [co]))
         | otherwise    -- The newtype is transparent; no need for a cast
-        = idCoercion
-       where
-          cls_tycon = classTyCon cls
+        = idHsWrapper
 
       -----------------------
-      --       make_body
-      -- Two cases; see Note [Newtype deriving superclasses] in TcDeriv.lhs
-      -- (a) no superclasses; then we can just use the coerced dict
-      -- (b) one or more superclasses; then new need to do the unpack/repack
+      --     (make_body C tys scs coreced_rep_dict)
+      --               returns 
+      --     (case coerced_rep_dict of { C _ ops -> C scs ops })
+      -- But if there are no superclasses, it returns just coerced_rep_dict
+      -- See Note [Newtype deriving superclasses] in TcDeriv.lhs
        
-    make_body cls cls_inst_tys inst_head_ty sc_dict_ids coerced_rep_dict
-       | null sc_dict_ids              -- Case (a)
+    make_body cls_tycon cls_inst_tys sc_dicts coerced_rep_dict
+       | null sc_dicts         -- Case (a)
        = return coerced_rep_dict
-       | otherwise                     -- Case (b)
+       | otherwise             -- Case (b)
        = do { op_ids            <- newSysLocalIds FSLIT("op") op_tys
             ; dummy_sc_dict_ids <- newSysLocalIds FSLIT("sc") (map idType sc_dict_ids)
             ; let the_pat = ConPatOut { pat_con = noLoc cls_data_con, pat_tvs = [],
                                         pat_dicts = dummy_sc_dict_ids,
                                         pat_binds = emptyLHsBinds,
                                         pat_args = PrefixCon (map nlVarPat op_ids),
-                                        pat_ty = inst_head_ty} 
+                                        pat_ty = pat_ty} 
                   the_match = mkSimpleMatch [noLoc the_pat] the_rhs
                   the_rhs = mkHsConApp cls_data_con cls_inst_tys $
                             map HsVar (sc_dict_ids ++ op_ids)
 
+               -- Warning: this HsCase scrutinises a value with a PredTy, which is
+               --          never otherwise seen in Haskell source code. It'd be
+               --          nicer to generate Core directly!
             ; return (HsCase (noLoc coerced_rep_dict) $
-                      MatchGroup [the_match] (mkFunTy inst_head_ty inst_head_ty)) }
+                      MatchGroup [the_match] (mkFunTy pat_ty pat_ty)) }
        where
-          cls_data_con = classDataCon cls
+         sc_dict_ids  = map instToId sc_dicts
+         pat_ty       = mkTyConApp cls_tycon cls_inst_tys
+          cls_data_con = head (tyConDataCons cls_tycon)
           cls_arg_tys  = dataConInstArgTys cls_data_con cls_inst_tys 
           op_tys       = dropList sc_dict_ids cls_arg_tys
 
@@ -584,12 +585,13 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = NewTypeDerived mb_preds })
 tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
   = let 
        dfun_id    = instanceDFunId ispec
-       rigid_info = InstSkol dfun_id
+       rigid_info = InstSkol
        inst_ty    = idType dfun_id
+       loc        = srcLocSpan (getSrcLoc dfun_id)
     in
         -- Prime error recovery
     recoverM (returnM emptyLHsBinds)           $
-    setSrcSpan (srcLocSpan (getSrcLoc dfun_id))        $
+    setSrcSpan loc                             $
     addErrCtxt (instDeclCtxt2 (idType dfun_id))        $
 
        -- Instantiate the instance decl with skolem constants 
@@ -603,20 +605,30 @@ 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'
     in
         -- Create dictionary Ids from the specified instance contexts.
     getInstLoc InstScOrigin                            `thenM` \ sc_loc -> 
-    newDictBndrs sc_loc sc_theta'                      `thenM` \ sc_dicts ->
+    newDictBndrs sc_loc dict_sc_theta'                 `thenM` \ sc_dicts ->
     getInstLoc origin                                  `thenM` \ inst_loc -> 
-    newDictBndrs inst_loc dfun_theta'                  `thenM` \ dfun_arg_dicts ->
-    newDictBndr inst_loc (mkClassPred clas inst_tys')  `thenM` \ this_dict ->
+    mkMetaCoVars eq_sc_theta'                          `thenM` \ sc_covars ->
+    mkEqInsts eq_sc_theta' (map mkWantedCo sc_covars)  `thenM` \ wanted_sc_eqs ->
+    mkCoVars eq_dfun_theta'                            `thenM` \ dfun_covars ->
+    mkEqInsts eq_dfun_theta' (map mkGivenCo $ mkTyVarTys dfun_covars)  `thenM` \ dfun_eqs    ->
+    newDictBndrs inst_loc dict_dfun_theta'             `thenM` \ dfun_dicts ->
+    newDictBndr inst_loc (mkClassPred clas inst_tys')   `thenM` \ this_dict ->
                -- 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?
-       avail_insts = [this_dict] ++ dfun_arg_dicts ++ sc_dicts
+       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     = [this_dict] ++ dfun_insts ++ given_sc_insts
     in
     tcMethods origin clas inst_tyvars' 
              dfun_theta' inst_tys' avail_insts 
@@ -624,11 +636,10 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
 
        -- Figure out bindings for the superclass context
        -- Don't include this_dict in the 'givens', else
-       -- sc_dicts get bound by just selecting  from this_dict!!
+       -- wanted_sc_insts get bound by just selecting  from this_dict!!
     addErrCtxt superClassCtxt
-       (tcSimplifySuperClasses inst_tyvars'
-                        dfun_arg_dicts
-                        sc_dicts)      `thenM` \ sc_binds ->
+       (tcSimplifySuperClasses inst_loc
+                        dfun_insts wanted_sc_insts)    `thenM` \ sc_binds ->
 
        -- It's possible that the superclass stuff might unified one
        -- of the inst_tyavars' with something in the envt
@@ -642,8 +653,8 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
         dict_constr   = classDataCon clas
        scs_and_meths = map instToId sc_dicts ++ meth_ids
        this_dict_id  = instToId this_dict
-       inline_prag | null dfun_arg_dicts = []
-                   | otherwise = [InlinePrag (Inline AlwaysActive True)]
+       inline_prag | null dfun_insts  = []
+                   | otherwise        = [L loc (InlinePrag (Inline AlwaysActive True))]
                -- Always inline the dfun; this is an experimental decision
                -- because it makes a big performance difference sometimes.
                -- Often it means we can do the method selection, and then
@@ -656,7 +667,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
                --      See Note [Inline dfuns] below
 
        dict_rhs
-         = mkHsConApp dict_constr inst_tys' (map HsVar scs_and_meths)
+         = mkHsConApp dict_constr (inst_tys' ++ mkTyVarTys sc_covars)  (map HsVar scs_and_meths)
                -- 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
@@ -668,15 +679,25 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = VanillaInst monobinds uprags })
        all_binds  = dict_bind `consBag` (sc_binds `unionBags` meth_binds)
 
        main_bind = noLoc $ AbsBinds
-                           inst_tyvars'
-                           (map instToId dfun_arg_dicts)
-                           [(inst_tyvars', dfun_id, this_dict_id, 
-                                           inline_prag ++ prags)] 
+                           (inst_tyvars' ++ dfun_covars)
+                           (map instToId dfun_dicts)
+                           [(inst_tyvars' ++ dfun_covars, dfun_id, this_dict_id, inline_prag ++ prags)] 
                            all_binds
     in
     showLIE (text "instance")          `thenM_`
     returnM (unitBag main_bind)
 
+mkCoVars :: [PredType] -> TcM [TyVar]
+mkCoVars = newCoVars . map unEqPred
+  where
+    unEqPred (EqPred ty1 ty2) = (ty1, ty2)
+    unEqPred _                = panic "TcInstDcls.mkCoVars"
+
+mkMetaCoVars :: [PredType] -> TcM [TyVar]
+mkMetaCoVars = mappM eqPredToCoVar
+  where
+    eqPredToCoVar (EqPred ty1 ty2) = newMetaCoVar ty1 ty2
+    eqPredToCoVar _                = panic "TcInstDcls.mkMetaCoVars"
 
 tcMethods origin clas inst_tyvars' dfun_theta' inst_tys' 
          avail_insts op_items monobinds uprags