Fix recursive superclasses (again). Fixes Trac #4809.
[ghc-hetmet.git] / compiler / typecheck / TcErrors.lhs
index 9531a50..c040473 100644 (file)
@@ -3,8 +3,9 @@ module TcErrors(
        reportUnsolved, reportUnsolvedDeriv,
        reportUnsolvedWantedEvVars, warnDefaulting, 
        unifyCtxt, typeExtraInfoMsg, 
-       kindErrorTcS, misMatchErrorTcS, flattenForAllErrorTcS,
-       occursCheckErrorTcS, solverDepthErrorTcS
+
+       flattenForAllErrorTcS,
+       solverDepthErrorTcS
   ) where
 
 #include "HsVersions.h"
@@ -13,6 +14,8 @@ import TcRnMonad
 import TcMType
 import TcSMonad
 import TcType
+import TypeRep
+
 import Inst
 import InstEnv
 
@@ -33,7 +36,7 @@ import Outputable
 import DynFlags
 import StaticFlags( opt_PprStyle_Debug )
 import Data.List( partition )
-import Control.Monad( unless )
+import Control.Monad( when, unless )
 \end{code}
 
 %************************************************************************
@@ -47,24 +50,126 @@ from the insts, or just whatever seems to be around in the monad just
 now?
 
 \begin{code}
-reportUnsolved :: (CanonicalCts, Bag Implication) -> TcM ()
-reportUnsolved (unsolved_flats, unsolved_implics)
-  | isEmptyBag unsolved
+reportUnsolved :: (Bag WantedEvVar, Bag Implication) -> Bag FrozenError -> TcM ()
+reportUnsolved (unsolved_flats, unsolved_implics) frozen_errors
+  | isEmptyBag unsolved && isEmptyBag frozen_errors
   = return ()
   | otherwise
-  = do { unsolved <- mapBagM zonkWanted unsolved
+  = do { frozen_errors_zonked <- mapBagM zonk_frozen frozen_errors
+       ; let frozen_tvs = tyVarsOfFrozen frozen_errors_zonked 
+
+       ; unsolved <- mapBagM zonkWanted unsolved
                     -- Zonk to un-flatten any flatten-skols
        ; env0 <- tcInitTidyEnv
-       ; let tidy_env      = tidyFreeTyVars env0 (tyVarsOfWanteds unsolved)
+       ; let tidy_env      = tidyFreeTyVars env0 $ 
+                             tyVarsOfWanteds unsolved `unionVarSet` frozen_tvs 
+
              tidy_unsolved = tidyWanteds tidy_env unsolved
              err_ctxt = CEC { cec_encl = [] 
                             , cec_extra = empty
-                            , cec_tidy = tidy_env } 
-       ; traceTc "reportUnsolved" (ppr unsolved)
+                            , cec_tidy = tidy_env 
+                            } 
+
+       ; traceTc "reportUnsolved" (vcat [
+              text "Unsolved constraints =" <+> ppr unsolved,
+              text "Frozen errors =" <+> ppr frozen_errors_zonked ])
+
+       ; let tidy_frozen_errors_zonked = tidyFrozen tidy_env frozen_errors_zonked
+
+       ; reportTidyFrozens tidy_env tidy_frozen_errors_zonked 
        ; reportTidyWanteds err_ctxt tidy_unsolved }
   where
-    unsolved = mkWantedConstraints unsolved_flats unsolved_implics
+    unsolved = Bag.mapBag WcEvVar unsolved_flats `unionBags` 
+                 Bag.mapBag WcImplic unsolved_implics
+
+    zonk_frozen (FrozenError frknd fl ty1 ty2)
+      = do { ty1z <- zonkTcType ty1 
+           ; ty2z <- zonkTcType ty2
+           ; return (FrozenError frknd fl ty1z ty2z) }
+
+    tyVarsOfFrozen fr 
+      = unionVarSets $ bagToList (mapBag tvs_of_frozen fr)
+    tvs_of_frozen (FrozenError _ _ ty1 ty2) = tyVarsOfTypes [ty1,ty2]
+
+    tidyFrozen env fr = mapBag (tidy_frozen env) fr
+    tidy_frozen env (FrozenError frknd fl ty1 ty2)
+      = FrozenError frknd fl (tidyType env ty1) (tidyType env ty2)
+
+reportTidyFrozens :: TidyEnv -> Bag FrozenError -> TcM ()
+reportTidyFrozens tidy_env fr = mapBagM_ (reportTidyFrozen tidy_env) fr 
+
+reportTidyFrozen :: TidyEnv -> FrozenError -> TcM () 
+reportTidyFrozen tidy_env err@(FrozenError _ fl _ty1 _ty2)
+  = do { let dec_errs = decompFrozenError err
+             init_err_ctxt = CEC { cec_encl  = [] 
+                                 , cec_extra = empty
+                                 , cec_tidy  = tidy_env }
+       ; mapM_ (report_dec_err init_err_ctxt) dec_errs }
+  where 
+    report_dec_err err_ctxt (ty1,ty2)
+        -- The only annoying thing here is that in the given case, 
+        -- the ``Inaccessible code'' message will be printed once for 
+        -- each decomposed equality.
+          = do { (tidy_env2,extra2)
+                     <- if isGiven fl
+                        then return (cec_tidy err_ctxt, inaccessible_msg)
+                        else getWantedEqExtra emptyTvSubst (cec_tidy err_ctxt) loc_orig ty1 ty2
+               ; let err_ctxt2 = err_ctxt { cec_tidy  = tidy_env2
+                                          , cec_extra = cec_extra err_ctxt $$ extra2 }
+               ; setCtFlavorLoc fl $ 
+                 reportEqErr err_ctxt2 ty1 ty2 
+               }
+
+    loc_orig | Wanted loc <- fl    = ctLocOrigin loc
+             | Derived loc _ <- fl = ctLocOrigin loc
+             | otherwise           = pprPanic "loc_orig" empty 
 
+    inaccessible_msg 
+      | Given loc <- fl
+      = hang (ptext (sLit "Inaccessible code in")) 2 (mk_what loc)
+      | otherwise = pprPanic "inaccessible_msg" empty
+
+    mk_what loc
+      = case ctLocOrigin loc of
+          PatSkol dc mc -> sep [ ptext (sLit "a pattern with constructor") 
+                                   <+> quotes (ppr dc) <> comma
+                               , ptext (sLit "in") <+> pprMatchContext mc ]
+         other_skol -> pprSkolInfo other_skol
+
+
+decompFrozenError :: FrozenError -> [(TcType,TcType)] 
+-- Postcondition: will always return a non-empty list
+decompFrozenError (FrozenError errk _fl ty1 ty2) 
+  | OccCheckError <- errk
+  = dec_occ_check ty1 ty2 
+  | otherwise 
+  = [(ty1,ty2)]
+  where dec_occ_check :: TcType -> TcType -> [(TcType,TcType)] 
+        -- This error arises from an original: 
+        --      a ~ Maybe a
+        -- But by now the a has been substituted away, eg: 
+        --      Int ~ Maybe Int
+        --      Maybe b ~ Maybe (Maybe b)
+        dec_occ_check ty1 ty2 
+          | tcEqType ty1 ty2 = []
+        dec_occ_check ty1@(TyVarTy {}) ty2 = [(ty1,ty2)] 
+        dec_occ_check (FunTy s1 t1) (FunTy s2 t2) 
+          = let errs1 = dec_occ_check s1 s2 
+                errs2 = dec_occ_check t1 t2
+            in errs1 ++ errs2 
+        dec_occ_check ty1@(TyConApp fn1 tys1) ty2@(TyConApp fn2 tys2) 
+          | fn1 == fn2 && length tys1 == length tys2 
+          , not (isSynFamilyTyCon fn1)
+          = concatMap (\(t1,t2) -> dec_occ_check t1 t2) (zip tys1 tys2)
+          | otherwise 
+          = [(ty1,ty2)]
+        dec_occ_check ty1 ty2 
+          | Just (s1,t1) <- tcSplitAppTy_maybe ty1 
+          , Just (s2,t2) <- tcSplitAppTy_maybe ty2 
+          = let errs1 = dec_occ_check s1 s2 
+                errs2 = dec_occ_check t1 t2 
+            in errs1 ++ errs2
+        dec_occ_check ty1 ty2 = [(ty1,ty2)]
 
 reportUnsolvedWantedEvVars :: Bag WantedEvVar -> TcM ()
 reportUnsolvedWantedEvVars wanteds
@@ -105,8 +210,8 @@ reportUnsolvedDeriv unsolved loc
 data ReportErrCtxt 
     = CEC { cec_encl :: [Implication]  -- Enclosing implications
                                       --   (innermost first)
-          , cec_tidy :: TidyEnv
-          , cec_extra :: SDoc         -- Add this to each error message
+          , cec_tidy     :: TidyEnv
+          , cec_extra    :: SDoc       -- Add this to each error message
       }
 
 reportTidyImplic :: ReportErrCtxt -> Implication -> TcM ()
@@ -117,17 +222,34 @@ reportTidyImplic ctxt implic
   
 reportTidyWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
 reportTidyWanteds ctxt unsolved
-  = do { let (flats, implics) = splitWanteds unsolved
-             (ambigs, others) = partition is_ambiguous (bagToList flats)
-       ; groupErrs (reportFlat ctxt) others
-       ; mapBagM_ (reportTidyImplic ctxt) implics
-       ; ifErrsM (return ()) $
-                  -- Only report ambiguity if no other errors happened
-          -- See Note [Avoiding spurious errors]
-         reportAmbigErrs ctxt skols ambigs }
+  = do { let (flats,  implics)    = splitWanteds unsolved
+             (ambigs, non_ambigs) = partition is_ambiguous (bagToList flats)
+                    (tv_eqs, others)     = partition is_tv_eq non_ambigs
+
+       ; groupErrs (reportEqErrs ctxt) tv_eqs
+       ; when (null tv_eqs) $ groupErrs (reportFlat ctxt) others
+       ; traceTc "rtw" (vcat [
+              text "unsolved =" <+> ppr unsolved,
+              text "tveqs =" <+> ppr tv_eqs,
+              text "others =" <+> ppr others,
+              text "ambigs =" <+> ppr ambigs ,
+              text "implics =" <+> ppr implics])
+
+       ; when (null tv_eqs) $ mapBagM_ (reportTidyImplic ctxt) implics
+
+                  -- Only report ambiguity if no other errors (at all) happened
+          -- See Note [Avoiding spurious errors] in TcSimplify
+       ; ifErrsM (return ()) $ reportAmbigErrs ctxt skols ambigs }
   where
     skols = foldr (unionVarSet . ic_skols) emptyVarSet (cec_encl ctxt)
  
+       -- Report equalities of form (a~ty) first.  They are usually
+       -- skolem-equalities, and they cause confusing knock-on 
+       -- effects in other errors; see test T4093b.
+    is_tv_eq c | EqPred ty1 ty2 <- wantedEvVarPred c
+               = tcIsTyVarTy ty1 || tcIsTyVarTy ty2
+               | otherwise = False
+
        -- Treat it as "ambiguous" if 
        --   (a) it is a class constraint
         --   (b) it constrains only type variables
@@ -139,6 +261,7 @@ reportTidyWanteds ctxt unsolved
                      pred = wantedEvVarPred d
 
 reportFlat :: ReportErrCtxt -> [PredType] -> CtOrigin -> TcM ()
+-- The [PredType] are already tidied
 reportFlat ctxt flats origin
   = do { unless (null dicts) $ reportDictErrs ctxt dicts origin
        ; unless (null eqs)   $ reportEqErrs   ctxt eqs   origin
@@ -211,12 +334,6 @@ pprErrCtxtLoc ctxt
     ppr_skol (PatSkol dc _) = ptext (sLit "the data constructor") <+> quotes (ppr dc)
     ppr_skol skol_info      = pprSkolInfo skol_info
 
-couldNotDeduce :: [EvVar] -> [PredType] -> SDoc
-couldNotDeduce givens wanteds
-  = sep [ ptext (sLit "Could not deduce") <+> pprTheta wanteds
-        , nest 2 $ ptext (sLit "from the context") 
-                     <+> pprEvVarTheta givens]
-
 getUserGivens :: ReportErrCtxt -> Maybe [EvVar]
 -- Just gs => Say "could not deduce ... from gs"
 -- Nothing => No interesting givens, say something else
@@ -226,11 +343,9 @@ getUserGivens (CEC {cec_encl = ctxt})
   where 
     givens = foldl (\gs ic -> ic_given ic ++ gs) [] ctxt
     user_givens | opt_PprStyle_Debug = givens
-                | otherwise          = filterOut isSelfDict givens
-       -- In user mode, don't show the "self-dict" given
-       -- which is only added to do co-inductive solving
-       -- Rather an awkward hack, but there we are
-       -- This is the only use of isSelfDict, so it's not in an inner loop
+                | otherwise          = filterOut isSilentEvVar givens
+       -- In user mode, don't show the "silent" givens, used for
+       -- the "self" dictionary and silent superclass arguments for dfuns
 \end{code}
 
 
@@ -261,32 +376,33 @@ reportIPErrs ctxt ips orig
 
 \begin{code}
 reportEqErrs :: ReportErrCtxt -> [PredType] -> CtOrigin -> TcM ()
+-- The [PredType] are already tidied
 reportEqErrs ctxt eqs orig
   = mapM_ report_one eqs 
   where
     env0 = cec_tidy ctxt
     report_one (EqPred ty1 ty2) 
       = do { (env1, extra) <- getWantedEqExtra emptyTvSubst env0 orig ty1 ty2
-           ; let ctxt' = ctxt { cec_tidy = env1
-                               , cec_extra = cec_extra ctxt $$ extra }
+            ; let ctxt' = ctxt { cec_tidy = env1
+                               , cec_extra = extra $$ cec_extra ctxt }
            ; reportEqErr ctxt' ty1 ty2 }
     report_one pred 
       = pprPanic "reportEqErrs" (ppr pred)    
 
 reportEqErr :: ReportErrCtxt -> TcType -> TcType -> TcM ()
+-- ty1 and ty2 are already tidied
 reportEqErr ctxt ty1 ty2
   | Just tv1 <- tcGetTyVar_maybe ty1 = reportTyVarEqErr ctxt tv1 ty2
   | Just tv2 <- tcGetTyVar_maybe ty2 = reportTyVarEqErr ctxt tv2 ty1
+
   | otherwise  -- Neither side is a type variable
                -- Since the unsolved constraint is canonical, 
                -- it must therefore be of form (F tys ~ ty)
-  = addErrorReport ctxt (msg $$ mkTyFunInfoMsg ty1 ty2)
-  where
-    msg = case getUserGivens ctxt of
-            Just givens -> couldNotDeduce givens [EqPred ty1 ty2]
-            Nothing     -> misMatchMsg ty1 ty2
+  = addErrorReport ctxt (misMatchOrCND ctxt ty1 ty2 $$ mkTyFunInfoMsg ty1 ty2)
+
 
 reportTyVarEqErr :: ReportErrCtxt -> TcTyVar -> TcType -> TcM ()
+-- tv1 and ty2 are already tidied
 reportTyVarEqErr ctxt tv1 ty2
   | not is_meta1
   , Just tv2 <- tcGetTyVar_maybe ty2
@@ -296,13 +412,20 @@ reportTyVarEqErr ctxt tv1 ty2
 
   | not is_meta1
   = -- sk ~ ty, where ty isn't a meta-tyvar: mis-match
-    addErrTcM (misMatchMsgWithExtras (cec_tidy ctxt) ty1 ty2)
+    addErrorReport (addExtraInfo ctxt ty1 ty2)
+                   (misMatchOrCND ctxt ty1 ty2)
 
   -- So tv is a meta tyvar, and presumably it is
   -- an *untouchable* meta tyvar, else it'd have been unified
   | not (k2 `isSubKind` k1)     -- Kind error
   = addErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2)
 
+  -- Occurs check
+  | tv1 `elemVarSet` tyVarsOfType ty2
+  = let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
+                           (sep [ppr ty1, char '=', ppr ty2])
+    in addErrorReport ctxt occCheckMsg
+
   -- Check for skolem escape
   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
   , let esc_skols = varSetElems (tyVarsOfType ty2 `intersectVarSet` ic_skols implic)
@@ -312,14 +435,15 @@ reportTyVarEqErr ctxt tv1 ty2
                                -- place the equality arose to the implication site
     do { (env1, env_sigs) <- findGlobals ctxt (unitVarSet tv1)
        ; let msg = misMatchMsg ty1 ty2
-             esc_doc | isSingleton esc_skols 
-                     = ptext (sLit "because this skolem type variable would escape:")
-                     | otherwise
-                     = ptext (sLit "because these skolem type variables would escape:")
-             extra1 = vcat [ nest 2 $ esc_doc <+> pprQuotedList esc_skols
+             esc_doc = sep [ ptext (sLit "because type variable") <> plural esc_skols
+                             <+> pprQuotedList esc_skols
+                           , ptext (sLit "would escape") <+>
+                             if isSingleton esc_skols then ptext (sLit "its scope")
+                                                      else ptext (sLit "their scope") ]
+             extra1 = vcat [ nest 2 $ esc_doc
                            , sep [ (if isSingleton esc_skols 
-                                      then ptext (sLit "This skolem is")
-                                      else ptext (sLit "These skolems are"))
+                                    then ptext (sLit "This (rigid, skolem) type variable is")
+                                    else ptext (sLit "These (rigid, skolem) type variables are"))
                                    <+> ptext (sLit "bound by")
                                  , nest 2 $ pprSkolInfo (ctLocOrigin implic_loc) ] ]
        ; addErrTcM (env1, msg $$ extra1 $$ mkEnvSigMsg (ppr tv1) env_sigs) }
@@ -329,15 +453,23 @@ reportTyVarEqErr ctxt tv1 ty2
   , let implic_loc = ic_loc implic
         given      = ic_given implic
   = setCtLoc (ic_loc implic) $
-    do { let (env1, msg) = misMatchMsgWithExtras (cec_tidy ctxt) ty1 ty2
-             extra = vcat [ ptext (sLit "because") <+> ppr tv1 <+> ptext (sLit "is untouchable")
-                          , ptext (sLit "inside the constraints") <+> pprEvVarTheta given 
-                          , nest 2 (ptext (sLit "bound at")
-                             <+> pprSkolInfo (ctLocOrigin implic_loc)) ]
-       ; addErrTcM (env1, msg $$ extra) }
-
-  | otherwise     -- I'm not sure how this can happen!
-  = addErrTcM (misMatchMsgWithExtras (cec_tidy ctxt) ty1 ty2)
+    do { let msg = misMatchMsg ty1 ty2
+             extra = quotes (ppr tv1)
+                 <+> sep [ ptext (sLit "is untouchable")
+                         , ptext (sLit "inside the constraints") <+> pprEvVarTheta given
+                         , ptext (sLit "bound at") <+> pprSkolInfo (ctLocOrigin implic_loc)]
+       ; addErrorReport (addExtraInfo ctxt ty1 ty2) (msg $$ nest 2 extra) }
+
+  | otherwise      -- This can happen, by a recursive decomposition of frozen
+                   -- occurs check constraints
+                   -- Example: alpha ~ T Int alpha has frozen.
+                   --          Then alpha gets unified to T beta gamma
+                   -- So now we have  T beta gamma ~ T Int (T beta gamma)
+                   -- Decompose to (beta ~ Int, gamma ~ T beta gamma)
+                   -- The (gamma ~ T beta gamma) is the occurs check, but
+                   -- the (beta ~ Int) isn't an error at all.  So return ()
+  = return ()
+
   where         
     is_meta1 = isMetaTyVar tv1
     k1              = tyVarKind tv1
@@ -357,15 +489,27 @@ mkTyFunInfoMsg ty1 ty2
     pp_inj tc | isInjectiveTyCon tc = empty
               | otherwise = ptext (sLit (", and may not be injective"))
 
-misMatchMsgWithExtras :: TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc)
--- This version is used by TcSimplify too, which doesn't track the
--- expected/acutal thing, so we just have ty1 ty2 here
--- NB: The types are already tidied
-misMatchMsgWithExtras env ty1 ty2
-  = (env2, sep [ misMatchMsg ty1 ty2, nest 2 (extra1 $$ extra2) ])
+misMatchOrCND :: ReportErrCtxt -> TcType -> TcType -> SDoc
+misMatchOrCND ctxt ty1 ty2
+  = case getUserGivens ctxt of
+      Just givens -> couldNotDeduce givens [EqPred ty1 ty2]
+      Nothing     -> misMatchMsg ty1 ty2
+
+couldNotDeduce :: [EvVar] -> [PredType] -> SDoc
+couldNotDeduce givens wanteds
+  = sep [ ptext (sLit "Could not deduce") <+> pprTheta wanteds
+        , nest 2 $ ptext (sLit "from the context") 
+                     <+> pprEvVarTheta givens]
+
+addExtraInfo :: ReportErrCtxt -> TcType -> TcType -> ReportErrCtxt
+-- Add on extra info about the types themselves
+-- NB: The types themselves are already tidied
+addExtraInfo ctxt ty1 ty2
+  = ctxt { cec_tidy  = env2
+         , cec_extra = nest 2 (extra1 $$ extra2) $$ cec_extra ctxt }
   where
-    (env1, extra1) = typeExtraInfoMsg env ty1
-    (env2, extra2) = typeExtraInfoMsg env1 ty2
+    (env1, extra1) = typeExtraInfoMsg (cec_tidy ctxt) ty1
+    (env2, extra2) = typeExtraInfoMsg env1            ty2
 
 misMatchMsg :: TcType -> TcType -> SDoc           -- Types are already tidy
 misMatchMsg ty1 ty2 = sep [ ptext (sLit "Couldn't match type") <+> quotes (ppr ty1)
@@ -386,7 +530,7 @@ typeExtraInfoMsg env ty
   | Just tv <- tcGetTyVar_maybe ty
   , isTcTyVar tv
   , isSkolemTyVar tv || isSigTyVar tv
-  , not (isUnk tv)
+  , not (isUnkSkol tv)
   , let (env1, tv1) = tidySkolemTyVar env tv
   = (env1, pprSkolTvBinding tv1)
   where
@@ -428,43 +572,10 @@ Warn of loopy local equalities that were dropped.
 reportDictErrs :: ReportErrCtxt -> [PredType] -> CtOrigin -> TcM ()    
 reportDictErrs ctxt wanteds orig
   = do { inst_envs <- tcGetInstEnvs
-       ; let (others, overlaps) = partitionWith (check_overlap inst_envs) wanteds
-       ; unless (null others) $
-         addErrorReport ctxt (mk_no_inst_err others) 
-       ; mapM_ (addErrorReport ctxt) overlaps }
+       ; non_overlaps <- mapMaybeM (reportOverlap ctxt inst_envs orig) wanteds
+       ; unless (null non_overlaps) $
+         addErrorReport ctxt (mk_no_inst_err non_overlaps) }
   where
-    check_overlap :: (InstEnv,InstEnv) -> PredType -> Either PredType SDoc
-       -- Right msg  => overlap message
-       -- Left  inst => no instance
-    check_overlap inst_envs pred@(ClassP clas tys)
-       = case lookupInstEnv inst_envs clas tys of
-               ([], _) -> Left pred            -- No match
-               -- The case of exactly one match and no unifiers means a
-               -- successful lookup.  That can't happen here, because dicts
-               -- only end up here if they didn't match in Inst.lookupInst
-               ([_],[])
-                | debugIsOn -> pprPanic "check_overlap" (ppr pred)
-               res -> Right (mk_overlap_msg pred res)
-    check_overlap _ _ = panic "check_overlap"
-
-    mk_overlap_msg pred (matches, unifiers)
-      = ASSERT( not (null matches) )
-        vcat [ addArising orig (ptext (sLit "Overlapping instances for") 
-                               <+> pprPred pred)
-            ,  sep [ptext (sLit "Matching instances") <> colon,
-                    nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])]
-            ,  if not (isSingleton matches)
-               then    -- Two or more matches
-                    empty
-               else    -- One match, plus some unifiers
-               ASSERT( not (null unifiers) )
-               parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
-                                quotes (pprWithCommas ppr (varSetElems (tyVarsOfPred pred))),
-                             ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
-                             ptext (sLit "when compiling the other instance declarations")])]
-      where
-       ispecs = [ispec | (ispec, _) <- matches]
-
     mk_no_inst_err :: [PredType] -> SDoc
     mk_no_inst_err wanteds
       | Just givens <- getUserGivens ctxt
@@ -482,10 +593,13 @@ reportDictErrs ctxt wanteds orig
                           <+> ptext (sLit "to the context of")
                   , nest 2 $ pprErrCtxtLoc ctxt ]
 
-       fixes2 | null instance_dicts = []
-              | otherwise           = [sep [ptext (sLit "add an instance declaration for"),
-                                       pprTheta instance_dicts]]
-       instance_dicts = filterOut isTyVarClassPred wanteds
+        fixes2 = case instance_dicts of
+                   []  -> []
+                   [_] -> [sep [ptext (sLit "add an instance declaration for"),
+                                pprTheta instance_dicts]]
+                   _   -> [sep [ptext (sLit "add instance declarations for"),
+                                pprTheta instance_dicts]]
+        instance_dicts = filterOut isTyVarClassPred wanteds
                -- Insts for which it is worth suggesting an adding an 
                -- instance declaration.  Exclude tyvar dicts.
 
@@ -494,6 +608,94 @@ reportDictErrs ctxt wanteds orig
        show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"), 
                                 nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
 
+reportOverlap :: ReportErrCtxt -> (InstEnv,InstEnv) -> CtOrigin
+              -> PredType -> TcM (Maybe PredType)
+-- Report an overlap error if this class constraint results
+-- from an overlap (returning Nothing), otherwise return (Just pred)
+reportOverlap ctxt inst_envs orig pred@(ClassP clas tys)
+  = do { tys_flat <- mapM quickFlattenTy tys
+           -- Note [Flattening in error message generation]
+
+       ; case lookupInstEnv inst_envs clas tys_flat of
+                ([], _) -> return (Just pred)               -- No match
+               -- The case of exactly one match and no unifiers means a
+               -- successful lookup.  That can't happen here, because dicts
+               -- only end up here if they didn't match in Inst.lookupInst
+               ([_],[])
+                | debugIsOn -> pprPanic "check_overlap" (ppr pred)
+                res          -> do { addErrorReport ctxt (mk_overlap_msg res)
+                                   ; return Nothing } }
+  where
+    mk_overlap_msg (matches, unifiers)
+      = ASSERT( not (null matches) )
+        vcat [ addArising orig (ptext (sLit "Overlapping instances for") 
+                               <+> pprPred pred)
+            ,  sep [ptext (sLit "Matching instances") <> colon,
+                    nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])]
+            ,  if not (isSingleton matches)
+               then    -- Two or more matches
+                    empty
+               else    -- One match, plus some unifiers
+               ASSERT( not (null unifiers) )
+               parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
+                                quotes (pprWithCommas ppr (varSetElems (tyVarsOfPred pred))),
+                             ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
+                             ptext (sLit "when compiling the other instance declarations")])]
+      where
+       ispecs = [ispec | (ispec, _) <- matches]
+
+reportOverlap _ _ _ _ = panic "reportOverlap"    -- Not a ClassP
+
+----------------------
+quickFlattenTy :: TcType -> TcM TcType
+-- See Note [Flattening in error message generation]
+quickFlattenTy ty | Just ty' <- tcView ty = quickFlattenTy ty'
+quickFlattenTy ty@(TyVarTy {})  = return ty
+quickFlattenTy ty@(ForAllTy {}) = return ty     -- See
+quickFlattenTy ty@(PredTy {})   = return ty     -- Note [Quick-flatten polytypes]
+  -- Don't flatten because of the danger or removing a bound variable
+quickFlattenTy (AppTy ty1 ty2) = do { fy1 <- quickFlattenTy ty1
+                                    ; fy2 <- quickFlattenTy ty2
+                                    ; return (AppTy fy1 fy2) }
+quickFlattenTy (FunTy ty1 ty2) = do { fy1 <- quickFlattenTy ty1
+                                    ; fy2 <- quickFlattenTy ty2
+                                    ; return (FunTy fy1 fy2) }
+quickFlattenTy (TyConApp tc tys)
+    | not (isSynFamilyTyCon tc)
+    = do { fys <- mapM quickFlattenTy tys 
+         ; return (TyConApp tc fys) }
+    | otherwise
+    = do { let (funtys,resttys) = splitAt (tyConArity tc) tys
+                -- Ignore the arguments of the type family funtys
+         ; v <- newMetaTyVar TauTv (typeKind (TyConApp tc funtys))
+         ; flat_resttys <- mapM quickFlattenTy resttys
+         ; return (foldl AppTy (mkTyVarTy v) flat_resttys) }
+\end{code}
+
+Note [Flattening in error message generation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (C (Maybe (F x))), where F is a type function, and we have
+instances
+                C (Maybe Int) and C (Maybe a)
+Since (F x) might turn into Int, this is an overlap situation, and
+indeed (because of flattening) the main solver will have refrained
+from solving.  But by the time we get to error message generation, we've
+un-flattened the constraint.  So we must *re*-flatten it before looking
+up in the instance environment, lest we only report one matching
+instance when in fact there are two.
+
+Re-flattening is pretty easy, because we don't need to keep track of
+evidence.  We don't re-use the code in TcCanonical because that's in
+the TcS monad, and we are in TcM here.
+
+Note [Quick-flatten polytypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we see C (Ix a => blah) or C (forall a. blah) we simply refrain from
+flattening any further.  After all, there can be no instance declarations
+that match such things.  And flattening under a for-all is problematic
+anyway; consider C (forall a. F a)
+
+\begin{code}
 reportAmbigErrs :: ReportErrCtxt -> TcTyVarSet -> [WantedEvVar] -> TcM ()
 reportAmbigErrs ctxt skols ambigs 
 -- Divide into groups that share a common set of ambiguous tyvars
@@ -523,10 +725,11 @@ mkMonomorphismMsg :: ReportErrCtxt -> [TcTyVar] -> TcM (TidyEnv, SDoc)
 -- ASSUMPTION: the Insts are fully zonked
 mkMonomorphismMsg ctxt inst_tvs
   = do { dflags <- getDOpts
-       ; (tidy_env, docs) <- findGlobals ctxt (mkVarSet inst_tvs)
+       ; traceTc "Mono" (vcat (map pprSkolTvBinding inst_tvs))
+        ; (tidy_env, docs) <- findGlobals ctxt (mkVarSet inst_tvs)
        ; return (tidy_env, mk_msg dflags docs) }
   where
-    mk_msg _ _ | any isRuntimeUnk inst_tvs
+    mk_msg _ _ | any isRuntimeUnkSkol inst_tvs  -- See Note [Runtime skolems]
         =  vcat [ptext (sLit "Cannot resolve unknown runtime types:") <+>
                    (pprWithCommas ppr inst_tvs),
                 ptext (sLit "Use :print or :force to determine these types")]
@@ -626,6 +829,12 @@ warnDefaulting wanteds default_ty
     (loc, ppr_wanteds) = pprWithArising wanteds
 \end{code}
 
+Note [Runtime skolems]
+~~~~~~~~~~~~~~~~~~~~~~
+We want to give a reasonably helpful error message for ambiguity
+arising from *runtime* skolems in the debugger.  These
+are created by in RtClosureInspect.zonkRTTIType.  
+
 %************************************************************************
 %*                                                                     *
                  Error from the canonicaliser
@@ -634,43 +843,6 @@ warnDefaulting wanteds default_ty
 %************************************************************************
 
 \begin{code}
-kindErrorTcS :: CtFlavor -> TcType -> TcType -> TcS ()
--- If there's a kind error, we don't want to blindly say "kind error"
--- We might, say, be unifying a skolem 'a' with a type 'Int', 
--- in which case that's the error to report.  So we set things
--- up to call reportEqErr, which does the business properly
-kindErrorTcS fl ty1 ty2
-  = wrapEqErrTcS fl ty1 ty2 $ \ env0 ty1 ty2 extra -> 
-    do { let ctxt = CEC { cec_encl = []
-                        , cec_extra = extra
-                        , cec_tidy = env0 }
-       ; reportEqErr ctxt ty1 ty2 }
-
-misMatchErrorTcS :: CtFlavor -> TcType -> TcType -> TcS a
-misMatchErrorTcS fl ty1 ty2
-  = wrapEqErrTcS fl ty1 ty2 $ \ env0 ty1 ty2 extra -> 
-    do { let (env1, msg)  = misMatchMsgWithExtras env0 ty1 ty2
-       ; failWithTcM (env1, inaccessible_msg $$ msg $$ extra) }
-  where
-    inaccessible_msg 
-      = case fl of 
-          Given loc -> hang (ptext (sLit "Inaccessible code in"))
-                          2 (mk_what loc)
-          _         -> empty
-    mk_what loc 
-      = case ctLocOrigin loc of
-          PatSkol dc mc -> sep [ ptext (sLit "a pattern with constructor") 
-                                   <+> quotes (ppr dc) <> comma
-                               , ptext (sLit "in") <+> pprMatchContext mc ]
-         other_skol -> pprSkolInfo other_skol
-
-occursCheckErrorTcS :: CtFlavor -> TcTyVar -> TcType -> TcS a
-occursCheckErrorTcS fl tv ty
-  = wrapEqErrTcS fl (mkTyVarTy tv) ty $ \ env0 ty1 ty2 extra2 -> 
-    do { let extra1 = sep [ppr ty1, char '=', ppr ty2]
-       ; failWithTcM (env0, hang msg 2 (extra1 $$ extra2)) }
-  where
-    msg = text $ "Occurs check: cannot construct the infinite type:"
 
 solverDepthErrorTcS :: Int -> [CanonicalCt] -> TcS a
 solverDepthErrorTcS depth stack
@@ -709,34 +881,9 @@ flattenForAllErrorTcS fl ty _bad_eqs
 
 \begin{code}
 setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a
-setCtFlavorLoc (Wanted  loc) thing = setCtLoc loc thing
-setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing
-setCtFlavorLoc (Given   loc) thing = setCtLoc loc thing
-
-wrapEqErrTcS :: CtFlavor -> TcType -> TcType
-             -> (TidyEnv -> TcType -> TcType -> SDoc -> TcM a)
-             -> TcS a
-wrapEqErrTcS fl ty1 ty2 thing_inside
-  = do { ty_binds_var <- getTcSTyBinds
-       ; wrapErrTcS $ setCtFlavorLoc fl $ 
-    do {   -- Apply the current substitition
-           -- and zonk to get rid of flatten-skolems
-       ; ty_binds_bag <- readTcRef ty_binds_var
-       ; let subst = mkOpenTvSubst (mkVarEnv (bagToList ty_binds_bag))
-       ; env0 <- tcInitTidyEnv 
-       ; (env1, ty1) <- zonkSubstTidy env0 subst ty1
-       ; (env2, ty2) <- zonkSubstTidy env1 subst ty2
-       ; let do_wanted loc = do { (env3, extra) <- getWantedEqExtra subst env2 
-                                                     (ctLocOrigin loc) ty1 ty2
-                                ; thing_inside env3 ty1 ty2 extra } 
-       ; case fl of
-           Wanted  loc -> do_wanted loc
-           Derived loc -> do_wanted loc
-           Given {}    -> thing_inside env2 ty1 ty2 empty 
-                                -- We could print more info, but it
-                                 -- seems to be coming out already
-       } }  
-  where
+setCtFlavorLoc (Wanted  loc)   thing = setCtLoc loc thing
+setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing
+setCtFlavorLoc (Given   loc)   thing = setCtLoc loc thing
 
 getWantedEqExtra :: TvSubst -> TidyEnv -> CtOrigin -> TcType -> TcType
                  -> TcM (TidyEnv, SDoc)