Improve error reporting for kind errors (fix Trac #1633)

[ghc-hetmet.git] / compiler / typecheck / TcUnify.lhs

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 84d79f6..e5e16fc 100644 (file)
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -6,13 +6,6 @@
 Type subsumption and unification
 
 \begin{code}
 Type subsumption and unification
 
 \begin{code}

-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-

 module TcUnify (
         -- Full-blown subsumption
   tcSubExp, tcGen,
 module TcUnify (
         -- Full-blown subsumption
   tcSubExp, tcGen,

@@ -21,7 +14,6 @@ module TcUnify (
         -- Various unifications
   unifyType, unifyTypeList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind,
         -- Various unifications
   unifyType, unifyTypeList, unifyTheta,
   unifyKind, unifyKinds, unifyFunKind,

-  checkExpectedKind,

   preSubType, boxyMatchTypes,
 
   --------------------------------
   preSubType, boxyMatchTypes,
 
   --------------------------------

@@ -59,7 +51,6 @@ import Maybes
 import BasicTypes
 import Util
 import Outputable
 import BasicTypes
 import Util
 import Outputable

-import Unique

 import FastString
 
 import Control.Monad
 import FastString
 
 import Control.Monad

@@ -84,10 +75,12 @@ tcInfer tc_infer = withBox openTypeKind tc_infer
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-subFunTys :: SDoc  -- Somthing like "The function f has 3 arguments"
+subFunTys :: SDoc  -- Something like "The function f has 3 arguments"

                    -- or "The abstraction (\x.e) takes 1 argument"
           -> Arity              -- Expected # of args
                    -- or "The abstraction (\x.e) takes 1 argument"
           -> Arity              -- Expected # of args

-          -> BoxyRhoType        -- res_ty
+          -> BoxySigmaType      -- res_ty
+         -> Maybe UserTypeCtxt -- Whether res_ty arises from a user signature
+                               -- Only relevant if we encounter a sigma-type

           -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
           -> TcM (HsWrapper, a)
 -- Attempt to decompse res_ty to have enough top-level arrows to
           -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
           -> TcM (HsWrapper, a)
 -- Attempt to decompse res_ty to have enough top-level arrows to

@@ -116,7 +109,7 @@ subFunTys :: SDoc  -- Somthing like "The function f has 3 arguments"
 -}
 
 
 -}
 
 

-subFunTys error_herald n_pats res_ty thing_inside
+subFunTys error_herald n_pats res_ty mb_ctxt thing_inside

   = loop n_pats [] res_ty
   where
         -- In 'loop', the parameter 'arg_tys' accumulates
   = loop n_pats [] res_ty
   where
         -- In 'loop', the parameter 'arg_tys' accumulates

@@ -129,8 +122,8 @@ subFunTys error_herald n_pats res_ty thing_inside
         | isSigmaTy res_ty      -- Do this before checking n==0, because we
                                 -- guarantee to return a BoxyRhoType, not a
                                 -- BoxySigmaType
         | 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' ->
-                                         loop n args_so_far res_ty'
+        = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet mb_ctxt $ \ _ res_ty ->
+                                         loop n args_so_far res_ty

              ; return (gen_fn <.> co_fn, res) }
 
     loop 0 args_so_far res_ty
              ; return (gen_fn <.> co_fn, res) }
 
     loop 0 args_so_far res_ty

@@ -143,7 +136,7 @@ subFunTys error_herald n_pats res_ty thing_inside
              ; return (co_fn', res) }
 
         -- Try to normalise synonym families and defer if that's not possible
              ; return (co_fn', res) }
 
         -- Try to normalise synonym families and defer if that's not possible

-    loop n args_so_far ty@(TyConApp tc tys)
+    loop n args_so_far ty@(TyConApp tc _)

         | isOpenSynTyCon tc
         = do { (coi1, ty') <- tcNormaliseFamInst ty
              ; case coi1 of
         | isOpenSynTyCon tc
         = do { (coi1, ty') <- tcNormaliseFamInst ty
              ; case coi1 of

@@ -190,7 +183,7 @@ subFunTys error_herald n_pats res_ty thing_inside
                 -- Note argTypeKind: the args can have an unboxed type,
                 -- but not an unboxed tuple.
 
                 -- Note argTypeKind: the args can have an unboxed type,
                 -- but not an unboxed tuple.
 

-    loop n args_so_far res_ty = bale_out args_so_far
+    loop _ args_so_far _ = bale_out args_so_far

 
          -- Build a template type a1 -> ... -> an -> b and defer an equality
          -- between that template and the expected result type res_ty; then,
 
          -- Build a template type a1 -> ... -> an -> b and defer an equality
          -- between that template and the expected result type res_ty; then,

@@ -322,7 +315,7 @@ boxySplitAppTy orig_ty
       = do { (coi1, ty') <- tcNormaliseFamInst ty
            ; case coi1 of
                IdCo   -> defer    -- no progress, but maybe solvable => defer
       = do { (coi1, ty') <- tcNormaliseFamInst ty
            ; case coi1 of
                IdCo   -> defer    -- no progress, but maybe solvable => defer

-               ACo co ->          -- progress: so lets try again
+               ACo _ ->          -- progress: so lets try again

                  do { (args, coi2) <- loop ty'
                     ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
                     }
                  do { (args, coi2) <- loop ty'
                     ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
                     }

@@ -364,6 +357,7 @@ boxySplitAppTy orig_ty
     mk_res_ty _other             = panic "TcUnify.mk_res_ty2"
 
 ------------------
     mk_res_ty _other             = panic "TcUnify.mk_res_ty2"
 
 ------------------

+boxySplitFailure :: TcType -> TcType -> TcM (a, CoercionI)

 boxySplitFailure actual_ty expected_ty = failWithMisMatch actual_ty expected_ty
 
 ------------------
 boxySplitFailure actual_ty expected_ty = failWithMisMatch actual_ty expected_ty
 
 ------------------

@@ -479,7 +473,7 @@ boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
         | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
         | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
 
         | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
         | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
 

-    go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst      -- Rule S-ANY; no bindings
+    go _ (TyVarTy _) _ _ = emptyTvSubst      -- Rule S-ANY; no bindings

         -- Rule S-ANY covers (a) type variables and (b) boxy types
         -- in the template.  Both look like a TyVarTy.
         -- See Note [Sub-match] below
         -- Rule S-ANY covers (a) type variables and (b) boxy types
         -- in the template.  Both look like a TyVarTy.
         -- See Note [Sub-match] below

@@ -552,12 +546,14 @@ boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
     boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
         -- ToDo: add error context?
 
     boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
         -- ToDo: add error context?
 

-boxy_match_s tmpl_tvs [] boxy_tvs [] subst
+boxy_match_s :: TcTyVarSet -> [TcType] -> TcTyVarSet -> [BoxySigmaType]
+             -> TvSubst -> TvSubst
+boxy_match_s _ [] _ [] subst

   = subst
 boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
   = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
     boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
   = subst
 boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
   = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
     boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst

-boxy_match_s tmpl_tvs _ boxy_tvs _ subst
+boxy_match_s _ _ _ _ _

   = panic "boxy_match_s"        -- Lengths do not match
 
 
   = panic "boxy_match_s"        -- Lengths do not match
 
 

@@ -614,7 +610,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
                         Nothing -> orig_boxy_ty
                         Just ty -> ty `boxyLub` orig_boxy_ty
 
                         Nothing -> orig_boxy_ty
                         Just ty -> ty `boxyLub` orig_boxy_ty
 

-    go _ (TyVarTy tv) | isMetaTyVar tv
+    go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
+                               -- NB: A TyVar (not TcTyVar) is possible here, representing
+                               --     a skolem, because in this pure boxy_match function 
+                               --     we don't instantiate foralls to TcTyVars; cf Trac #2714

         = subst         -- Don't fail if the template has more info than the target!
                         -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
                         -- would fail to instantiate 'a', because the meta-type-variable
         = subst         -- Don't fail if the template has more info than the target!
                         -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
                         -- would fail to instantiate 'a', because the meta-type-variable

@@ -644,11 +643,11 @@ boxyLub orig_ty1 orig_ty2
       | tc1 == tc2, length ts1 == length ts2
       = TyConApp tc1 (zipWith boxyLub ts1 ts2)
 
       | tc1 == tc2, length ts1 == length ts2
       = TyConApp tc1 (zipWith boxyLub ts1 ts2)
 

-    go (TyVarTy tv1) ty2                -- This is the whole point;
+    go (TyVarTy tv1) _                  -- This is the whole point;

       | isTcTyVar tv1, isBoxyTyVar tv1  -- choose ty2 if ty2 is a box
       = orig_ty2
 
       | isTcTyVar tv1, isBoxyTyVar tv1  -- choose ty2 if ty2 is a box
       = orig_ty2
 

-    go ty1 (TyVarTy tv2)                -- Symmetrical case
+    go _ (TyVarTy tv2)                -- Symmetrical case

       | isTcTyVar tv2, isBoxyTyVar tv2
       = orig_ty1
 
       | isTcTyVar tv2, isBoxyTyVar tv2
       = orig_ty1
 

@@ -657,7 +656,7 @@ boxyLub orig_ty1 orig_ty2
                | Just ty2' <- tcView ty1 = go ty1 ty2'
 
     -- For now, we don't look inside ForAlls, PredTys
                | Just ty2' <- tcView ty1 = go ty1 ty2'
 
     -- For now, we don't look inside ForAlls, PredTys

-    go ty1 ty2 = orig_ty1       -- Default
+    go _ _ = orig_ty1       -- Default

 \end{code}
 
 Note [Matching kinds]
 \end{code}
 
 Note [Matching kinds]

@@ -735,6 +734,8 @@ tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty
         -- This indirection is just here to make
         -- it easy to insert a debug trace!
 
         -- This indirection is just here to make
         -- it easy to insert a debug trace!
 

+tc_sub1 :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> InBox
+        -> BoxySigmaType -> Type -> TcM HsWrapper

 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
   | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty'
 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
   | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty'
 tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty

@@ -771,7 +772,7 @@ tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
     if exp_ib then      -- SKOL does not apply if exp_ty is inside a box
         defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
     else do
     if exp_ib then      -- SKOL does not apply if exp_ty is inside a box
         defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
     else do

-        { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
+        { (gen_fn, co_fn) <- tcGen exp_ty act_tvs Nothing $ \ _ body_exp_ty ->

                              tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
         ; return (gen_fn <.> co_fn) }
     }
                              tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
         ; return (gen_fn <.> co_fn) }
     }

@@ -786,7 +787,7 @@ tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
 --      expected_ty: Int -> Int
 --      co_fn e =    e Int dOrdInt
 
 --      expected_ty: Int -> Int
 --      co_fn e =    e Int dOrdInt
 

-tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 orig _ actual_ty exp_ib exp_sty expected_ty

 -- Implements the new SPEC rule in the Appendix of the paper
 -- "Boxy types: inference for higher rank types and impredicativity"
 -- (This appendix isn't in the published version.)
 -- Implements the new SPEC rule in the Appendix of the paper
 -- "Boxy types: inference for higher rank types and impredicativity"
 -- (This appendix isn't in the published version.)

@@ -821,7 +822,7 @@ tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
 
 -----------------------------------
 -- Function case (rule F1)
 
 -----------------------------------
 -- Function case (rule F1)

-tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
+tc_sub1 orig _ (FunTy act_arg act_res) exp_ib _ (FunTy exp_arg exp_res)

   = do { traceTc (text "tc_sub1 - case 4")
        ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
        }
   = do { traceTc (text "tc_sub1 - case 4")
        ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
        }

@@ -837,7 +838,7 @@ tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
                         ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } }
  where
     mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
                         ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } }
  where
     mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'

-    mk_res_ty other = panic "TcUnify.mk_res_ty3"
+    mk_res_ty _ = panic "TcUnify.mk_res_ty3"

     fun_kinds = [argTypeKind, openTypeKind]
 
 -- Everything else: defer to boxy matching
     fun_kinds = [argTypeKind, openTypeKind]
 
 -- Everything else: defer to boxy matching

@@ -852,6 +853,8 @@ tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
        }
 
 -----------------------------------
        }
 
 -----------------------------------

+defer_to_boxy_matching :: InstOrigin -> TcType -> TcType -> InBox
+                       -> TcType -> TcType -> TcM HsWrapper

 defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
   = do  { coi <- addSubCtxt orig act_sty exp_sty $
                  u_tys (Unify True act_sty exp_sty)
 defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
   = do  { coi <- addSubCtxt orig act_sty exp_sty $
                  u_tys (Unify True act_sty exp_sty)

@@ -859,6 +862,8 @@ defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
         ; return $ coiToHsWrapper coi }
 
 -----------------------------------
         ; return $ coiToHsWrapper coi }
 
 -----------------------------------

+tc_sub_funs :: InstOrigin -> TcType -> BoxySigmaType -> InBox
+            -> TcType -> BoxySigmaType -> TcM HsWrapper

 tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
   = do  { arg_coi   <- addSubCtxt orig act_arg exp_arg $
                        uTysOuter False act_arg exp_ib exp_arg
 tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
   = do  { arg_coi   <- addSubCtxt orig act_arg exp_arg $
                        uTysOuter False act_arg exp_ib exp_arg

@@ -893,26 +898,21 @@ wrapFunResCoercion arg_tys co_fn_res
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-tcGen :: BoxySigmaType                          -- expected_ty
-      -> TcTyVarSet                             -- Extra tyvars that the universally
-                                                --      quantified tyvars of expected_ty
-                                                --      must not be unified
+tcGen :: BoxySigmaType                -- expected_ty
+      -> TcTyVarSet                   -- Extra tyvars that the universally
+                                      --      quantified tyvars of expected_ty
+                                      --      must not be unified
+      -> Maybe UserTypeCtxt          -- Just ctxt => this polytype arose directly
+                                     --                from a user type sig
+                                     -- Nothing => a higher order situation

       -> ([TcTyVar] -> BoxyRhoType -> TcM result)
       -> TcM (HsWrapper, result)
         -- The expression has type: spec_ty -> expected_ty
 
       -> ([TcTyVar] -> BoxyRhoType -> TcM result)
       -> TcM (HsWrapper, result)
         -- The expression has type: spec_ty -> expected_ty
 

-tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a forall-type
-                                                -- If not, the call is a no-op
+tcGen expected_ty extra_tvs mb_ctxt thing_inside        -- We expect expected_ty to be a forall-type
+                                                       -- If not, the call is a no-op

   = do  { traceTc (text "tcGen")
   = do  { traceTc (text "tcGen")

-                -- We want the GenSkol info in the skolemised type variables to
-                -- 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
-        ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
-                do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
-                        -- 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) })
+        ; ((tvs', theta', rho'), skol_info) <- instantiate expected_ty

 
         ; when debugIsOn $
               traceTc (text "tcGen" <+> vcat [
 
         ; when debugIsOn $
               traceTc (text "tcGen" <+> vcat [

@@ -923,7 +923,8 @@ tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a
                            text "free_tvs" <+> ppr free_tvs])
 
         -- Type-check the arg and unify with poly type
                            text "free_tvs" <+> ppr free_tvs])
 
         -- Type-check the arg and unify with poly type

-        ; (result, lie) <- getLIE (thing_inside tvs' rho')
+        ; (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
 
         -- Check that the "forall_tvs" havn't been constrained
         -- The interesting bit here is that we must include the free variables

@@ -950,6 +951,23 @@ tcGen expected_ty extra_tvs thing_inside        -- We expect expected_ty to be a
         ; return (co_fn, result) }
   where
     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
         ; return (co_fn, result) }
   where
     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs

+
+    instantiate :: TcType -> TcM (([TcTyVar],ThetaType,TcRhoType), SkolemInfo)
+    instantiate expected_ty
+      | Just ctxt <- mb_ctxt   -- This case split is the wohle reason for mb_ctxt
+      = do { let skol_info = SigSkol ctxt
+           ; stuff <- tcInstSigType True skol_info expected_ty
+          ; return (stuff, skol_info) }
+
+      | otherwise   -- We want the GenSkol info in the skolemised type variables to
+                    -- 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
+      = fixM $ \ ~(_, skol_info) ->
+        do { stuff@(forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
+                -- Get loation from *monad*, not from expected_ty
+           ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
+           ; return (stuff, skol_info) }

 \end{code}
 
 
 \end{code}
 
 

@@ -995,7 +1013,7 @@ unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
 unifyTheta theta1 theta2
   = do  { checkTc (equalLength theta1 theta2)
                   (vcat [ptext (sLit "Contexts differ in length"),
 unifyTheta theta1 theta2
   = do  { checkTc (equalLength theta1 theta2)
                   (vcat [ptext (sLit "Contexts differ in length"),

-                         nest 2 $ parens $ ptext (sLit "Use -fglasgow-exts to allow this")])
+                         nest 2 $ parens $ ptext (sLit "Use -XRelaxedPolyRec to allow this")])

         ; uList unifyPred theta1 theta2
         }
 
         ; uList unifyPred theta1 theta2
         }
 

@@ -1005,12 +1023,12 @@ uList :: (a -> a -> TcM b)
 -- Unify corresponding elements of two lists of types, which
 -- should be of equal length.  We charge down the list explicitly so that
 -- we can complain if their lengths differ.
 -- Unify corresponding elements of two lists of types, which
 -- should be of equal length.  We charge down the list explicitly so that
 -- we can complain if their lengths differ.

-uList unify []         []         = return []
+uList _     []         []         = return []

 uList unify (ty1:tys1) (ty2:tys2) = do { x  <- unify ty1 ty2;
                                        ; xs <- uList unify tys1 tys2
                                        ; return (x:xs)
                                        }
 uList unify (ty1:tys1) (ty2:tys2) = do { x  <- unify ty1 ty2;
                                        ; xs <- uList unify tys1 tys2
                                        ; return (x:xs)
                                        }

-uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!"
+uList _ _ _ = panic "Unify.uList: mismatched type lists!"

 \end{code}
 
 @unifyTypeList@ takes a single list of @TauType@s and unifies them
 \end{code}
 
 @unifyTypeList@ takes a single list of @TauType@s and unifies them

@@ -1020,7 +1038,7 @@ lists, when all the elts should be of the same type.
 \begin{code}
 unifyTypeList :: [TcTauType] -> TcM ()
 unifyTypeList []                 = return ()
 \begin{code}
 unifyTypeList :: [TcTauType] -> TcM ()
 unifyTypeList []                 = return ()

-unifyTypeList [ty]               = return ()
+unifyTypeList [_]                = return ()

 unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
                                       ; unifyTypeList tys }
 \end{code}
 unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
                                       ; unifyTypeList tys }
 \end{code}

@@ -1083,11 +1101,11 @@ uTys nb1 ty1 nb2 ty2
 uTys_s :: InBox -> [TcType]     -- tys1 are the *actual*   types
        -> InBox -> [TcType]     -- tys2 are the *expected* types
        -> TcM [CoercionI]
 uTys_s :: InBox -> [TcType]     -- tys1 are the *actual*   types
        -> InBox -> [TcType]     -- tys2 are the *expected* types
        -> TcM [CoercionI]

-uTys_s nb1 []         nb2 []         = return []
+uTys_s _   []         _   []         = return []

 uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
                                           ; cois <- uTys_s nb1 tys1 nb2 tys2
                                           ; return (coi:cois) }
 uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
                                           ; cois <- uTys_s nb1 tys1 nb2 tys2
                                           ; return (coi:cois) }

-uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!"
+uTys_s _ _ _ _ = panic "Unify.uTys_s: mismatched type lists!"

 
 --------------
 u_tys :: Outer
 
 --------------
 u_tys :: Outer

@@ -1121,13 +1139,13 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
     go :: Outer -> TcType -> TcType -> TcType -> TcType -> TcM CoercionI
         -- Always expand synonyms: see Note [Unification and synonyms]
         -- (this also throws away FTVs)
     go :: Outer -> TcType -> TcType -> TcType -> TcType -> TcM CoercionI
         -- Always expand synonyms: see Note [Unification and synonyms]
         -- (this also throws away FTVs)

-    go outer sty1 ty1 sty2 ty2
+    go _ sty1 ty1 sty2 ty2

       | Just ty1' <- tcView ty1 = go (Unify False ty1' ty2 ) sty1 ty1' sty2 ty2
       | Just ty2' <- tcView ty2 = go (Unify False ty1  ty2') sty1 ty1  sty2 ty2'
 
         -- Variables; go for uVar
       | Just ty1' <- tcView ty1 = go (Unify False ty1' ty2 ) sty1 ty1' sty2 ty2
       | Just ty2' <- tcView ty2 = go (Unify False ty1  ty2') sty1 ty1  sty2 ty2'
 
         -- Variables; go for uVar

-    go outer sty1 (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2
-    go outer sty1 ty1 sty2 (TyVarTy tyvar2) = uVar outer True  tyvar2 nb1 sty1 ty1
+    go outer _ (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2
+    go outer sty1 ty1 _ (TyVarTy tyvar2) = uVar outer True  tyvar2 nb1 sty1 ty1

                                 -- "True" means args swapped
 
         -- The case for sigma-types must *follow* the variable cases
                                 -- "True" means args swapped
 
         -- The case for sigma-types must *follow* the variable cases

@@ -1150,7 +1168,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
 
              ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
              { unless (equalLength theta1 theta2) (bale_out outer)
 
              ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
              { unless (equalLength theta1 theta2) (bale_out outer)

-             ; cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
+             ; _cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois

              ; traceTc (text "TOMDO!")
              ; coi <- uTys nb1 tau1 nb2 tau2
 
              ; traceTc (text "TOMDO!")
              ; coi <- uTys nb1 tau1 nb2 tau2
 

@@ -1176,13 +1194,13 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
     go outer _ (PredTy p1) _ (PredTy p2)
         = uPred outer nb1 p1 nb2 p2
 
     go outer _ (PredTy p1) _ (PredTy p2)
         = uPred outer nb1 p1 nb2 p2
 

-        -- Type constructors must match
+        -- Non-synonym type constructors must match

     go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
       | con1 == con2 && not (isOpenSynTyCon con1)
       = do { cois <- uTys_s nb1 tys1 nb2 tys2
            ; return $ mkTyConAppCoI con1 tys1 cois
            }
     go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
       | con1 == con2 && not (isOpenSynTyCon con1)
       = do { cois <- uTys_s nb1 tys1 nb2 tys2
            ; return $ mkTyConAppCoI con1 tys1 cois
            }

-        -- See Note [TyCon app]
+        -- Family synonyms See Note [TyCon app]

       | con1 == con2 && identicalOpenSynTyConApp
       = do { cois <- uTys_s nb1 tys1' nb2 tys2'
            ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
       | con1 == con2 && identicalOpenSynTyConApp
       = do { cois <- uTys_s nb1 tys1' nb2 tys2'
            ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)

@@ -1194,6 +1212,29 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
         identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
         -- See Note [OpenSynTyCon app]
 
         identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
         -- See Note [OpenSynTyCon app]
 

+        -- If we can reduce a family app => proceed with reduct
+        -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+        --     defer oversaturated applications!
+    go outer sty1 ty1@(TyConApp con1 _) sty2 ty2
+      | isOpenSynTyCon con1
+      = do { (coi1, ty1') <- tcNormaliseFamInst ty1
+           ; case coi1 of
+               IdCo -> defer    -- no reduction, see [Deferred Unification]
+               _    -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2
+           }
+
+        -- If we can reduce a family app => proceed with reduct
+        -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+        --     defer oversaturated applications!
+    go outer sty1 ty1 sty2 ty2@(TyConApp con2 _)
+      | isOpenSynTyCon con2
+      = do { (coi2, ty2') <- tcNormaliseFamInst ty2
+           ; case coi2 of
+               IdCo -> defer    -- no reduction, see [Deferred Unification]
+               _    -> liftM (`mkTransCoI` mkSymCoI coi2) $ 
+                         go outer sty1 ty1 sty2 ty2'
+           }
+

         -- Functions; just check the two parts
     go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
       = do { coi_l <- uTys nb1 fun1 nb2 fun2
         -- Functions; just check the two parts
     go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
       = do { coi_l <- uTys nb1 fun1 nb2 fun2

@@ -1219,56 +1260,35 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
            ; coi_t <- uTys nb1 t1 nb2 t2
            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
 
            ; coi_t <- uTys nb1 t1 nb2 t2
            ; return $ mkAppTyCoI s1 coi_s t1 coi_t }
 

-        -- One or both outermost constructors are type family applications.
-        -- If we can normalise them away, proceed as usual; otherwise, we
-        -- need to defer unification by generating a wanted equality constraint.
-    go outer sty1 ty1 sty2 ty2
-      | ty1_is_fun || ty2_is_fun
-      = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1
-                                           else return (IdCo, ty1)
-           ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2
-                                           else return (IdCo, ty2)
-           ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
-                    then do { -- One type family app can't be reduced yet
-                              -- => defer
-                            ; ty1'' <- zonkTcType ty1'
-                            ; ty2'' <- zonkTcType ty2'
-                            ; if tcEqType ty1'' ty2''
-                              then return IdCo
-                              else -- see [Deferred Unification]
-                                defer_unification outer False orig_ty1 orig_ty2
-                            }
-                     else -- unification can proceed
-                          go outer sty1 ty1' sty2 ty2'
-           ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
-           }
-        where
-          ty1_is_fun = isOpenSynTyConApp ty1
-          ty2_is_fun = isOpenSynTyConApp ty2
-

         -- Anything else fails
     go outer _ _ _ _ = bale_out outer
 
         -- Anything else fails
     go outer _ _ _ _ = bale_out outer
 

+    defer = defer_unification outer False orig_ty1 orig_ty2
+
+

 ----------
 ----------

-uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
+uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
+uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)

   | n1 == n2 =
         do { coi <- uTys nb1 t1 nb2 t2
            ; return $ mkIParamPredCoI n1 coi
            }
   | n1 == n2 =
         do { coi <- uTys nb1 t1 nb2 t2
            ; return $ mkIParamPredCoI n1 coi
            }

-uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
+uPred _ nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)

   | c1 == c2 =
         do { cois <- uTys_s nb1 tys1 nb2 tys2           -- Guaranteed equal lengths because the kinds check
            ; return $ mkClassPPredCoI c1 tys1 cois
            }
   | c1 == c2 =
         do { cois <- uTys_s nb1 tys1 nb2 tys2           -- Guaranteed equal lengths because the kinds check
            ; return $ mkClassPPredCoI c1 tys1 cois
            }

-uPred outer _ p1 _ p2 = unifyMisMatch outer
+uPred outer _ _ _ _ = unifyMisMatch outer

 
 

-uPreds outer nb1 []       nb2 []       = return []
+uPreds :: Outer -> InBox -> [PredType] -> InBox -> [PredType]
+       -> TcM [CoercionI]
+uPreds _     _   []       _   []       = return []

 uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
         do { coi  <- uPred  outer nb1 p1 nb2 p2
            ; cois <- uPreds outer nb1 ps1 nb2 ps2
            ; return (coi:cois)
            }
 uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
         do { coi  <- uPred  outer nb1 p1 nb2 p2
            ; cois <- uPreds outer nb1 ps1 nb2 ps2
            ; return (coi:cois)
            }

-uPreds outer nb1 ps1 nb2 ps2  = panic "uPreds"
+uPreds _ _ _ _ _ = panic "uPreds"

 \end{code}
 
 Note [TyCon app]
 \end{code}
 
 Note [TyCon app]

@@ -1276,8 +1296,8 @@ Note [TyCon app]
 When we find two TyConApps, the argument lists are guaranteed equal
 length.  Reason: intially the kinds of the two types to be unified is
 the same. The only way it can become not the same is when unifying two
 When we find two TyConApps, the argument lists are guaranteed equal
 length.  Reason: intially the kinds of the two types to be unified is
 the same. The only way it can become not the same is when unifying two

-AppTys (f1 a1):=:(f2 a2).  In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app).  If we unify f1:=:f2 first,
+AppTys (f1 a1)~(f2 a2).  In that case there can't be a TyConApp in
+the f1,f2 (because it'd absorb the app).  If we unify f1~f2 first,

 which we do, that ensures that f1,f2 have the same kind; and that
 means a1,a2 have the same kind.  And now the argument repeats.
 
 which we do, that ensures that f1,f2 have the same kind; and that
 means a1,a2 have the same kind.  And now the argument repeats.
 

@@ -1389,14 +1409,14 @@ uUnfilledVar :: Outer
              -> TcM CoercionI
 -- Invariant: tyvar 1 is not unified with anything
 
              -> TcM CoercionI
 -- Invariant: tyvar 1 is not unified with anything
 

-uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
+uUnfilledVar _ swapped tv1 details1 ps_ty2 ty2

   | Just ty2' <- tcView ty2
   =     -- Expand synonyms; ignore FTVs
     let outer' | swapped   = Unify False ty2' (mkTyVarTy tv1)
                | otherwise = Unify False (mkTyVarTy tv1) ty2'
     in uUnfilledVar outer' swapped tv1 details1 ps_ty2 ty2'
 
   | Just ty2' <- tcView ty2
   =     -- Expand synonyms; ignore FTVs
     let outer' | swapped   = Unify False ty2' (mkTyVarTy tv1)
                | otherwise = Unify False (mkTyVarTy tv1) ty2'
     in uUnfilledVar outer' swapped tv1 details1 ps_ty2 ty2'
 

-uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2)
+uUnfilledVar outer swapped tv1 details1 _ (TyVarTy tv2)

   | tv1 == tv2  -- Same type variable => no-op (but watch out for the boxy case)
   = case details1 of
         MetaTv BoxTv ref1  -- A boxy type variable meets itself;
   | tv1 == tv2  -- Same type variable => no-op (but watch out for the boxy case)
   = case details1 of
         MetaTv BoxTv ref1  -- A boxy type variable meets itself;

@@ -1405,7 +1425,7 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2)
                     ; updateMeta tv1 ref1 (mkTyVarTy tau_tv)
                     ; return IdCo
                     }
                     ; updateMeta tv1 ref1 (mkTyVarTy tau_tv)
                     ; return IdCo
                     }

-        other -> return IdCo    -- No-op
+        _ -> return IdCo    -- No-op

 
   | otherwise  -- Distinct type variables
   = do  { lookup2 <- lookupTcTyVar tv2
 
   | otherwise  -- Distinct type variables
   = do  { lookup2 <- lookupTcTyVar tv2

@@ -1503,7 +1523,7 @@ uMetaVar :: Outer
 -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
 -- ty2 is not a type variable
 
 -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
 -- ty2 is not a type variable
 

-uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
+uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 ty2

   =     -- tv1 is a BoxTv.  So we must unbox ty2, to ensure
         -- that any boxes in ty2 are filled with monotypes
         --
   =     -- tv1 is a BoxTv.  So we must unbox ty2, to ensure
         -- that any boxes in ty2 are filled with monotypes
         --

@@ -1512,18 +1532,24 @@ uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
         -- it does, the unbox operation will fill it, and the debug code
         -- checks for that.
     do { final_ty <- unBox ps_ty2
         -- it does, the unbox operation will fill it, and the debug code
         -- checks for that.
     do { final_ty <- unBox ps_ty2

-       ; when debugIsOn $ do
-           { meta_details <- readMutVar ref1
-           ; case meta_details of
-                 Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
-                                return () -- This really should *not* happen
-                 Flexi -> return ()
-           }
-        ; checkUpdateMeta swapped tv1 ref1 final_ty
-        ; return IdCo
+       ; meta_details <- readMutVar ref1
+       ; case meta_details of
+                 Indirect _ ->   -- This *can* happen due to an occurs check,
+                           -- just as it can in checkTauTvUpdate in the next
+                           -- equation of uMetaVar; see Trac #2414
+                           -- Note [Occurs check]
+                       -- Go round again.  Probably there's an immediate
+                       -- error, but maybe not (a type function might discard
+                       -- its argument).  Next time round we'll end up in the
+                       -- TauTv case of uMetaVar.
+                  uVar outer swapped tv1 False ps_ty2 ty2
+                       -- Setting for nb2::InBox is irrelevant
+
+                 Flexi -> do { checkUpdateMeta swapped tv1 ref1 final_ty
+                       ; return IdCo }

         }
 
         }
 

-uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2
+uMetaVar outer swapped tv1 _ ref1 ps_ty2 _

   = do  { -- Occurs check + monotype check
         ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2
         ; case mb_final_ty of
   = do  { -- Occurs check + monotype check
         ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2
         ; case mb_final_ty of

@@ -1535,6 +1561,18 @@ uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2
                  }
         }
 
                  }
         }
 

+{- Note [Occurs check]
+   ~~~~~~~~~~~~~~~~~~~
+An eager occurs check is made in checkTauTvUpdate, deferring tricky
+cases by calling defer_unification (see notes with
+checkTauTvUpdate). An occurs check can also (and does) happen in the
+BoxTv case, but unBox doesn't check for occurrences, and in any case
+doesn't have the type-function-related complexity that
+checkTauTvUpdate has.  So we content ourselves with spotting the potential
+occur check (by the fact that tv1 is now filled), and going round again.
+Next time round we'll get the TauTv case of uMetaVar.
+-}
+

 ----------------
 uUnfilledVars :: Outer
               -> SwapFlag
 ----------------
 uUnfilledVars :: Outer
               -> SwapFlag

@@ -1549,13 +1587,13 @@ uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _)
   = -- see [Deferred Unification]
     defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
 
   = -- see [Deferred Unification]
     defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
 

-uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _)
+uUnfilledVars _ swapped tv1 (MetaTv _ ref1) tv2 (SkolemTv _)

   = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo
   = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo

-uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2)
+uUnfilledVars _ swapped tv1 (SkolemTv _) tv2 (MetaTv _ ref2)

   = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo
 
 -- ToDo: this function seems too long for what it acutally does!
   = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo
 
 -- ToDo: this function seems too long for what it acutally does!

-uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
+uUnfilledVars _ swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)

   = case (info1, info2) of
         (BoxTv,   BoxTv)   -> box_meets_box >> return IdCo
 
   = case (info1, info2) of
         (BoxTv,   BoxTv)   -> box_meets_box >> return IdCo
 

@@ -1626,7 +1664,7 @@ 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 :: 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)
+refineBoxToTau (TyVarTy box_tv)

   | isMetaTyVar box_tv
   , MetaTv BoxTv ref <- tcTyVarDetails box_tv
   = do  { cts <- readMutVar ref
   | isMetaTyVar box_tv
   , MetaTv BoxTv ref <- tcTyVarDetails box_tv
   = do  { cts <- readMutVar ref

@@ -1679,6 +1717,7 @@ unBox (TyVarTy tv)
   | otherwise   -- Skolems, and meta-tau-variables
   = return (TyVarTy tv)
 
   | otherwise   -- Skolems, and meta-tau-variables
   = return (TyVarTy tv)
 

+unBoxPred :: PredType -> TcM PredType

 unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') }
 unBoxPred (IParam ip ty)   = do { ty' <- unBox ty; return (IParam ip ty') }
 unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') }
 unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') }
 unBoxPred (IParam ip ty)   = do { ty' <- unBox ty; return (IParam ip ty') }
 unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') }

@@ -1703,6 +1742,7 @@ popUnifyCtxt (Unify True  _ _) thing = popErrCtxt thing
 popUnifyCtxt (Unify False _ _) thing = thing
 
 -----------------------
 popUnifyCtxt (Unify False _ _) thing = thing
 
 -----------------------

+unifyCtxt :: TcType -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)

 unifyCtxt act_ty exp_ty tidy_env
   = do  { act_ty' <- zonkTcType act_ty
         ; exp_ty' <- zonkTcType exp_ty
 unifyCtxt act_ty exp_ty tidy_env
   = do  { act_ty' <- zonkTcType act_ty
         ; exp_ty' <- zonkTcType exp_ty

@@ -1711,6 +1751,7 @@ unifyCtxt act_ty exp_ty tidy_env
         ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
 
 ----------------
         ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
 
 ----------------

+mkExpectedActualMsg :: Type -> Type -> SDoc

 mkExpectedActualMsg act_ty exp_ty
   = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
                    text "Inferred type" <> colon <+> ppr act_ty ])
 mkExpectedActualMsg act_ty exp_ty
   = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
                    text "Inferred type" <> colon <+> ppr act_ty ])

@@ -1718,6 +1759,7 @@ mkExpectedActualMsg act_ty exp_ty
 ----------------
 -- If an error happens we try to figure out whether the function
 -- function has been given too many or too few arguments, and say so.
 ----------------
 -- If an error happens we try to figure out whether the function
 -- function has been given too many or too few arguments, and say so.

+addSubCtxt :: InstOrigin -> TcType -> TcType -> TcM a -> TcM a

 addSubCtxt orig actual_res_ty expected_res_ty thing_inside
   = addErrCtxtM mk_err thing_inside
   where
 addSubCtxt orig actual_res_ty expected_res_ty thing_inside
   = addErrCtxtM mk_err thing_inside
   where

@@ -1736,7 +1778,7 @@ addSubCtxt orig actual_res_ty expected_res_ty thing_inside
                              OccurrenceOf fun
                                   | len_exp_args < len_act_args -> wrongArgsCtxt "too few"  fun
                                   | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
                              OccurrenceOf fun
                                   | len_exp_args < len_act_args -> wrongArgsCtxt "too few"  fun
                                   | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun

-                             other -> mkExpectedActualMsg act_ty'' exp_ty''
+                             _ -> mkExpectedActualMsg act_ty'' exp_ty''

            ; return (env2, message) }
 
     wrongArgsCtxt too_many_or_few fun
            ; return (env2, message) }
 
     wrongArgsCtxt too_many_or_few fun

@@ -1745,6 +1787,7 @@ addSubCtxt orig actual_res_ty expected_res_ty thing_inside
         <+> ptext (sLit "arguments")
 
 ------------------
         <+> ptext (sLit "arguments")
 
 ------------------

+unifyForAllCtxt :: [TyVar] -> Type -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)

 unifyForAllCtxt tvs phi1 phi2 env
   = return (env2, msg)
   where
 unifyForAllCtxt tvs phi1 phi2 env
   = return (env2, msg)
   where

@@ -1817,18 +1860,19 @@ uUnboundKVar swapped kv1 non_var_k2
         ; writeKindVar kv1 k2'' }
 
 ----------------
         ; writeKindVar kv1 k2'' }
 
 ----------------

+kindOccurCheck :: TyVar -> Type -> TcM ()

 kindOccurCheck kv1 k2   -- k2 is zonked
   = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
   where
 kindOccurCheck kv1 k2   -- k2 is zonked
   = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
   where

-    not_in (TyVarTy kv2)   = kv1 /= kv2
+    not_in (TyVarTy kv2) = kv1 /= kv2

     not_in (FunTy a2 r2) = not_in a2 && not_in r2
     not_in (FunTy a2 r2) = not_in a2 && not_in r2

-    not_in other         = True
+    not_in _             = True

 
 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
 -- If the flag is False, it requires k <: sk
 -- E.g.         kindSimpleKind False ?? = *
 
 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
 -- If the flag is False, it requires k <: sk
 -- E.g.         kindSimpleKind False ?? = *

--- What about (kv -> *) :=: ?? -> *
+-- What about (kv -> *) ~ ?? -> *

 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where
 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where

@@ -1838,11 +1882,11 @@ kindSimpleKind orig_swapped orig_kind
     go True k
      | isOpenTypeKind k = return liftedTypeKind
      | isArgTypeKind k  = return liftedTypeKind
     go True k
      | isOpenTypeKind k = return liftedTypeKind
      | isArgTypeKind k  = return liftedTypeKind

-    go sw k
+    go _ k

      | isLiftedTypeKind k   = return liftedTypeKind
      | isUnliftedTypeKind k = return unliftedTypeKind
      | isLiftedTypeKind k   = return liftedTypeKind
      | isUnliftedTypeKind k = return unliftedTypeKind

-    go sw k@(TyVarTy _)   = return k    -- KindVars are always simple
-    go swapped kind = failWithTc (ptext (sLit "Unexpected kind unification failure:")
+    go _ k@(TyVarTy _) = return k -- KindVars are always simple
+    go _ _ = failWithTc (ptext (sLit "Unexpected kind unification failure:")

                                   <+> ppr orig_swapped <+> ppr orig_kind)
         -- I think this can't actually happen
 
                                   <+> ppr orig_swapped <+> ppr orig_kind)
         -- I think this can't actually happen
 

@@ -1850,6 +1894,7 @@ kindSimpleKind orig_swapped orig_kind
 -- T v w = MkT (v -> w)  v must not be an umboxed tuple
 
 ----------------
 -- T v w = MkT (v -> w)  v must not be an umboxed tuple
 
 ----------------

+kindOccurCheckErr :: Var -> Type -> SDoc

 kindOccurCheckErr tyvar ty
   = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
        2 (sep [ppr tyvar, char '=', ppr ty])
 kindOccurCheckErr tyvar ty
   = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
        2 (sep [ppr tyvar, char '=', ppr ty])

@@ -1870,76 +1915,7 @@ unifyFunKind (TyVarTy kvar) = do
              ; return (Just (arg_kind,res_kind)) }
 
 unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
              ; return (Just (arg_kind,res_kind)) }
 
 unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))

-unifyFunKind other                     = return Nothing
-\end{code}
-
-%************************************************************************
-%*                                                                      *
-        Checking kinds
-%*                                                                      *
-%************************************************************************
-
----------------------------
--- We would like to get a decent error message from
---   (a) Under-applied type constructors
---              f :: (Maybe, Maybe)
---   (b) Over-applied type constructors
---              f :: Int x -> Int x
---
-
-\begin{code}
-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
-  = return ()
-  | otherwise = do
-    (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
-    case mb_r of
-        Just r  -> return () ;  -- Unification succeeded
-        Nothing -> do
-
-        -- So there's definitely an error
-        -- Now to find out what sort
-           exp_kind <- zonkTcKind exp_kind
-           act_kind <- zonkTcKind act_kind
-
-           env0 <- tcInitTidyEnv
-           let (exp_as, _) = splitKindFunTys exp_kind
-               (act_as, _) = splitKindFunTys act_kind
-               n_exp_as = length exp_as
-               n_act_as = length act_as
-
-               (env1, tidy_exp_kind) = tidyKind env0 exp_kind
-               (env2, tidy_act_kind) = tidyKind env1 act_kind
-
-               err | n_exp_as < n_act_as     -- E.g. [Maybe]
-                   = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
-
-                     -- Now n_exp_as >= n_act_as. In the next two cases,
-                     -- n_exp_as == 0, and hence so is n_act_as
-                   | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
-                   = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
-                       <+> ptext (sLit "is unlifted")
-
-                   | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
-                   = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
-                       <+> ptext (sLit "is lifted")
-
-                   | otherwise               -- E.g. Monad [Int]
-                   = ptext (sLit "Kind mis-match")
-
-               more_info = sep [ ptext (sLit "Expected kind") <+>
-                                     quotes (pprKind tidy_exp_kind) <> comma,
-                                 ptext (sLit "but") <+> quotes (ppr ty) <+>
-                                     ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
-
-           failWithTcM (env2, err $$ more_info)
+unifyFunKind _                         = return Nothing

 \end{code}
 
 %************************************************************************
 \end{code}
 
 %************************************************************************

@@ -1992,10 +1968,10 @@ check_sig_tyvars
         -> [TcTyVar]    -- Universally-quantified type variables in the signature
                         --      Guaranteed to be skolems
         -> TcM ()
         -> [TcTyVar]    -- Universally-quantified type variables in the signature
                         --      Guaranteed to be skolems
         -> TcM ()

-check_sig_tyvars extra_tvs []
+check_sig_tyvars _ []

   = return ()
 check_sig_tyvars extra_tvs sig_tvs
   = return ()
 check_sig_tyvars extra_tvs sig_tvs

-  = ASSERT( all isSkolemTyVar sig_tvs )
+  = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs )

     do  { gbl_tvs <- tcGetGlobalTyVars
         ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
                                       text "gbl_tvs" <+> ppr gbl_tvs,
     do  { gbl_tvs <- tcGetGlobalTyVars
         ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
                                       text "gbl_tvs" <+> ppr gbl_tvs,

@@ -2031,6 +2007,7 @@ bleatEscapedTvs globals sig_tvs zonked_tvs
            ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
 
 -----------------------
            ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
 
 -----------------------

+escape_msg :: Var -> Var -> [SDoc] -> SDoc

 escape_msg sig_tv zonked_tv globs
   | notNull globs
   = vcat [sep [msg, ptext (sLit "is mentioned in the environment:")],
 escape_msg sig_tv zonked_tv globs
   | notNull globs
   = vcat [sep [msg, ptext (sLit "is mentioned in the environment:")],