Adding pushing of hpc translation status through hi files.
[ghc-hetmet.git] / compiler / typecheck / TcUnify.lhs
index 39c3cbd..821a1cc 100644 (file)
@@ -1,7 +1,9 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
-\section{Type subsumption and unification}
+
+Type subsumption and unification
 
 \begin{code}
 module TcUnify (
@@ -17,7 +19,7 @@ module TcUnify (
 
   --------------------------------
   -- Holes
-  tcInfer, subFunTys, unBox, stripBoxyType, withBox, 
+  tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, 
   boxyUnify, boxyUnifyList, zapToMonotype,
   boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
   wrapFunResCoercion
@@ -25,61 +27,30 @@ module TcUnify (
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsWrapper(..), idHsWrapper, isIdHsWrapper, (<.>),
-                         mkWpLams, mkWpTyLams, mkWpApps )
-import TypeRep         ( Type(..), PredType(..) )
-
-import TcMType         ( lookupTcTyVar, LookupTyVarResult(..),
-                          tcInstSkolType, tcInstBoxyTyVar, newKindVar, newMetaTyVar,
-                         newBoxyTyVar, newBoxyTyVarTys, readFilledBox, 
-                         readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy,
-                         tcInstSkolTyVars, tcInstTyVar,
-                         zonkTcKind, zonkType, zonkTcType,  zonkTcTyVarsAndFV, 
-                         readKindVar, writeKindVar )
-import TcSimplify      ( tcSimplifyCheck )
-import TcEnv           ( tcGetGlobalTyVars, findGlobals )
-import TcIface         ( checkWiredInTyCon )
+import HsSyn
+import TypeRep
+
+import TcMType
+import TcSimplify
+import TcEnv
+import TcIface
 import TcRnMonad         -- TcType, amongst others
-import TcType          ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType,
-                         BoxySigmaType, BoxyRhoType, BoxyType, 
-                         TcTyVarSet, TcThetaType, TcTyVarDetails(..), BoxInfo(..), 
-                         SkolemInfo( GenSkol, UnkSkol ), MetaDetails(..), isImmutableTyVar,
-                         pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy, 
-                         mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar,
-                         tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys,
-                         tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, 
-                         typeKind, mkForAllTys, mkAppTy, isBoxyTyVar,
-                         tcView, exactTyVarsOfType, 
-                         tidyOpenType, tidyOpenTyVar, tidyOpenTyVars,
-                         pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar,
-                         TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst, 
-                         substTy, substTheta, 
-                         lookupTyVar, extendTvSubst )
-import Type            ( Kind, SimpleKind, KindVar, 
-                         openTypeKind, liftedTypeKind, unliftedTypeKind, 
-                         mkArrowKind, defaultKind,
-                         argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
-                         isSubKind, pprKind, splitKindFunTys, isSubKindCon,
-                          isOpenTypeKind, isArgTypeKind )
-import TysPrim         ( alphaTy, betaTy )
-import Inst            ( newDictBndrsO, instCall, instToId )
-import TyCon           ( TyCon, tyConArity, tyConTyVars, isSynTyCon )
-import TysWiredIn      ( listTyCon )
-import Id              ( Id )
-import Var             ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails )
+import TcType
+import Type
+import TysPrim
+import Inst
+import TyCon
+import TysWiredIn
+import Var
 import VarSet
 import VarEnv
-import Name            ( Name, isSystemName )
-import ErrUtils                ( Message )
-import Maybes          ( expectJust, isNothing )
-import BasicTypes      ( Arity )
-import Util            ( notNull, equalLength )
+import Module
+import Name
+import ErrUtils
+import Maybes
+import BasicTypes
+import Util
 import Outputable
-
--- Assertion imports
-#ifdef DEBUG
-import TcType          ( isBoxyTy, isFlexi )
-#endif
 \end{code}
 
 %************************************************************************
@@ -95,7 +66,7 @@ tcInfer tc_infer
        ; res <- tc_infer (mkTyVarTy box)
        ; res_ty <- readFilledBox box   -- Guaranteed filled-in by now
        ; return (res, res_ty) }
-\end{code}                
+\end{code}
 
 
 %************************************************************************
@@ -142,13 +113,14 @@ subFunTys error_herald n_pats res_ty thing_inside
   where
        -- In 'loop', the parameter 'arg_tys' accumulates 
        -- the arg types so far, in *reverse order*
+       -- INVARIANT:   res_ty :: *
     loop n args_so_far res_ty
        | Just res_ty' <- tcView res_ty  = loop n args_so_far res_ty'
 
     loop n args_so_far res_ty
        | isSigmaTy res_ty      -- Do this before checking n==0, because we 
                                -- guarantee to return a BoxyRhoType, not a BoxySigmaType
-       = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ res_ty' ->
+       = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
                                         loop n args_so_far res_ty'
             ; return (gen_fn <.> co_fn, res) }
 
@@ -172,7 +144,7 @@ subFunTys error_herald n_pats res_ty thing_inside
               else loop n args_so_far (FunTy arg_ty' res_ty') }
 
     loop n args_so_far (TyVarTy tv)
-        | not (isImmutableTyVar tv)
+        | isTyConableTyVar tv
        = do { cts <- readMetaTyVar tv 
             ; case cts of
                 Indirect ty -> loop n args_so_far ty
@@ -223,10 +195,12 @@ boxySplitTyConApp tc orig_ty
        return (args ++ args_so_far)
 
     loop n_req args_so_far (AppTy fun arg)
+      | n_req > 0
       = loop (n_req - 1) (arg:args_so_far) fun
 
     loop n_req args_so_far (TyVarTy tv)
-      | not (isImmutableTyVar tv)
+      | isTyConableTyVar tv
+      , res_kind `isSubKind` tyVarKind tv
       = do { cts <- readMetaTyVar tv
           ; case cts of
               Indirect ty -> loop n_req args_so_far ty
@@ -235,7 +209,7 @@ boxySplitTyConApp tc orig_ty
        }
       where
        mk_res_ty arg_tys' = mkTyConApp tc arg_tys'
-       arg_kinds = map tyVarKind (take n_req (tyConTyVars tc))
+       (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc)
 
     loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty
 
@@ -248,7 +222,8 @@ boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty
 ----------------------
 boxySplitAppTy :: BoxyRhoType                          -- Type to split: m a
               -> TcM (BoxySigmaType, BoxySigmaType)    -- Returns m, a
--- Assumes (m: * -> k), where k is the kind of the incoming type
+-- If the incoming type is a mutable type variable of kind k, then 
+-- boxySplitAppTy returns a new type variable (m: * -> k); note the *.
 -- If the incoming type is boxy, then so are the result types; and vice versa
 
 boxySplitAppTy orig_ty
@@ -262,7 +237,7 @@ boxySplitAppTy orig_ty
       = return (fun_ty, arg_ty)
 
     loop (TyVarTy tv)
-      | not (isImmutableTyVar tv)
+      | isTyConableTyVar tv
       = do { cts <- readMetaTyVar tv
           ; case cts of
               Indirect ty -> loop ty
@@ -552,7 +527,7 @@ boxyLub orig_ty1 orig_ty2
 
        -- Look inside type synonyms, but only if the naive version fails
     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
-              | Just ty2' <- tcView ty1 = go ty1 ty2'
+              | Just ty2' <- tcView ty2 = go ty1 ty2'
 
     -- For now, we don't look inside ForAlls, PredTys
     go ty1 ty2 = orig_ty1      -- Default
@@ -637,7 +612,8 @@ tc_sub :: SubCtxt           -- How to add an error-context
 -- e.g. in the SPEC rule where we just use splitSigmaTy 
        
 tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
-  = tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+  = traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >>
+    tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
        -- This indirection is just here to make 
        -- it easy to insert a debug trace!
 
@@ -667,9 +643,11 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
 -- Consider  f g !
 
 tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
-  | not exp_ib,        -- SKOL does not apply if exp_ty is inside a box
-    isSigmaTy exp_ty   
-  = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty ->
+  | isSigmaTy exp_ty   
+  = if exp_ib then     -- SKOL does not apply if exp_ty is inside a box
+       defer_to_boxy_matching sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+    else do 
+       { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
                             tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty
        ; return (gen_fn <.> co_fn) }
   where
@@ -712,7 +690,13 @@ tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
        ; co_fn2 <- tc_sub sub_ctxt tau' tau' exp_ib exp_sty expected_ty
 
                -- Deal with the dictionaries
-       ; co_fn1 <- instCall InstSigOrigin inst_tys (substTheta subst' theta)
+               -- The origin gives a helpful origin when we have
+               -- a function with type f :: Int -> forall a. Num a => ...
+               -- This way the (Num a) dictionary gets an OccurrenceOf f origin
+       ; let orig = case sub_ctxt of
+                       SubFun n -> OccurrenceOf n
+                       other    -> InstSigOrigin       -- Unhelpful
+       ; co_fn1 <- instCall orig inst_tys (substTheta subst' theta)
        ; return (co_fn2 <.> co_fn1) }
 
 -----------------------------------
@@ -737,10 +721,17 @@ tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_t
 
 -- Everything else: defer to boxy matching
 tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+  = defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+
+-----------------------------------
+defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
   = do { addSubCtxt sub_ctxt act_sty exp_sty $
-         u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty
+         u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty
        ; return idHsWrapper }
-
+  where
+    outer = case sub_ctxt of           -- Ugh
+               SubDone -> False
+               other   -> True
 
 -----------------------------------
 tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
@@ -774,7 +765,7 @@ tcGen :: BoxySigmaType                              -- expected_ty
       -> TcTyVarSet                            -- Extra tyvars that the universally
                                                --      quantified tyvars of expected_ty
                                                --      must not be unified
-      -> (BoxyRhoType -> TcM result)           -- spec_ty
+      -> ([TcTyVar] -> BoxyRhoType -> TcM result)
       -> TcM (HsWrapper, result)
        -- The expression has type: spec_ty -> expected_ty
 
@@ -784,22 +775,21 @@ tcGen expected_ty extra_tvs thing_inside  -- We expect expected_ty to be a forall
                -- mention the *instantiated* tyvar names, so that we get a
                -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
                -- Hence the tiresome but innocuous fixM
-         ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
+         ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
                do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
-                  ; span <- getSrcSpanM
-                  ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
+                       -- Get loation from monad, not from expected_ty
+                  ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
                   ; return ((forall_tvs, theta, rho_ty), skol_info) })
 
 #ifdef DEBUG
        ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
                                    text "expected_ty" <+> ppr expected_ty,
-                                   text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
-                                   text "free_tvs" <+> ppr free_tvs,
-                                   text "forall_tvs" <+> ppr forall_tvs])
+                                   text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho',
+                                   text "free_tvs" <+> ppr free_tvs])
 #endif
 
        -- Type-check the arg and unify with poly type
-       ; (result, lie) <- getLIE (thing_inside rho_ty)
+       ; (result, lie) <- getLIE (thing_inside tvs' rho')
 
        -- Check that the "forall_tvs" havn't been constrained
        -- The interesting bit here is that we must include the free variables
@@ -812,20 +802,20 @@ tcGen expected_ty extra_tvs thing_inside  -- We expect expected_ty to be a forall
        -- Conclusion: include the free vars of the expected_ty in the
        -- list of "free vars" for the signature check.
 
-       ; dicts <- newDictBndrsO (SigOrigin skol_info) theta
-       ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
+       ; loc <- getInstLoc (SigOrigin skol_info)
+       ; dicts <- newDictBndrs loc theta'
+       ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
 
-       ; checkSigTyVarsWrt free_tvs forall_tvs
+       ; checkSigTyVarsWrt free_tvs tvs'
        ; traceTc (text "tcGen:done")
 
        ; let
            -- The WpLet binds any Insts which came out of the simplification.
                dict_ids = map instToId dicts
-               co_fn = mkWpTyLams forall_tvs <.> mkWpLams dict_ids <.> WpLet inst_binds
+               co_fn = mkWpTyLams tvs' <.> mkWpLams dict_ids <.> WpLet inst_binds
        ; returnM (co_fn, result) }
   where
     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
-    sig_msg  = ptext SLIT("expected type of an expression")
 \end{code}    
 
     
@@ -872,7 +862,8 @@ unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
 -- Acutal and expected types
 unifyTheta theta1 theta2
   = do { checkTc (equalLength theta1 theta2)
-                 (ptext SLIT("Contexts differ in length"))
+                 (vcat [ptext SLIT("Contexts differ in length"),
+                        nest 2 $ parens $ ptext SLIT("Use -fglasgow-exts to allow this")])
        ; uList unifyPred theta1 theta2 }
 
 ---------------
@@ -966,8 +957,51 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
     go outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
     go outer ty1 (TyVarTy tyvar2) = uVar outer True  tyvar2 nb1 orig_ty1 ty1
                                -- "True" means args swapped
+
+       -- The case for sigma-types must *follow* the variable cases
+       -- because a boxy variable can be filed with a polytype;
+       -- but must precede FunTy, because ((?x::Int) => ty) look
+       -- like a FunTy; there isn't necy a forall at the top
+    go _ ty1 ty2
+      | isSigmaTy ty1 || isSigmaTy ty2
+      = do   { checkM (equalLength tvs1 tvs2)
+                     (unifyMisMatch outer False orig_ty1 orig_ty2)
+
+            ; tvs <- tcInstSkolTyVars UnkSkol tvs1     -- Not a helpful SkolemInfo
+                       -- Get location from monad, not from tvs1
+            ; let tys      = mkTyVarTys tvs
+                  in_scope = mkInScopeSet (mkVarSet tvs)
+                  phi1   = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
+                  phi2   = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
+                  (theta1,tau1) = tcSplitPhiTy phi1
+                  (theta2,tau2) = tcSplitPhiTy phi2
+
+            ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
+            { checkM (equalLength theta1 theta2)
+                     (unifyMisMatch outer False orig_ty1 orig_ty2)
+            
+            ; uPreds False nb1 theta1 nb2 theta2
+            ; uTys nb1 tau1 nb2 tau2
+
+               -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
+            ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
+            ; ifM (any (`elemVarSet` free_tvs) tvs)
+                  (bleatEscapedTvs free_tvs tvs tvs)
+
+               -- If both sides are inside a box, we are in a "box-meets-box"
+               -- situation, and we should not have a polytype at all.  
+               -- If we get here we have two boxes, already filled with
+               -- the same polytype... but it should be a monotype.
+               -- This check comes last, because the error message is 
+               -- extremely unhelpful.  
+            ; ifM (nb1 && nb2) (notMonoType ty1)
+            }}
+      where
+       (tvs1, body1) = tcSplitForAllTys ty1
+       (tvs2, body2) = tcSplitForAllTys ty2
+
        -- Predicates
-    go outer (PredTy p1) (PredTy p2) = uPred outer nb1 p1 nb2 p2
+    go outer (PredTy p1) (PredTy p2) = uPred False nb1 p1 nb2 p2
 
        -- Type constructors must match
     go _ (TyConApp con1 tys1) (TyConApp con2 tys2)
@@ -993,26 +1027,6 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
       | Just (s1,t1) <- tcSplitAppTy_maybe ty1
       = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
 
-    go _ ty1@(ForAllTy _ _) ty2@(ForAllTy _ _)
-      | length tvs1 == length tvs2
-      = do   { tvs <- tcInstSkolTyVars UnkSkol tvs1    -- Not a helpful SkolemInfo
-            ; let tys      = mkTyVarTys tvs
-                  in_scope = mkInScopeSet (mkVarSet tvs)
-                  subst1   = mkTvSubst in_scope (zipTyEnv tvs1 tys)
-                  subst2   = mkTvSubst in_scope (zipTyEnv tvs2 tys)
-            ; uTys nb1 (substTy subst1 body1) nb2 (substTy subst2 body2)
-
-               -- If both sides are inside a box, we are in a "box-meets-box"
-               -- situation, and we should not have a polytype at all.  
-               -- If we get here we have two boxes, already filled with
-               -- the same polytype... but it should be a monotype.
-               -- This check comes last, because the error message is 
-               -- extremely unhelpful.  
-            ; ifM (nb1 && nb2) (notMonoType ty1)
-            }
-      where
-       (tvs1, body1) = tcSplitForAllTys ty1
-       (tvs2, body2) = tcSplitForAllTys ty2
 
        -- Anything else fails
     go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
@@ -1023,6 +1037,10 @@ uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
 uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
   | c1 == c2 = uTys_s nb1 tys1 nb2 tys2                -- Guaranteed equal lengths because the kinds check
 uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2)
+
+uPreds outer nb1 []       nb2 []       = return ()
+uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = uPred outer nb1 p1 nb2 p2 >> uPreds outer nb1 ps1 nb2 ps2
+uPreds outer nb1 ps1      nb2 ps2      = panic "uPreds"
 \end{code}
 
 Note [Tycon app]
@@ -1262,7 +1280,7 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
     k1_sub_k2 = k1 `isSubKind` k2
     k2_sub_k1 = k2 `isSubKind` k1
 
-    nicer_to_update_tv1 = isSystemName (varName tv1)
+    nicer_to_update_tv1 = isSystemName (Var.varName tv1)
        -- Try to update sys-y type variables in preference to ones
        -- gotten (say) by instantiating a polymorphic function with
        -- a user-written type sig
@@ -1363,7 +1381,11 @@ checkTauTvUpdate orig_tv orig_ty
             ; case mb_tys' of
                Just tys' -> return (TyConApp tc tys')
                                -- Retain the synonym (the common case)
-               Nothing   -> go (expectJust "checkTauTvUpdate" 
+               Nothing | isOpenTyCon tc
+                         -> notMonoArgs (TyConApp tc tys)
+                               -- Synonym families must have monotype args
+                       | otherwise
+                         -> go (expectJust "checkTauTvUpdate" 
                                        (tcView (TyConApp tc tys)))
                                -- Try again, expanding the synonym
             }
@@ -1403,16 +1425,27 @@ But we should not reject the program, because A t = ().
 Rather, we should bind t to () (= non_var_ty2).
 
 \begin{code}
-stripBoxyType :: BoxyType -> TcM TcType
--- Strip all boxes from the input type, returning a non-boxy type.
--- It's fine for there to be a polytype inside a box (c.f. unBox)
--- All of the boxes should have been filled in by now; 
--- hence we return a TcType
-stripBoxyType ty = zonkType strip_tv ty
-  where
-    strip_tv tv = ASSERT( not (isBoxyTyVar tv) ) return (TyVarTy tv)
-       -- strip_tv will be called for *Flexi* meta-tyvars
-       -- There should not be any Boxy ones; hence the ASSERT
+refineBox :: TcType -> TcM TcType
+-- Unbox the outer box of a boxy type (if any)
+refineBox ty@(TyVarTy box_tv) 
+  | isMetaTyVar box_tv
+  = do { cts <- readMetaTyVar box_tv
+       ; case cts of
+               Flexi       -> return ty
+               Indirect ty -> return ty } 
+refineBox other_ty = return other_ty
+
+refineBoxToTau :: TcType -> TcM TcType
+-- Unbox the outer box of a boxy type, filling with a monotype if it is empty
+-- Like refineBox except for the "fill with monotype" part.
+refineBoxToTau ty@(TyVarTy box_tv) 
+  | isMetaTyVar box_tv
+  , MetaTv BoxTv ref <- tcTyVarDetails box_tv
+  = do { cts <- readMutVar ref
+       ; case cts of
+               Flexi       -> fillBoxWithTau box_tv ref
+               Indirect ty -> return ty } 
+refineBoxToTau other_ty = return other_ty
 
 zapToMonotype :: BoxySigmaType -> TcM TcTauType
 -- Subtle... we must zap the boxy res_ty
@@ -1519,6 +1552,16 @@ addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside
        <+> ptext SLIT("arguments")
 
 ------------------
+unifyForAllCtxt tvs phi1 phi2 env
+  = returnM (env2, msg)
+  where
+    (env', tvs') = tidyOpenTyVars env tvs      -- NB: not tidyTyVarBndrs
+    (env1, phi1') = tidyOpenType env' phi1
+    (env2, phi2') = tidyOpenType env1 phi2
+    msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')),
+               ptext SLIT("          and") <+> quotes (ppr (mkForAllTys tvs' phi2'))]
+
+------------------
 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
        -- tv1 and ty2 are zonked already
   = returnM msg
@@ -1542,31 +1585,59 @@ unifyMisMatch outer swapped ty1 ty2
                   else failWithTcM (env, msg)
        } 
 
+-----------------------
+misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
+-- Generate the message when two types fail to match,
+-- going to some trouble to make it helpful
 misMatchMsg ty1 ty2
   = do { env0 <- tcInitTidyEnv
-       ; (env1, pp1, extra1) <- ppr_ty env0 ty1
-       ; (env2, pp2, extra2) <- ppr_ty env1 ty2
+       ; (env1, pp1, extra1) <- ppr_ty env0 ty1 ty2
+       ; (env2, pp2, extra2) <- ppr_ty env1 ty2 ty1
        ; return (env2, sep [sep [ptext SLIT("Couldn't match expected type") <+> pp1, 
                                  nest 7 (ptext SLIT("against inferred type") <+> pp2)],
-                            nest 2 extra1, nest 2 extra2]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
-  = do { ty' <- zonkTcType ty
-       ; let (env1,tidy_ty) = tidyOpenType env ty'
-            simple_result  = (env1, quotes (ppr tidy_ty), empty)
-       ; case tidy_ty of
-          TyVarTy tv 
-               | isSkolemTyVar tv || isSigTyVar tv
-               -> return (env2, pp_rigid tv', pprSkolTvBinding tv')
-               | otherwise -> return simple_result
-               where
-                 (env2, tv') = tidySkolemTyVar env1 tv
-          other -> return simple_result }
+                            nest 2 (extra1 $$ extra2)]) }
+
+ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc)
+ppr_ty env ty other_ty 
+  = do { ty' <- zonkTcType ty
+       ; let (env1, tidy_ty) = tidyOpenType env ty'
+       ; (env2, extra) <- ppr_extra env1 tidy_ty other_ty
+       ; return (env2, quotes (ppr tidy_ty), extra) }
+
+-- (ppr_extra env ty other_ty) shows extra info about 'ty'
+ppr_extra env (TyVarTy tv) other_ty
+  | isSkolemTyVar tv || isSigTyVar tv
+  = return (env1, pprSkolTvBinding tv1)
   where
-    pp_rigid tv = quotes (ppr tv) <+> parens (ptext SLIT("a rigid variable"))
+    (env1, tv1) = tidySkolemTyVar env tv
+
+ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _) 
+  | getOccName tc1 == getOccName tc2
+  = -- This case helps with messages that would otherwise say
+    --    Could not match 'T' does not match 'M.T'
+    -- which is not helpful
+    do { this_mod <- getModule
+       ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined") <+> mk_mod this_mod) }
+  where
+    tc_mod  = nameModule (getName tc1)
+    tc_pkg  = modulePackageId tc_mod
+    tc2_pkg = modulePackageId (nameModule (getName tc2))
+    mk_mod this_mod 
+       | tc_mod == this_mod = ptext SLIT("in this module")
+
+       | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg
+               -- Suppress the module name if (a) it's from another package
+               --                             (b) other_ty isn't from that same package
+
+       | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg
+       where
+         home_pkg = tc_pkg == modulePackageId this_mod
+         pp_pkg | home_pkg  = empty
+                | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg)
 
+ppr_extra env ty other_ty = return (env, empty)                -- Normal case
 
+-----------------------
 notMonoType ty
   = do { ty' <- zonkTcType ty
        ; env0 <- tcInitTidyEnv
@@ -1574,6 +1645,13 @@ notMonoType ty
              msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
        ; failWithTcM (env1, msg) }
 
+notMonoArgs ty
+  = do { ty' <- zonkTcType ty
+       ; env0 <- tcInitTidyEnv
+       ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+             msg = ptext SLIT("Arguments of synonym family must be monotypes") <+> quotes (ppr tidy_ty)
+       ; failWithTcM (env1, msg) }
+
 occurCheck tyvar ty
   = do { env0 <- tcInitTidyEnv
        ; ty'  <- zonkTcType ty
@@ -1731,6 +1809,10 @@ unifyFunKind other                      = returnM Nothing
 checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
 -- A fancy wrapper for 'unifyKind', which tries 
 -- to give decent error messages.
+--     (checkExpectedKind ty act_kind exp_kind)
+-- checks that the actual kind act_kind is compatible 
+--     with the expected kind exp_kind
+-- The first argument, ty, is used only in the error message generation
 checkExpectedKind ty act_kind exp_kind
   | act_kind `isSubKind` exp_kind -- Short cut for a very common case
   = returnM ()