Add silent superclass parameters (again)

Silent superclass parameters solve the problem that
the superclasses of a dicionary construction can easily
turn out to be (wrongly) bottom.  The problem and solution
are described in
   Note [Silent superclass arguments] in TcInstDcls

I first implemented this fix (with Dimitrios) in Dec 2010, but removed
it again in Jun 2011 becuase we thought it wasn't necessary any
more. (The reason we thought it wasn't necessary is that we'd stopped
generating derived superclass constraints for *wanteds*.  But we were
wrong; that didn't solve the superclass-loop problem.)

So we have to re-implement it.  It's not hard.  Main features:

  * The IdDetails for a DFunId says how many silent arguments it has

  * A DFunUnfolding describes which dictionary args are
    just parameters (DFunLamArg) and which are a function to apply
    to the parameters (DFunPolyArg).  This adds the DFunArg type
    to CoreSyn

  * Consequential changes to IfaceSyn.  (Binary hi file format changes
    slightly.)

  * TcInstDcls changes to generate the right dfuns

  * CoreSubst.exprIsConApp_maybe handles the new DFunUnfolding

The thing taht is *not* done yet is to alter the vectoriser to
pass the relevant extra argument when building a PA dictionary.

21 files changed, 196 insertions, 85 deletions

diff --git a/compiler/basicTypes/Id.lhs b/compiler/basicTypes/Id.lhs
index e6e221bfce..02987d4656 100644
--- a/compiler/basicTypes/Id.lhs
+++ b/compiler/basicTypes/Id.lhs
@@ -65,7 +65,7 @@ module Id (
         hasNoBinding,
 
 	-- ** Evidence variables
-	DictId, isDictId, isEvVar,
+	DictId, isDictId, dfunNSilent, isEvVar,
 
 	-- ** Inline pragma stuff
 	idInlinePragma, setInlinePragma, modifyInlinePragma,
@@ -342,6 +342,11 @@ isDFunId id = case Var.idDetails id of
                         DFunId {} -> True
                         _         -> False
 
+dfunNSilent :: Id -> Int
+dfunNSilent id = case Var.idDetails id of
+                   DFunId ns _ -> ns
+                   _ -> pprPanic "dfunSilent: not a dfun:" (ppr id)
+
 isPrimOpId_maybe id = case Var.idDetails id of
                         PrimOpId op -> Just op
                         _           -> Nothing
diff --git a/compiler/basicTypes/IdInfo.lhs b/compiler/basicTypes/IdInfo.lhs
index 3f5eaa4b5a..89ed243a81 100644
--- a/compiler/basicTypes/IdInfo.lhs
+++ b/compiler/basicTypes/IdInfo.lhs
@@ -136,7 +136,14 @@ data IdDetails
 
   | TickBoxOpId TickBoxOp	-- ^ The 'Id' is for a HPC tick box (both traditional and binary)
 
-  | DFunId Bool                 -- ^ A dictionary function.
+  | DFunId Int Bool             -- ^ A dictionary function.
+       -- Int = the number of "silent" arguments to the dfun
+       --       e.g.  class D a => C a where ...
+       --             instance C a => C [a]
+       --       has is_silent = 1, because the dfun
+       --       has type  dfun :: (D a, C a) => C [a]
+       --       See the DFun Superclass Invariant in TcInstDcls
+       --
        -- Bool = True <=> the class has only one method, so may be
        --                  implemented with a newtype, so it might be bad
        --                  to be strict on this dictionary
@@ -158,7 +165,8 @@ pprIdDetails other     = brackets (pp other)
    pp (PrimOpId _)      = ptext (sLit "PrimOp")
    pp (FCallId _)       = ptext (sLit "ForeignCall")
    pp (TickBoxOpId _)   = ptext (sLit "TickBoxOp")
-   pp (DFunId nt)       = ptext (sLit "DFunId")
+   pp (DFunId ns nt)    = ptext (sLit "DFunId")
+                             <> ppWhen (ns /= 0) (brackets (int ns))
                              <> ppWhen nt (ptext (sLit "(nt)"))
    pp (RecSelId { sel_naughty = is_naughty })
       			 = brackets $ ptext (sLit "RecSel") 
diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index 3eaa7dceb5..c1127da18f 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -826,17 +826,29 @@ mkDictFunId :: Name      -- Name to use for the dict fun;
 -- Implements the DFun Superclass Invariant (see TcInstDcls)
 
 mkDictFunId dfun_name tvs theta clas tys
-  = mkExportedLocalVar (DFunId is_nt)
+  = mkExportedLocalVar (DFunId n_silent is_nt)
                        dfun_name
                        dfun_ty
                        vanillaIdInfo
   where
     is_nt = isNewTyCon (classTyCon clas)
-    dfun_ty = mkDictFunTy tvs theta clas tys
+    (n_silent, dfun_ty) = mkDictFunTy tvs theta clas tys
 
-mkDictFunTy :: [TyVar] -> ThetaType -> Class -> [Type] -> Type
+mkDictFunTy :: [TyVar] -> ThetaType -> Class -> [Type] -> (Int, Type)
 mkDictFunTy tvs theta clas tys
-  = mkSigmaTy tvs theta (mkClassPred clas tys)
+  = (length silent_theta, dfun_ty)
+  where
+    dfun_ty = mkSigmaTy tvs (silent_theta ++ theta) (mkClassPred clas tys)
+    silent_theta 
+      | null tvs, null theta 
+      = []
+      | otherwise
+      = filterOut discard $
+        substTheta (zipTopTvSubst (classTyVars clas) tys)
+                   (classSCTheta clas)
+                   -- See Note [Silent Superclass Arguments]
+    discard pred = any (`eqPred` pred) theta
+                 -- See the DFun Superclass Invariant in TcInstDcls
 \end{code}
 
 
diff --git a/compiler/coreSyn/CoreFVs.lhs b/compiler/coreSyn/CoreFVs.lhs
index eb3cd5e948..d2bb6ed57a 100644
--- a/compiler/coreSyn/CoreFVs.lhs
+++ b/compiler/coreSyn/CoreFVs.lhs
@@ -442,7 +442,7 @@ stableUnfoldingVars fv_cand unf
   = case unf of
       CoreUnfolding { uf_tmpl = rhs, uf_src = src }
          | isStableSource src -> Just (exprSomeFreeVars fv_cand rhs)
-      DFunUnfolding _ _ args  -> Just (exprsSomeFreeVars fv_cand args)
+      DFunUnfolding _ _ args  -> Just (exprsSomeFreeVars fv_cand (dfunArgExprs args))
       _other                  -> Nothing
 \end{code}
 
diff --git a/compiler/coreSyn/CoreSubst.lhs b/compiler/coreSyn/CoreSubst.lhs
index 16173fb332..a8de9c2b16 100644
--- a/compiler/coreSyn/CoreSubst.lhs
+++ b/compiler/coreSyn/CoreSubst.lhs
@@ -658,7 +658,7 @@ substUnfoldingSC subst unf 	 -- Short-cut version
 substUnfolding subst (DFunUnfolding ar con args)
   = DFunUnfolding ar con (map subst_arg args)
   where
-    subst_arg = substExpr (text "dfun-unf") subst
+    subst_arg = fmap (substExpr (text "dfun-unf") subst)
 
 substUnfolding subst unf@(CoreUnfolding { uf_tmpl = tmpl, uf_src = src })
 	-- Retain an InlineRule!
@@ -1194,7 +1194,8 @@ exprIsConApp_maybe id_unf expr
         , length args == dfun_nargs    -- See Note [DFun arity check]
         , let (dfun_tvs, _n_theta, _cls, dfun_res_tys) = tcSplitDFunTy (idType fun)
               subst    = zipOpenTvSubst dfun_tvs (stripTypeArgs (takeList dfun_tvs args))
-              mk_arg e = mkApps e args
+              mk_arg (DFunPolyArg e) = mkApps e args
+              mk_arg (DFunLamArg i)  = args !! i
         = dealWithCoercion co (con, substTys subst dfun_res_tys, map mk_arg ops)
 
         -- Look through unfoldings, but only arity-zero one; 
diff --git a/compiler/coreSyn/CoreSyn.lhs b/compiler/coreSyn/CoreSyn.lhs
index e52a6cfe45..a84a29a6c0 100644
--- a/compiler/coreSyn/CoreSyn.lhs
+++ b/compiler/coreSyn/CoreSyn.lhs
@@ -49,6 +49,7 @@ module CoreSyn (
 
         -- * Unfolding data types
         Unfolding(..),  UnfoldingGuidance(..), UnfoldingSource(..),
+        DFunArg(..), dfunArgExprs,
 
 	-- ** Constructing 'Unfolding's
 	noUnfolding, evaldUnfolding, mkOtherCon,
@@ -635,7 +636,7 @@ data Unfolding
 
         DataCon 	-- The dictionary data constructor (possibly a newtype datacon)
 
-        [CoreExpr]      -- Specification of superclasses and methods, in positional order
+        [DFunArg CoreExpr]  -- Specification of superclasses and methods, in positional order
 
   | CoreUnfolding {		-- An unfolding for an Id with no pragma, 
                                 -- or perhaps a NOINLINE pragma
@@ -673,6 +674,21 @@ data Unfolding
   --  uf_guidance:  Tells us about the /size/ of the unfolding template
 
 ------------------------------------------------
+data DFunArg e   -- Given (df a b d1 d2 d3)
+  = DFunPolyArg  e      -- Arg is (e a b d1 d2 d3)
+  | DFunLamArg   Int    -- Arg is one of [a,b,d1,d2,d3], zero indexed
+  deriving( Functor )
+
+  -- 'e' is often CoreExpr, which are usually variables, but can
+  -- be trivial expressions instead (e.g. a type application).
+
+dfunArgExprs :: [DFunArg e] -> [e]
+dfunArgExprs []                    = []
+dfunArgExprs (DFunPolyArg  e : as) = e : dfunArgExprs as
+dfunArgExprs (DFunLamArg {}  : as) = dfunArgExprs as
+
+
+------------------------------------------------
 data UnfoldingSource
   = InlineRhs          -- The current rhs of the function
     		       -- Replace uf_tmpl each time around
diff --git a/compiler/coreSyn/CoreTidy.lhs b/compiler/coreSyn/CoreTidy.lhs
index 2045538ace..e29c50cc9d 100644
--- a/compiler/coreSyn/CoreTidy.lhs
+++ b/compiler/coreSyn/CoreTidy.lhs
@@ -205,8 +205,8 @@ tidyIdBndr env@(tidy_env, var_env) id
 
 ------------ Unfolding  --------------
 tidyUnfolding :: TidyEnv -> Unfolding -> Unfolding -> Unfolding
-tidyUnfolding tidy_env (DFunUnfolding ar con ids) _
-  = DFunUnfolding ar con (map (tidyExpr tidy_env) ids)
+tidyUnfolding tidy_env (DFunUnfolding ar con args) _
+  = DFunUnfolding ar con (map (fmap (tidyExpr tidy_env)) args)
 tidyUnfolding tidy_env 
               unf@(CoreUnfolding { uf_tmpl = unf_rhs, uf_src = src })
               unf_from_rhs
diff --git a/compiler/coreSyn/CoreUnfold.lhs b/compiler/coreSyn/CoreUnfold.lhs
index 8f62ed439e..816d34e87b 100644
--- a/compiler/coreSyn/CoreUnfold.lhs
+++ b/compiler/coreSyn/CoreUnfold.lhs
@@ -96,7 +96,7 @@ mkImplicitUnfolding expr = mkTopUnfolding False (simpleOptExpr expr)
 mkSimpleUnfolding :: CoreExpr -> Unfolding
 mkSimpleUnfolding = mkUnfolding InlineRhs False False
 
-mkDFunUnfolding :: Type -> [CoreExpr] -> Unfolding
+mkDFunUnfolding :: Type -> [DFunArg CoreExpr] -> Unfolding
 mkDFunUnfolding dfun_ty ops 
   = DFunUnfolding dfun_nargs data_con ops
   where
diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs
index c7dc1a6524..17e2966e15 100644
--- a/compiler/coreSyn/CoreUtils.lhs
+++ b/compiler/coreSyn/CoreUtils.lhs
@@ -928,7 +928,7 @@ expr_ok primop_ok other_expr
 app_ok :: (PrimOp -> Bool) -> Id -> [Expr b] -> Bool
 app_ok primop_ok fun args
   = case idDetails fun of
-      DFunId new_type ->  not new_type
+      DFunId _ new_type ->  not new_type
          -- DFuns terminate, unless the dict is implemented 
          -- with a newtype in which case they may not
 
diff --git a/compiler/coreSyn/PprCore.lhs b/compiler/coreSyn/PprCore.lhs
index 8ac0664b8b..39910c0812 100644
--- a/compiler/coreSyn/PprCore.lhs
+++ b/compiler/coreSyn/PprCore.lhs
@@ -430,6 +430,10 @@ instance Outputable Unfolding where
              | otherwise          = empty
             -- Don't print the RHS or we get a quadratic
             -- blowup in the size of the printout!
+
+instance Outputable e => Outputable (DFunArg e) where
+  ppr (DFunPolyArg e) = braces (ppr e)
+  ppr (DFunLamArg i)  = char '<' <> int i <> char '>'
 \end{code}
 
 -----------------------------------------------------
diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs
index f749f97cdb..201e7bb900 100644
--- a/compiler/iface/BinIface.hs
+++ b/compiler/iface/BinIface.hs
@@ -23,6 +23,7 @@ import TyCon      (TyCon, tyConName, tupleTyConSort, tupleTyConArity, isTupleTyC
 import DataCon    (dataConName, dataConWorkId, dataConTyCon)
 import PrelInfo   (wiredInThings, basicKnownKeyNames)
 import Id         (idName, isDataConWorkId_maybe)
+import CoreSyn    (DFunArg(..))
 import TysWiredIn
 import IfaceEnv
 import HscTypes
@@ -1180,13 +1181,21 @@ instance Binary IfaceBinding where
 instance Binary IfaceIdDetails where
     put_ bh IfVanillaId      = putByte bh 0
     put_ bh (IfRecSelId a b) = putByte bh 1 >> put_ bh a >> put_ bh b
-    put_ bh IfDFunId         = putByte bh 2
+    put_ bh (IfDFunId n)     = do { putByte bh 2; put_ bh n }
     get bh = do
         h <- getByte bh
         case h of
             0 -> return IfVanillaId
             1 -> do { a <- get bh; b <- get bh; return (IfRecSelId a b) }
-            _ -> return IfDFunId
+            _ -> do { n <- get bh; return (IfDFunId n) }
+
+instance Binary (DFunArg IfaceExpr) where
+    put_ bh (DFunPolyArg  e) = putByte bh 0 >> put_ bh e
+    put_ bh (DFunLamArg i)   = putByte bh 1 >> put_ bh i
+    get bh = do { h <- getByte bh
+                ; case h of
+                    0 -> do { a <- get bh; return (DFunPolyArg a) }
+                    _ -> do { a <- get bh; return (DFunLamArg a) } }
 
 instance Binary IfaceIdInfo where
     put_ bh NoInfo      = putByte bh 0
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index b53398da7d..bc5fc954eb 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -35,6 +35,8 @@ module IfaceSyn (
 #include "HsVersions.h"
 
 import IfaceType
+import CoreSyn( DFunArg, dfunArgExprs )
+import PprCore()            -- Printing DFunArgs
 import Demand
 import Annotations
 import Class
@@ -194,7 +196,7 @@ type IfaceAnnTarget = AnnTarget OccName
 data IfaceIdDetails
   = IfVanillaId
   | IfRecSelId IfaceTyCon Bool
-  | IfDFunId 
+  | IfDFunId Int          -- Number of silent args
 
 data IfaceIdInfo
   = NoInfo                      -- When writing interface file without -O
@@ -237,7 +239,7 @@ data IfaceUnfolding
   | IfLclWrapper Arity IfLclName  --     because the worker can simplify to a function in
                                   --     another module.
 
-  | IfDFunUnfold [IfaceExpr]
+  | IfDFunUnfold [DFunArg IfaceExpr]
 
 --------------------------------
 data IfaceExpr
@@ -701,7 +703,7 @@ instance Outputable IfaceIdDetails where
   ppr IfVanillaId       = empty
   ppr (IfRecSelId tc b) = ptext (sLit "RecSel") <+> ppr tc
                           <+> if b then ptext (sLit "<naughty>") else empty
-  ppr IfDFunId          = ptext (sLit "DFunId")
+  ppr (IfDFunId ns)     = ptext (sLit "DFunId") <> brackets (int ns)
 
 instance Outputable IfaceIdInfo where
   ppr NoInfo       = empty
@@ -856,7 +858,7 @@ freeNamesIfUnfold (IfCompulsory e)       = freeNamesIfExpr e
 freeNamesIfUnfold (IfInlineRule _ _ _ e) = freeNamesIfExpr e
 freeNamesIfUnfold (IfExtWrapper _ v)     = unitNameSet v
 freeNamesIfUnfold (IfLclWrapper {})      = emptyNameSet
-freeNamesIfUnfold (IfDFunUnfold vs)      = fnList freeNamesIfExpr vs
+freeNamesIfUnfold (IfDFunUnfold vs)      = fnList freeNamesIfExpr (dfunArgExprs vs)
 
 freeNamesIfExpr :: IfaceExpr -> NameSet
 freeNamesIfExpr (IfaceExt v)      = unitNameSet v
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index 1ff9a48c24..91651829b7 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -1643,7 +1643,7 @@ toIfaceLetBndr id  = IfLetBndr (occNameFS (getOccName id))
 --------------------------
 toIfaceIdDetails :: IdDetails -> IfaceIdDetails
 toIfaceIdDetails VanillaId                      = IfVanillaId
-toIfaceIdDetails (DFunId {})                    = IfDFunId 
+toIfaceIdDetails (DFunId ns _)                  = IfDFunId ns
 toIfaceIdDetails (RecSelId { sel_naughty = n
                            , sel_tycon = tc })  = IfRecSelId (toIfaceTyCon tc) n
 toIfaceIdDetails other                          = pprTrace "toIfaceIdDetails" (ppr other) 
@@ -1708,7 +1708,7 @@ toIfUnfolding lb (CoreUnfolding { uf_tmpl = rhs, uf_arity = arity
     if_rhs = toIfaceExpr rhs
 
 toIfUnfolding lb (DFunUnfolding _ar _con ops)
-  = Just (HsUnfold lb (IfDFunUnfold (map toIfaceExpr ops)))
+  = Just (HsUnfold lb (IfDFunUnfold (map (fmap toIfaceExpr) ops)))
       -- No need to serialise the data constructor; 
       -- we can recover it from the type of the dfun
 
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index e63bf7268f..80c2029a70 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -1160,8 +1160,8 @@ do_one (IfaceRec pairs) thing_inside
 \begin{code}
 tcIdDetails :: Type -> IfaceIdDetails -> IfL IdDetails
 tcIdDetails _  IfVanillaId = return VanillaId
-tcIdDetails ty IfDFunId
-  = return (DFunId (isNewTyCon (classTyCon cls)))
+tcIdDetails ty (IfDFunId ns)
+  = return (DFunId ns (isNewTyCon (classTyCon cls)))
   where
     (_, _, cls, _) = tcSplitDFunTy ty
 
@@ -1225,12 +1225,14 @@ tcUnfolding name _ _ (IfInlineRule arity unsat_ok boring_ok if_expr)
     }
 
 tcUnfolding name dfun_ty _ (IfDFunUnfold ops)
-  = do { mb_ops1 <- forkM_maybe doc $ mapM tcIfaceExpr ops
+  = do { mb_ops1 <- forkM_maybe doc $ mapM tc_arg ops
        ; return (case mb_ops1 of
                     Nothing   -> noUnfolding
                     Just ops1 -> mkDFunUnfolding dfun_ty ops1) }
   where
     doc = text "Class ops for dfun" <+> ppr name
+    tc_arg (DFunPolyArg  e) = do { e' <- tcIfaceExpr e; return (DFunPolyArg e') }
+    tc_arg (DFunLamArg i)   = return (DFunLamArg i)
 
 tcUnfolding name ty info (IfExtWrapper arity wkr)
   = tcIfaceWrapper name ty info arity (tcIfaceExtId wkr)
diff --git a/compiler/main/TidyPgm.lhs b/compiler/main/TidyPgm.lhs
index 43a2db1e91..8e4e7dd0a0 100644
--- a/compiler/main/TidyPgm.lhs
+++ b/compiler/main/TidyPgm.lhs
@@ -882,7 +882,7 @@ dffvLetBndr vanilla_unfold id
             -- but I've seen cases where we had a wrapper id $w but a
             -- rhs where $w had been inlined; see Trac #3922
 
-    go_unf (DFunUnfolding _ _ args) = mapM_ dffvExpr args
+    go_unf (DFunUnfolding _ _ args) = mapM_ dffvExpr (dfunArgExprs args)
     go_unf _ = return ()
 
     go_rule (BuiltinRule {}) = return ()
diff --git a/compiler/simplCore/Simplify.lhs b/compiler/simplCore/Simplify.lhs
index fca2f1fff9..115dd94bd4 100644
--- a/compiler/simplCore/Simplify.lhs
+++ b/compiler/simplCore/Simplify.lhs
@@ -731,7 +731,7 @@ simplUnfolding :: SimplEnv-> TopLevelFlag
 simplUnfolding env _ _ _ (DFunUnfolding ar con ops)
   = return (DFunUnfolding ar con ops')
   where
-    ops' = map (substExpr (text "simplUnfolding") env) ops
+    ops' = map (fmap (substExpr (text "simplUnfolding") env)) ops
 
 simplUnfolding env top_lvl id _
     (CoreUnfolding { uf_tmpl = expr, uf_arity = arity
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index ff774fa37b..1a5811b531 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -680,6 +680,9 @@ mkDictErr ctxt cts
 
        -- Report definite no-instance errors, 
        -- or (iff there are none) overlap errors
+       -- But we report only one of them (hence 'head') becuase they all
+       -- have the same source-location origin, to try avoid a cascade
+       -- of error from one location
        ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
        ; mkErrorReport ctxt err }
   where
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index 49c5131275..9eb747ad51 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -39,6 +39,7 @@ import TcEnv
 import TcHsType
 import TcUnify
 import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
+import CoreSyn    ( DFunArg(..) )
 import Type
 import TcEvidence
 import TyCon
@@ -49,7 +50,7 @@ import VarEnv
 import VarSet     ( mkVarSet, subVarSet, varSetElems )
 import Pair
 import CoreUnfold ( mkDFunUnfolding )
-import CoreSyn    ( Expr(Var), CoreExpr, varToCoreExpr )
+import CoreSyn    ( Expr(Var), CoreExpr )
 import PrelNames  ( typeableClassNames )
 
 import Bag
@@ -731,13 +732,13 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                      -- See Note [Subtle interaction of recursion and overlap]
                      -- and Note [Binding when looking up instances]
        ; let (clas, inst_tys) = tcSplitDFunHead inst_head
-             (class_tyvars, sc_theta, sc_sels, op_items) = classBigSig clas
+             (class_tyvars, sc_theta, _, op_items) = classBigSig clas
              sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys) sc_theta
+
        ; dfun_ev_vars <- newEvVars dfun_theta
 
-       ; (sc_args, sc_binds)
-             <- mapAndUnzipM (tcSuperClass inst_tyvars dfun_ev_vars)
-                              (sc_sels `zip` sc_theta')
+       ; (sc_binds, sc_ev_vars, sc_dfun_args) 
+            <- tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta'
 
        -- Deal with 'SPECIALISE instance' pragmas
        -- See Note [SPECIALISE instance pragmas]
@@ -770,20 +771,14 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                      --    con_app_args = MkD ty1 ty2 sc1 sc2 op1 op2
              con_app_tys  = wrapId (mkWpTyApps inst_tys)
                                    (dataConWrapId dict_constr)
-             con_app_scs  = mkHsWrap (mkWpEvApps (map mk_sc_ev_term sc_args)) con_app_tys
+             con_app_scs  = mkHsWrap (mkWpEvApps (map EvId sc_ev_vars)) con_app_tys
              con_app_args = foldl mk_app con_app_scs $
                             map (wrapId arg_wrapper) meth_ids
 
              mk_app :: HsExpr Id -> HsExpr Id -> HsExpr Id
              mk_app fun arg = HsApp (L loc fun) (L loc arg)
 
-             mk_sc_ev_term :: EvVar -> EvTerm
-             mk_sc_ev_term sc
-               | null inst_tv_tys
-               , null dfun_ev_vars = EvId sc
-               | otherwise         = EvDFunApp sc inst_tv_tys (map EvId dfun_ev_vars)
-
-             inst_tv_tys    = mkTyVarTys inst_tyvars
+             inst_tv_tys = mkTyVarTys inst_tyvars
              arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
 
                 -- Do not inline the dfun; instead give it a magic DFunFunfolding
@@ -796,9 +791,8 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                 = dfun_id `setIdUnfolding`  mkDFunUnfolding dfun_ty dfun_args
                           `setInlinePragma` dfunInlinePragma
 
-             dfun_args :: [CoreExpr]
-             dfun_args = map varToCoreExpr sc_args ++
-                         map Var           meth_ids
+             dfun_args :: [DFunArg CoreExpr]
+             dfun_args = sc_dfun_args ++ map (DFunPolyArg . Var) meth_ids
 
              export = ABE { abe_wrap = idHsWrapper, abe_poly = dfun_id_w_fun
                           , abe_mono = self_dict, abe_prags = noSpecPrags }
@@ -806,12 +800,11 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
              main_bind = AbsBinds { abs_tvs = inst_tyvars
                                   , abs_ev_vars = dfun_ev_vars
                                   , abs_exports = [export]
-                                  , abs_ev_binds = emptyTcEvBinds
+                                  , abs_ev_binds = sc_binds
                                   , abs_binds = unitBag dict_bind }
 
        ; return (unitBag (L loc main_bind) `unionBags`
-                 listToBag meth_binds      `unionBags`
-                 unionManyBags sc_binds)
+                 listToBag meth_binds)
        }
  where
    dfun_ty   = idType dfun_id
@@ -819,6 +812,31 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
    loc       = getSrcSpan dfun_id
 
 ------------------------------
+tcSuperClasses :: DFunId -> [TcTyVar] -> [EvVar] -> TcThetaType
+               -> TcM (TcEvBinds, [EvVar], [DFunArg CoreExpr])
+-- See Note [Silent superclass arguments]
+tcSuperClasses dfun_id inst_tyvars dfun_ev_vars sc_theta
+  = do {   -- Check that all superclasses can be deduced from
+           -- the originally-specified dfun arguments
+       ; (sc_binds, sc_evs) <- checkConstraints InstSkol inst_tyvars orig_ev_vars $
+                               emitWanteds ScOrigin sc_theta
+
+       ; if null inst_tyvars && null dfun_ev_vars 
+         then return (sc_binds,       sc_evs,      map (DFunPolyArg . Var) sc_evs)
+         else return (emptyTcEvBinds, sc_lam_args, sc_dfun_args) }
+  where
+    n_silent     = dfunNSilent dfun_id
+    n_tv_args    = length inst_tyvars
+    orig_ev_vars = drop n_silent dfun_ev_vars
+
+    (sc_lam_args, sc_dfun_args) = unzip (map (find n_tv_args dfun_ev_vars) sc_theta)
+    find _ [] pred 
+      = pprPanic "tcInstDecl2" (ppr dfun_id $$ ppr (idType dfun_id) $$ ppr pred)
+    find i (ev:evs) pred 
+      | pred `eqPred` evVarPred ev = (ev, DFunLamArg i)
+      | otherwise                  = find (i+1) evs pred
+
+----------------------
 mkMethIds :: HsSigFun -> Class -> [TcTyVar] -> [EvVar] 
           -> [TcType] -> Id -> TcM (TcId, TcSigInfo)
 mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id
@@ -875,33 +893,6 @@ misplacedInstSig name hs_ty
          , ptext (sLit "(Use -XInstanceSigs to allow this)") ]
 
 ------------------------------
-tcSuperClass :: [TcTyVar] -> [EvVar]
-             -> (Id, PredType)
-             -> TcM (TcId, LHsBinds TcId)
-
--- Build a top level decl like
---      sc_op = /\a \d. let sc = ... in
---                      sc
--- and return sc_op, that binding
-
-tcSuperClass tyvars ev_vars (sc_sel, sc_pred)
-  = do { (ev_binds, sc_dict)
-             <- newImplication InstSkol tyvars ev_vars $
-                emitWanted ScOrigin sc_pred
-
-       ; uniq <- newUnique
-       ; let sc_op_ty   = mkForAllTys tyvars $ mkPiTypes ev_vars (varType sc_dict)
-             sc_op_name = mkDerivedInternalName mkClassOpAuxOcc uniq
-                                                (getName sc_sel)
-             sc_op_id   = mkLocalId sc_op_name sc_op_ty
-             sc_op_bind = mkVarBind sc_op_id (L noSrcSpan $ wrapId sc_wrapper sc_dict)
-             sc_wrapper = mkWpTyLams tyvars
-                          <.> mkWpLams ev_vars
-                          <.> mkWpLet ev_binds
-
-       ; return (sc_op_id, unitBag sc_op_bind) }
-
-------------------------------
 tcSpecInstPrags :: DFunId -> InstBindings Name
                 -> TcM ([Located TcSpecPrag], PragFun)
 tcSpecInstPrags _ (NewTypeDerived {})
@@ -913,8 +904,17 @@ tcSpecInstPrags dfun_id (VanillaInst binds uprags _)
        ; return (spec_inst_prags, mkPragFun uprags binds) }
 \end{code}
 
-Note [Superclass loop avoidance]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Silent superclass arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See Trac #3731, #4809, #5751, #5913, #6117, which all
+describe somewhat more complicated situations, but ones
+encountered in practice.  
+
+      THE PROBLEM
+
+The problem is that it is all too easy to create a class whose
+superclass is bottom when it should not be.
+
 Consider the following (extreme) situation:
         class C a => D a where ...
         instance D [a] => D [a] where ...
@@ -929,10 +929,51 @@ argument:
        dfun :: forall a. D [a] -> D [a]
        dfun = \d::D [a] -> MkD (scsel d) ..
 
-Rather, we want to get it by finding an instance for (C [a]).  We
-achieve this by
-    not making the superclasses of a "wanted"
-    available for solving wanted constraints.
+Otherwise if we later encounter a situation where
+we have a [Wanted] dw::D [a] we might solve it thus:
+     dw := dfun dw
+Which is all fine except that now ** the superclass C is bottom **!
+
+      THE SOLUTION
+
+Our solution to this problem "silent superclass arguments".  We pass
+to each dfun some ``silent superclass arguments’’, which are the
+immediate superclasses of the dictionary we are trying to
+construct. In our example:
+       dfun :: forall a. C [a] -> D [a] -> D [a]
+       dfun = \(dc::C [a]) (dd::D [a]) -> DOrd dc ...
+Notice teh extra (dc :: C [a]) argument compared to the previous version.
+
+This gives us:
+
+     -----------------------------------------------------------
+     DFun Superclass Invariant
+     ~~~~~~~~~~~~~~~~~~~~~~~~
+     In the body of a DFun, every superclass argument to the
+     returned dictionary is
+       either   * one of the arguments of the DFun,
+       or       * constant, bound at top level
+     -----------------------------------------------------------
+
+This net effect is that it is safe to treat a dfun application as
+wrapping a dictionary constructor around its arguments (in particular,
+a dfun never picks superclasses from the arguments under the
+dictionary constructor). No superclass is hidden inside a dfun
+application.
+
+The extra arguments required to satisfy the DFun Superclass Invariant
+always come first, and are called the "silent" arguments.  DFun types
+are built (only) by MkId.mkDictFunId, so that is where we decide
+what silent arguments are to be added.
+
+In our example, if we had  [Wanted] dw :: D [a] we would get via the instance:
+    dw := dfun d1 d2
+    [Wanted] (d1 :: C [a])
+    [Wanted] (d2 :: D [a])
+
+And now, though we *can* solve: 
+     d2 := dw
+That's fine; and we solve d1:C[a] separately.
 
 Test case SCLoop tests this fix.
 
@@ -980,7 +1021,7 @@ tcSpecInst dfun_id prag@(SpecInstSig hs_ty)
   = addErrCtxt (spec_ctxt prag) $
     do  { let name = idName dfun_id
         ; (tyvars, theta, clas, tys) <- tcHsInstHead SpecInstCtxt hs_ty
-        ; let spec_dfun_ty = mkDictFunTy tyvars theta clas tys
+        ; let (_, spec_dfun_ty) = mkDictFunTy tyvars theta clas tys
 
         ; co_fn <- tcSubType (SpecPragOrigin name) SpecInstCtxt
                              (idType dfun_id) spec_dfun_ty
diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs
index fac61afe65..4f3731ae0d 100644
--- a/compiler/typecheck/TcSplice.lhs
+++ b/compiler/typecheck/TcSplice.lhs
@@ -1296,12 +1296,13 @@ reifyClass cls
 ------------------------------
 reifyClassInstance :: ClsInst -> TcM TH.Dec
 reifyClassInstance i
-  = do { cxt <- reifyCxt theta
+  = do { cxt <- reifyCxt (drop n_silent theta)
        ; thtypes <- reifyTypes types
        ; let head_ty = foldl TH.AppT (TH.ConT (reifyName cls)) thtypes
        ; return $ (TH.InstanceD cxt head_ty []) }
   where
      (_tvs, theta, cls, types) = instanceHead i
+     n_silent = dfunNSilent (instanceDFunId i)
 
 ------------------------------
 reifyFamilyInstance :: FamInst -> TcM TH.Dec
diff --git a/compiler/types/InstEnv.lhs b/compiler/types/InstEnv.lhs
index 21e1acd3e7..388846b8ee 100644
--- a/compiler/types/InstEnv.lhs
+++ b/compiler/types/InstEnv.lhs
@@ -155,8 +155,15 @@ pprInstance ispec
 pprInstanceHdr :: ClsInst -> SDoc
 -- Prints the ClsInst as an instance declaration
 pprInstanceHdr (ClsInst { is_flag = flag, is_dfun = dfun })
-  = ptext (sLit "instance") <+> ppr flag <+> pprSigmaType (idType dfun)
-        -- Print without the for-all, which the programmer doesn't write
+  = getPprStyle $ \ sty ->
+    let theta_to_print
+          | debugStyle sty = theta
+          | otherwise = drop (dfunNSilent dfun) theta
+    in ptext (sLit "instance") <+> ppr flag
+       <+> sep [pprThetaArrowTy theta_to_print, ppr res_ty]
+  where
+    (_, theta, res_ty) = tcSplitSigmaTy (idType dfun)
+       -- Print without the for-all, which the programmer doesn't write
 
 pprInstances :: [ClsInst] -> SDoc
 pprInstances ispecs = vcat (map pprInstance ispecs)
diff --git a/compiler/vectorise/Vectorise/Generic/PADict.hs b/compiler/vectorise/Vectorise/Generic/PADict.hs
index d73bea17ee..5bc25194fc 100644
--- a/compiler/vectorise/Vectorise/Generic/PADict.hs
+++ b/compiler/vectorise/Vectorise/Generic/PADict.hs
@@ -79,7 +79,7 @@ buildPADict vect_tc prepr_ax pdata_tc pdatas_tc repr
           -- Set the unfolding for the inliner.
       ; raw_dfun <- newExportedVar dfun_name dfun_ty
       ; let dfun_unf = mkDFunUnfolding dfun_ty $
-                       map Var method_ids
+                       map (DFunPolyArg . Var) method_ids
             dfun = raw_dfun `setIdUnfolding`  dfun_unf
                             `setInlinePragma` dfunInlinePragma