Improve error messages from functional dependencies

Reponding to Trac #9612:

 * Track the CtOrigin of a Derived equality, arising from a
   functional dependency

 * And report it clearly in the error stream

This relies on a previous commit, in which I stop dropping Derived
insolubles on the floor.

13 files changed, 268 insertions, 129 deletions

diff --git a/compiler/typecheck/FunDeps.lhs b/compiler/typecheck/FunDeps.lhs
index 5cfd22664a..283886e836 100644
--- a/compiler/typecheck/FunDeps.lhs
+++ b/compiler/typecheck/FunDeps.lhs
@@ -30,6 +30,7 @@ import VarSet
 import VarEnv
 import Outputable
 import ErrUtils( Validity(..), allValid )
+import SrcLoc
 import Util
 import FastString
 
@@ -135,11 +136,11 @@ unification variables when producing the FD constraints.
 Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
 
 \begin{code}
-data Equation
+data Equation loc
    = FDEqn { fd_qtvs :: [TyVar]                 -- Instantiate these type and kind vars to fresh unification vars
            , fd_eqs  :: [FDEq]                  --   and then make these equal
-           , fd_pred1, fd_pred2 :: PredType }   -- The Equation arose from
-                                                -- combining these two constraints
+           , fd_pred1, fd_pred2 :: PredType     -- The Equation arose from combining these two constraints
+           , fd_loc :: loc  }
 
 data FDEq = FDEq { fd_pos      :: Int -- We use '0' for the first position
                  , fd_ty_left  :: Type
@@ -215,14 +216,14 @@ zipAndComputeFDEqs _ _ _ = []
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 improveFromAnother :: PredType -- Template item (usually given, or inert)
                    -> PredType -- Workitem [that can be improved]
-                   -> [Equation]
+                   -> [Equation ()]
 -- Post: FDEqs always oriented from the other to the workitem
 --       Equations have empty quantified variables
 improveFromAnother pred1 pred2
   | Just (cls1, tys1) <- getClassPredTys_maybe pred1
   , Just (cls2, tys2) <- getClassPredTys_maybe pred2
   , tys1 `lengthAtLeast` 2 && cls1 == cls2
-  = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
+  = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = () }
     | let (cls_tvs, cls_fds) = classTvsFds cls1
     , fd <- cls_fds
     , let (ltys1, rs1)  = instFD         fd cls_tvs tys1
@@ -237,15 +238,15 @@ improveFromAnother _ _ = []
 -- Improve a class constraint from instance declarations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-pprEquation :: Equation -> SDoc
+pprEquation :: Equation a -> SDoc
 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
   = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr qtvs),
           nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
 
 improveFromInstEnv :: (InstEnv,InstEnv)
                    -> PredType
-                   -> [Equation] -- Needs to be an Equation because
-                                 -- of quantified variables
+                   -> [Equation SrcSpan] -- Needs to be an Equation because
+                                         -- of quantified variables
 -- Post: Equations oriented from the template (matching instance) to the workitem!
 improveFromInstEnv _inst_env pred
   | not (isClassPred pred)
@@ -256,7 +257,9 @@ improveFromInstEnv inst_env pred
   , let (cls_tvs, cls_fds) = classTvsFds cls
         instances          = classInstances inst_env cls
         rough_tcs          = roughMatchTcs tys
-  = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
+  = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs
+            , fd_pred1 = p_inst, fd_pred2=pred
+            , fd_loc = getSrcSpan (is_dfun ispec) }
     | fd <- cls_fds             -- Iterate through the fundeps first,
                                 -- because there often are none!
     , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 57f9829432..b1165a5e18 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -208,7 +208,7 @@ reportWanteds ctxt wanted@(WC { wc_flat = flats, wc_insol = insols, wc_impl = im
   = do { reportFlats ctxt  (mapBag (tidyCt env) insol_given)
        ; reportFlats ctxt1 (mapBag (tidyCt env) insol_wanted)
        ; reportFlats ctxt2 (mapBag (tidyCt env) flats)
-            -- All the Derived ones have been filtered out of flats 
+            -- All the Derived ones have been filtered out of flats
             -- by the constraint solver. This is ok; we don't want
             -- to report unsolved Derived goals as errors
             -- See Note [Do not report derived but soluble errors]
@@ -609,10 +609,11 @@ mkEqErr1 ctxt ct
 
   | otherwise   -- Wanted or derived
   = do { (ctxt, binds_msg) <- relevantBindings True ctxt ct
-       ; (ctxt, tidy_orig) <- zonkTidyOrigin ctxt (ctLocOrigin loc)
+       ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
        ; let (is_oriented, wanted_msg) = mk_wanted_extra tidy_orig
        ; dflags <- getDynFlags
-       ; mkEqErr_help dflags ctxt (wanted_msg $$ binds_msg) 
+       ; mkEqErr_help dflags (ctxt {cec_tidy = env1})
+                      (wanted_msg $$ binds_msg)
                       ct is_oriented ty1 ty2 }
   where
     ev         = ctEvidence ct
@@ -642,10 +643,12 @@ mkEqErr1 ctxt ct
                  TypeEqOrigin {} -> snd (mkExpectedActualMsg cty1 cty2 sub_o)
                  _ -> empty
 
-    mk_wanted_extra _ = (Nothing, empty)
+    mk_wanted_extra orig@(FunDepOrigin1 {}) = (Nothing, pprArising orig)
+    mk_wanted_extra orig@(FunDepOrigin2 {}) = (Nothing, pprArising orig)
+    mk_wanted_extra _                       = (Nothing, empty)
 
 mkEqErr_help :: DynFlags -> ReportErrCtxt -> SDoc
-             -> Ct          
+             -> Ct
              -> Maybe SwapFlag   -- Nothing <=> not sure
              -> TcType -> TcType -> TcM ErrMsg
 mkEqErr_help dflags ctxt extra ct oriented ty1 ty2
@@ -656,7 +659,7 @@ mkEqErr_help dflags ctxt extra ct oriented ty1 ty2
     swapped = fmap flipSwap oriented
 
 reportEqErr :: ReportErrCtxt -> SDoc
-            -> Ct    
+            -> Ct
             -> Maybe SwapFlag   -- Nothing <=> not sure
             -> TcType -> TcType -> TcM ErrMsg
 reportEqErr ctxt extra1 ct oriented ty1 ty2
@@ -664,7 +667,7 @@ reportEqErr ctxt extra1 ct oriented ty1 ty2
        ; mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
                                    , extra2, extra1]) }
 
-mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> SDoc -> Ct 
+mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> SDoc -> Ct
              -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
 mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
@@ -1366,7 +1369,7 @@ relevantBindings want_filtering ctxt ct
          -- tcl_bndrs has the innermost bindings first, 
          -- which are probably the most relevant ones
 
-       ; traceTc "relevantBindings" (ppr [id | TcIdBndr id _ <- tcl_bndrs lcl_env])
+       ; traceTc "relevantBindings" (ppr ct $$ ppr [id | TcIdBndr id _ <- tcl_bndrs lcl_env])
        ; let doc = hang (ptext (sLit "Relevant bindings include")) 
                       2 (vcat docs $$ max_msg)
              max_msg | discards 
@@ -1378,8 +1381,15 @@ relevantBindings want_filtering ctxt ct
          else do { traceTc "rb" doc
                  ; return (ctxt { cec_tidy = tidy_env' }, doc) } } 
   where
-    lcl_env = ctLocEnv (ctLoc ct)
-    ct_tvs = tyVarsOfCt ct
+    loc       = ctLoc ct
+    lcl_env   = ctLocEnv loc
+    ct_tvs    = tyVarsOfCt ct `unionVarSet` extra_tvs
+
+    -- For *kind* errors, report the relevant bindings of the
+    -- enclosing *type* equality, becuase that's more useful for the programmer
+    extra_tvs = case ctLocOrigin loc of
+                  KindEqOrigin t1 t2 _ -> tyVarsOfTypes [t1,t2]
+                  _                    -> emptyVarSet
 
     run_out :: Maybe Int -> Bool
     run_out Nothing = False
@@ -1397,6 +1407,7 @@ relevantBindings want_filtering ctxt ct
        = return (tidy_env, reverse docs, discards)
     go tidy_env n_left tvs_seen docs discards (TcIdBndr id top_lvl : tc_bndrs)
        = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env (idType id)
+            ; traceTc "relevantBindings 1" (ppr id <+> dcolon <+> ppr tidy_ty)
             ; let id_tvs = tyVarsOfType tidy_ty
                   doc = sep [ pprPrefixOcc id <+> dcolon <+> ppr tidy_ty
 		            , nest 2 (parens (ptext (sLit "bound at")
@@ -1481,20 +1492,28 @@ zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
                            ; return (tidyOpenType env ty') }
 
-zonkTidyOrigin :: ReportErrCtxt -> CtOrigin -> TcM (ReportErrCtxt, CtOrigin)
-zonkTidyOrigin ctxt (GivenOrigin skol_info)
+zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
+zonkTidyOrigin env (GivenOrigin skol_info)
   = do { skol_info1 <- zonkSkolemInfo skol_info
-       ; let (env1, skol_info2) = tidySkolemInfo (cec_tidy ctxt) skol_info1
-       ; return (ctxt { cec_tidy = env1 }, GivenOrigin skol_info2) }
-zonkTidyOrigin ctxt (TypeEqOrigin { uo_actual = act, uo_expected = exp })
-  = do { (env1, act') <- zonkTidyTcType (cec_tidy ctxt) act
-       ; (env2, exp') <- zonkTidyTcType env1            exp
-       ; return ( ctxt { cec_tidy = env2 }
-                , TypeEqOrigin { uo_actual = act', uo_expected = exp' }) }
-zonkTidyOrigin ctxt (KindEqOrigin ty1 ty2 orig)
-  = do { (env1, ty1') <- zonkTidyTcType (cec_tidy ctxt) ty1
-       ; (env2, ty2') <- zonkTidyTcType env1            ty2
-       ; (ctxt2, orig') <- zonkTidyOrigin (ctxt { cec_tidy = env2 }) orig
-       ; return (ctxt2, KindEqOrigin ty1' ty2' orig') }
-zonkTidyOrigin ctxt orig = return (ctxt, orig)
+       ; let (env1, skol_info2) = tidySkolemInfo env skol_info1
+       ; return (env1, GivenOrigin skol_info2) }
+zonkTidyOrigin env (TypeEqOrigin { uo_actual = act, uo_expected = exp })
+  = do { (env1, act') <- zonkTidyTcType env  act
+       ; (env2, exp') <- zonkTidyTcType env1 exp
+       ; return ( env2, TypeEqOrigin { uo_actual = act', uo_expected = exp' }) }
+zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig)
+  = do { (env1, ty1') <- zonkTidyTcType env  ty1
+       ; (env2, ty2') <- zonkTidyTcType env1 ty2
+       ; (env3, orig') <- zonkTidyOrigin env2 orig
+       ; return (env3, KindEqOrigin ty1' ty2' orig') }
+zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
+  = do { (env1, p1') <- zonkTidyTcType env  p1
+       ; (env2, p2') <- zonkTidyTcType env1 p2
+       ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
+zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
+  = do { (env1, p1') <- zonkTidyTcType env  p1
+       ; (env2, p2') <- zonkTidyTcType env1 p2
+       ; (env3, o1') <- zonkTidyOrigin env2 o1
+       ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
+zonkTidyOrigin env orig = return (env, orig)
 \end{code}
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index e56c96131f..04122f964f 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -414,8 +414,10 @@ interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
 
 addFunDepWork :: Ct -> Ct -> TcS ()
 addFunDepWork work_ct inert_ct
-  = do {  let fd_eqns = improveFromAnother (ctPred inert_ct) (ctPred work_ct)
-       ; fd_work <- rewriteWithFunDeps fd_eqns (ctLoc work_ct)
+  = do {  let fd_eqns :: [Equation CtLoc]
+              fd_eqns = [ eqn { fd_loc = derived_loc }
+                        | eqn <- improveFromAnother inert_pred work_pred ]
+       ; fd_work <- rewriteWithFunDeps fd_eqns
                 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
                 -- NB: We do create FDs for given to report insoluble equations that arise
                 -- from pairs of Givens, and also because of floating when we approximate
@@ -430,6 +432,14 @@ addFunDepWork work_ct inert_ct
        ; case fd_work of
            [] -> return ()
            _  -> updWorkListTcS (extendWorkListEqs fd_work)    }
+  where
+    work_pred  = ctPred work_ct
+    inert_pred = ctPred inert_ct
+    work_loc   = ctLoc work_ct
+    inert_loc  = ctLoc inert_ct
+    derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred  work_loc
+                                                        inert_pred inert_loc }
+
 \end{code}
 
 Note [Shadowing of Implicit Parameters]
@@ -1353,16 +1363,16 @@ To achieve this required some refactoring of FunDeps.lhs (nicer
 now!).
 
 \begin{code}
-rewriteWithFunDeps :: [Equation] -> CtLoc -> TcS [Ct]
+rewriteWithFunDeps :: [Equation CtLoc] -> TcS [Ct]
 -- NB: The returned constraints are all Derived
 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
-rewriteWithFunDeps eqn_pred_locs loc
- = do { fd_cts <- mapM (instFunDepEqn loc) eqn_pred_locs
+rewriteWithFunDeps eqn_pred_locs
+ = do { fd_cts <- mapM instFunDepEqn eqn_pred_locs
       ; return (concat fd_cts) }
 
-instFunDepEqn :: CtLoc -> Equation -> TcS [Ct]
+instFunDepEqn :: Equation CtLoc -> TcS [Ct]
 -- Post: Returns the position index as well as the corresponding FunDep equality
-instFunDepEqn loc (FDEqn { fd_qtvs = tvs, fd_eqs = eqs })
+instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
   = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
        ; foldM (do_one subst) [] eqs }
   where
@@ -1483,8 +1493,12 @@ doTopReactDict inerts fl cls xis
      -- so we make sure we get on and solve it first. See Note [Weird fundeps]
      try_fundeps_and_return
        = do { instEnvs <- getInstEnvs
-            ; let fd_eqns = improveFromInstEnv instEnvs pred
-            ; fd_work <- rewriteWithFunDeps fd_eqns loc
+            ; let fd_eqns :: [Equation CtLoc]
+                  fd_eqns = [ fd { fd_loc = loc { ctl_origin = FunDepOrigin2 pred (ctl_origin loc)
+                                                                             inst_pred inst_loc } }
+                            | fd@(FDEqn { fd_loc = inst_loc, fd_pred1 = inst_pred })
+                                 <- improveFromInstEnv instEnvs pred ]
+            ; fd_work <- rewriteWithFunDeps fd_eqns
             ; unless (null fd_work) $
               do { traceTcS "Addig FD work" (ppr pred $$ vcat (map pprEquation fd_eqns) $$ ppr fd_work)
                  ; updWorkListTcS (extendWorkListEqs fd_work) }
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 1be81cb42b..0900ed04a5 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -64,7 +64,7 @@ module TcRnTypes(
         CtLoc(..), ctLocSpan, ctLocEnv, ctLocOrigin,
         ctLocDepth, bumpCtLocDepth,
         setCtLocOrigin, setCtLocEnv,
-        CtOrigin(..),
+        CtOrigin(..), pprCtOrigin,
         pushErrCtxt, pushErrCtxtSameOrigin,
 
         SkolemInfo(..),
@@ -1668,12 +1668,11 @@ pprArising :: CtOrigin -> SDoc
 -- Used for the main, top-level error message
 -- We've done special processing for TypeEq and FunDep origins
 pprArising (TypeEqOrigin {}) = empty
-pprArising FunDepOrigin      = empty
-pprArising orig              = text "arising from" <+> ppr orig
+pprArising orig              = pprCtOrigin orig
 
 pprArisingAt :: CtLoc -> SDoc
 pprArisingAt (CtLoc { ctl_origin = o, ctl_env = lcl})
-  = sep [ text "arising from" <+> ppr o
+  = sep [ pprCtOrigin o
         , text "at" <+> ppr (tcl_loc lcl)]
 \end{code}
 
@@ -1822,58 +1821,99 @@ data CtOrigin
   | IfOrigin            -- Arising from an if statement
   | ProcOrigin          -- Arising from a proc expression
   | AnnOrigin           -- An annotation
-  | FunDepOrigin
+
+  | FunDepOrigin1       -- A functional dependency from combining
+        PredType CtLoc      -- This constraint arising from ...
+        PredType CtLoc      -- and this constraint arising from ...
+
+  | FunDepOrigin2       -- A functional dependency from combining
+        PredType CtOrigin   -- This constraint arising from ...
+        PredType SrcSpan    -- and this instance
+        -- We only need a CtOrigin on the first, because the location
+        -- is pinned on the entire error message
+
   | HoleOrigin
   | UnboundOccurrenceOf RdrName
   | ListOrigin          -- An overloaded list
 
-pprO :: CtOrigin -> SDoc
-pprO (GivenOrigin sk)      = ppr sk
-pprO FlatSkolOrigin        = ptext (sLit "a given flatten-skolem")
-pprO (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
-pprO AppOrigin             = ptext (sLit "an application")
-pprO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
-pprO (IPOccOrigin name)    = hsep [ptext (sLit "a use of implicit parameter"), quotes (ppr name)]
-pprO RecordUpdOrigin       = ptext (sLit "a record update")
-pprO (AmbigOrigin ctxt)    = ptext (sLit "the ambiguity check for")
-                             <+> case ctxt of
-                                    FunSigCtxt name -> quotes (ppr name)
-                                    InfSigCtxt name -> quotes (ppr name)
-                                    _               -> pprUserTypeCtxt ctxt
-pprO ExprSigOrigin         = ptext (sLit "an expression type signature")
-pprO PatSigOrigin          = ptext (sLit "a pattern type signature")
-pprO PatOrigin             = ptext (sLit "a pattern")
-pprO ViewPatOrigin         = ptext (sLit "a view pattern")
-pprO IfOrigin              = ptext (sLit "an if statement")
-pprO (LiteralOrigin lit)   = hsep [ptext (sLit "the literal"), quotes (ppr lit)]
-pprO (ArithSeqOrigin seq)  = hsep [ptext (sLit "the arithmetic sequence"), quotes (ppr seq)]
-pprO (PArrSeqOrigin seq)   = hsep [ptext (sLit "the parallel array sequence"), quotes (ppr seq)]
-pprO SectionOrigin         = ptext (sLit "an operator section")
-pprO TupleOrigin           = ptext (sLit "a tuple")
-pprO NegateOrigin          = ptext (sLit "a use of syntactic negation")
-pprO ScOrigin              = ptext (sLit "the superclasses of an instance declaration")
-pprO DerivOrigin           = ptext (sLit "the 'deriving' clause of a data type declaration")
-pprO (DerivOriginDC dc n)  = hsep [ ptext (sLit "the"), speakNth n,
-                                    ptext (sLit "field of"), quotes (ppr dc),
-                                    parens (ptext (sLit "type") <+> quotes (ppr ty)) ]
-    where ty = dataConOrigArgTys dc !! (n-1)
-pprO (DerivOriginCoerce meth ty1 ty2)
-                           = sep [ ptext (sLit "the coercion of the method") <+> quotes (ppr meth)
-                                 , ptext (sLit "from type") <+> quotes (ppr ty1)
-                                 , nest 2 (ptext (sLit "to type") <+> quotes (ppr ty2)) ]
-pprO StandAloneDerivOrigin = ptext (sLit "a 'deriving' declaration")
-pprO DefaultOrigin         = ptext (sLit "a 'default' declaration")
-pprO DoOrigin              = ptext (sLit "a do statement")
-pprO MCompOrigin           = ptext (sLit "a statement in a monad comprehension")
-pprO ProcOrigin            = ptext (sLit "a proc expression")
-pprO (TypeEqOrigin t1 t2)  = ptext (sLit "a type equality") <+> sep [ppr t1, char '~', ppr t2]
-pprO (KindEqOrigin t1 t2 _) = ptext (sLit "a kind equality arising from") <+> sep [ppr t1, char '~', ppr t2]
-pprO AnnOrigin             = ptext (sLit "an annotation")
-pprO FunDepOrigin          = ptext (sLit "a functional dependency")
-pprO HoleOrigin            = ptext (sLit "a use of") <+> quotes (ptext $ sLit "_")
-pprO (UnboundOccurrenceOf name) = hsep [ptext (sLit "an undeclared identifier"), quotes (ppr name)]
-pprO ListOrigin            = ptext (sLit "an overloaded list")
-
-instance Outputable CtOrigin where
-  ppr = pprO
+
+ctoHerald :: SDoc
+ctoHerald = ptext (sLit "arising from")
+
+pprCtOrigin :: CtOrigin -> SDoc
+
+pprCtOrigin (GivenOrigin sk) = ctoHerald <+> ppr sk
+
+pprCtOrigin (FunDepOrigin1 pred1 loc1 pred2 loc2)
+  = hang (ctoHerald <+> ptext (sLit "a functional dependency between constraints:"))
+       2 (vcat [ hang (quotes (ppr pred1)) 2 (pprArisingAt loc1)
+               , hang (quotes (ppr pred2)) 2 (pprArisingAt loc2) ])
+
+pprCtOrigin (FunDepOrigin2 pred1 orig1 pred2 loc2)
+  = hang (ctoHerald <+> ptext (sLit "a functional dependency between:"))
+       2 (vcat [ hang (ptext (sLit "constraint") <+> quotes (ppr pred1))
+                    2 (pprArising orig1 )
+               , hang (ptext (sLit "instance") <+> quotes (ppr pred2))
+                    2 (ptext (sLit "at") <+> ppr loc2) ])
+
+pprCtOrigin (KindEqOrigin t1 t2 _)
+  = hang (ctoHerald <+> ptext (sLit "a kind equality arising from"))
+       2 (sep [ppr t1, char '~', ppr t2])
+
+pprCtOrigin (UnboundOccurrenceOf name)
+  = ctoHerald <+> ptext (sLit "an undeclared identifier") <+> quotes (ppr name)
+
+pprCtOrigin (DerivOriginDC dc n)
+  = hang (ctoHerald <+> ptext (sLit "the") <+> speakNth n
+          <+> ptext (sLit "field of") <+> quotes (ppr dc))
+       2 (parens (ptext (sLit "type") <+> quotes (ppr ty)))
+  where
+    ty = dataConOrigArgTys dc !! (n-1)
+
+pprCtOrigin (AmbigOrigin ctxt)
+  = ctoHerald <+> ptext (sLit "the ambiguity check for")
+    <+> case ctxt of
+           FunSigCtxt name -> quotes (ppr name)
+           InfSigCtxt name -> quotes (ppr name)
+           _               -> pprUserTypeCtxt ctxt
+
+pprCtOrigin (DerivOriginCoerce meth ty1 ty2)
+  = hang (ctoHerald <+> ptext (sLit "the coercion of the method") <+> quotes (ppr meth))
+       2 (sep [ ptext (sLit "from type") <+> quotes (ppr ty1)
+              , ptext (sLit "  to type") <+> quotes (ppr ty2) ])
+
+pprCtOrigin simple_origin
+  = ctoHerald <+> pprCtO simple_origin
+
+----------------
+pprCtO :: CtOrigin -> SDoc  -- Ones that are short one-liners
+pprCtO FlatSkolOrigin        = ptext (sLit "a given flatten-skolem")
+pprCtO (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
+pprCtO AppOrigin             = ptext (sLit "an application")
+pprCtO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
+pprCtO (IPOccOrigin name)    = hsep [ptext (sLit "a use of implicit parameter"), quotes (ppr name)]
+pprCtO RecordUpdOrigin       = ptext (sLit "a record update")
+pprCtO ExprSigOrigin         = ptext (sLit "an expression type signature")
+pprCtO PatSigOrigin          = ptext (sLit "a pattern type signature")
+pprCtO PatOrigin             = ptext (sLit "a pattern")
+pprCtO ViewPatOrigin         = ptext (sLit "a view pattern")
+pprCtO IfOrigin              = ptext (sLit "an if statement")
+pprCtO (LiteralOrigin lit)   = hsep [ptext (sLit "the literal"), quotes (ppr lit)]
+pprCtO (ArithSeqOrigin seq)  = hsep [ptext (sLit "the arithmetic sequence"), quotes (ppr seq)]
+pprCtO (PArrSeqOrigin seq)   = hsep [ptext (sLit "the parallel array sequence"), quotes (ppr seq)]
+pprCtO SectionOrigin         = ptext (sLit "an operator section")
+pprCtO TupleOrigin           = ptext (sLit "a tuple")
+pprCtO NegateOrigin          = ptext (sLit "a use of syntactic negation")
+pprCtO ScOrigin              = ptext (sLit "the superclasses of an instance declaration")
+pprCtO DerivOrigin           = ptext (sLit "the 'deriving' clause of a data type declaration")
+pprCtO StandAloneDerivOrigin = ptext (sLit "a 'deriving' declaration")
+pprCtO DefaultOrigin         = ptext (sLit "a 'default' declaration")
+pprCtO DoOrigin              = ptext (sLit "a do statement")
+pprCtO MCompOrigin           = ptext (sLit "a statement in a monad comprehension")
+pprCtO ProcOrigin            = ptext (sLit "a proc expression")
+pprCtO (TypeEqOrigin t1 t2)  = ptext (sLit "a type equality") <+> sep [ppr t1, char '~', ppr t2]
+pprCtO AnnOrigin             = ptext (sLit "an annotation")
+pprCtO HoleOrigin            = ptext (sLit "a use of") <+> quotes (ptext $ sLit "_")
+pprCtO ListOrigin            = ptext (sLit "an overloaded list")
+pprCtO _                     = panic "pprCtOrigin"
 \end{code}
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index d26091728e..b66f06b91b 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -545,7 +545,7 @@ uType_defer origin ty1 ty2
             { ctxt <- getErrCtxt
             ; doc <- mkErrInfo emptyTidyEnv ctxt
             ; traceTc "utype_defer" (vcat [ppr eqv, ppr ty1,
-                                           ppr ty2, ppr origin, doc])
+                                           ppr ty2, pprCtOrigin origin, doc])
             }
        ; return (mkTcCoVarCo eqv) }
 
@@ -556,7 +556,7 @@ uType origin orig_ty1 orig_ty2
        ; traceTc "u_tys " $ vcat
               [ text "untch" <+> ppr untch
               , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
-              , ppr origin]
+              , pprCtOrigin origin]
        ; co <- go orig_ty1 orig_ty2
        ; if isTcReflCo co
             then traceTc "u_tys yields no coercion" Outputable.empty
diff --git a/testsuite/tests/typecheck/should_compile/FD3.stderr b/testsuite/tests/typecheck/should_compile/FD3.stderr
index d2364921f6..0ba6587273 100644
--- a/testsuite/tests/typecheck/should_compile/FD3.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD3.stderr
@@ -1,5 +1,14 @@
-

-FD3.hs:15:15:

-    No instance for (MkA (String, a) a) arising from a use of ‘mkA’

-    In the expression: mkA a

-    In an equation for ‘translate’: translate a = mkA a

+
+FD3.hs:15:15:
+    Couldn't match type ‘a’ with ‘(String, a)’
+      ‘a’ is a rigid type variable bound by
+          the type signature for translate :: (String, a) -> A a
+          at FD3.hs:14:14
+    arising from a functional dependency between:
+      constraint ‘MkA (String, a) a’ arising from a use of ‘mkA’
+      instance ‘MkA a1 a1’ at FD3.hs:12:10-16
+    Relevant bindings include
+      a :: (String, a) (bound at FD3.hs:15:11)
+      translate :: (String, a) -> A a (bound at FD3.hs:15:1)
+    In the expression: mkA a
+    In an equation for ‘translate’: translate a = mkA a
diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
index 56d3006260..f3320d0d8e 100644
--- a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
+++ b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
@@ -1,10 +1,12 @@
-

-FDsFromGivens.hs:21:15:

-    Could not deduce (C Char [a]) arising from a use of ‘f’

-    from the context (C Char Char)

-      bound by a pattern with constructor

-                 KCC :: C Char Char => () -> KCC,

-               in an equation for ‘bar’

-      at FDsFromGivens.hs:21:6-10

-    In the expression: f

-    In an equation for ‘bar’: bar (KCC _) = f

+
+FDsFromGivens.hs:21:15:
+    Couldn't match type ‘Char’ with ‘[a0]’
+    arising from a functional dependency between constraints:
+      ‘C Char [a0]’ arising from a use of ‘f’ at FDsFromGivens.hs:21:15
+      ‘C Char Char’
+        arising from a pattern with constructor
+                       KCC :: C Char Char => () -> KCC,
+                     in an equation for ‘bar’
+        at FDsFromGivens.hs:21:6-10
+    In the expression: f
+    In an equation for ‘bar’: bar (KCC _) = f
diff --git a/testsuite/tests/typecheck/should_fail/T5236.stderr b/testsuite/tests/typecheck/should_fail/T5236.stderr
index 557a0413c9..8a723bab9b 100644
--- a/testsuite/tests/typecheck/should_fail/T5236.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5236.stderr
@@ -1,5 +1,10 @@
-

-T5236.hs:17:5:

-    No instance for (Id A B) arising from a use of ‘loop’

-    In the expression: loop

-    In an equation for ‘f’: f = loop

+
+T5236.hs:13:9:
+    Couldn't match type ‘A’ with ‘B’
+    arising from a functional dependency between:
+      constraint ‘Id A B’
+        arising from the type signature for loop :: Id A B => Bool
+      instance ‘Id A A’ at T5236.hs:10:10-15
+    In the ambiguity check for: Id A B => Bool
+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+    In the type signature for ‘loop’: loop :: Id A B => Bool
diff --git a/testsuite/tests/typecheck/should_fail/T5978.stderr b/testsuite/tests/typecheck/should_fail/T5978.stderr
index db6b8f355e..263e68ba2d 100644
--- a/testsuite/tests/typecheck/should_fail/T5978.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5978.stderr
@@ -1,5 +1,8 @@
-

-T5978.hs:22:11:

-    No instance for (C Double Char) arising from a use of ‘polyBar’

-    In the expression: polyBar id monoFoo

-    In an equation for ‘monoBar’: monoBar = polyBar id monoFoo

+
+T5978.hs:22:11:
+    Couldn't match type ‘Bool’ with ‘Char’
+    arising from a functional dependency between:
+      constraint ‘C Double Char’ arising from a use of ‘polyBar’
+      instance ‘C Double Bool’ at T5978.hs:8:10-22
+    In the expression: polyBar id monoFoo
+    In an equation for ‘monoBar’: monoBar = polyBar id monoFoo
diff --git a/testsuite/tests/typecheck/should_fail/T9612.hs b/testsuite/tests/typecheck/should_fail/T9612.hs
new file mode 100644
index 0000000000..a332c47b04
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T9612.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses #-}
+module T9612 where
+import Data.Monoid
+import Control.Monad.Trans.Writer.Lazy( Writer, WriterT )
+import Data.Functor.Identity( Identity )
+
+class (Monoid w, Monad m) => MonadWriter w m | m -> w where
+    writer :: (a,w) -> m a
+    tell   :: w -> m ()
+    listen :: m a -> m (a, w)
+    pass   :: m (a, w -> w) -> m a
+
+f ::(Eq a) => a -> (Int, a) -> Writer [(Int, a)] (Int, a)
+f y (n,x) {- | y == x    = return (n+1, x)
+             | otherwise = -}
+   = do tell (n,x)
+        return (1,y)
+
+
+instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
diff --git a/testsuite/tests/typecheck/should_fail/T9612.stderr b/testsuite/tests/typecheck/should_fail/T9612.stderr
new file mode 100644
index 0000000000..823fee112c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T9612.stderr
@@ -0,0 +1,20 @@
+
+T9612.hs:16:9:
+    Couldn't match type ‘[(Int, a)]’ with ‘(Int, a)’
+    arising from a functional dependency between:
+      constraint ‘MonadWriter (Int, a) (WriterT [(Int, a)] Identity)’
+        arising from a use of ‘tell’
+      instance ‘MonadWriter w (WriterT w m)’ at T9612.hs:20:10-59
+    Relevant bindings include
+      x :: a (bound at T9612.hs:14:8)
+      y :: a (bound at T9612.hs:14:3)
+      f :: a -> (Int, a) -> Writer [(Int, a)] (Int, a)
+        (bound at T9612.hs:14:1)
+    In a stmt of a 'do' block: tell (n, x)
+    In the expression:
+      do { tell (n, x);
+           return (1, y) }
+    In an equation for ‘f’:
+        f y (n, x)
+          = do { tell (n, x);
+                 return (1, y) }
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 4f001f5ab7..431a9ba767 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -334,3 +334,4 @@ test('T9196', normal, compile_fail, [''])
 test('T9305', normal, compile_fail, [''])
 test('T9323', normal, compile_fail, [''])
 test('T9415', normal, compile_fail, [''])
+test('T9612', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail143.stderr b/testsuite/tests/typecheck/should_fail/tcfail143.stderr
index 394fa43c4e..b36d7a8b37 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail143.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail143.stderr
@@ -1,5 +1,8 @@
-

-tcfail143.hs:29:9:

-    No instance for (MinMax (S Z) Z Z Z) arising from a use of ‘extend’

-    In the expression: n1 `extend` n0

-    In an equation for ‘t2’: t2 = n1 `extend` n0

+
+tcfail143.hs:29:9:
+    Couldn't match type ‘S Z’ with ‘Z’
+    arising from a functional dependency between:
+      constraint ‘MinMax (S Z) Z Z Z’ arising from a use of ‘extend’
+      instance ‘MinMax a Z Z a’ at tcfail143.hs:11:10-23
+    In the expression: n1 `extend` n0
+    In an equation for ‘t2’: t2 = n1 `extend` n0