fix haddock submodule pointer
[ghc-hetmet.git] / compiler / typecheck / TcHsType.lhs
index 968ccfb..4fe6b60 100644 (file)
@@ -1,21 +1,23 @@
-
+%
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
 module TcHsType (
-       tcHsSigType, tcHsDeriv,
+       tcHsSigType, tcHsSigTypeNC, tcHsDeriv, 
+       tcHsInstHead, tcHsQuantifiedType,
        UserTypeCtxt(..), 
 
                -- Kind checking
        kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
-       kcCheckHsType, kcHsContext, kcHsType, 
+       kcLHsType, kcCheckLHsType, kcHsContext, 
        
                -- Typechecking kinded types
        tcHsKindedContext, tcHsKindedType, tcHsBangType,
-       tcTyVarBndrs, dsHsType, tcLHsConResTy,
-       tcDataKindSig,
+       tcTyVarBndrs, dsHsType, kcHsLPred, dsHsLPred,
+       tcDataKindSig, ExpKind(..), EkCtxt(..),
 
                -- Pattern type signatures
        tcHsPatSigType, tcPatSig
@@ -23,42 +25,33 @@ module TcHsType (
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, 
-                         LHsContext, HsPred(..), LHsPred, HsExplicitForAll(..) )
-import RnHsSyn         ( extractHsTyVars )
+#ifdef GHCI    /* Only if bootstrapped */
+import {-# SOURCE #-}  TcSplice( kcSpliceType )
+#endif
+
+import HsSyn
+import RnHsSyn
 import TcRnMonad
-import TcEnv           ( tcExtendTyVarEnv, tcExtendKindEnvTvs, 
-                         tcLookup, tcLookupClass, tcLookupTyCon,
-                         TyThing(..), getInLocalScope, getScopedTyVarBinds,
-                         wrongThingErr
-                       )
-import TcMType         ( newKindVar, 
-                         zonkTcKindToKind, 
-                         tcInstBoxyTyVar, readFilledBox,
-                         checkValidType
-                       )
-import TcUnify         ( boxyUnify, unifyFunKind, checkExpectedKind )
-import TcIface         ( checkWiredInTyCon )
-import TcType          ( Type, PredType(..), ThetaType, BoxySigmaType,
-                         TcType, TcKind, isRigidTy,
-                         UserTypeCtxt(..), pprUserTypeCtxt,
-                         substTyWith, mkTyVarTys, tcEqType,
-                         tcIsTyVarTy, mkFunTy, mkSigmaTy, mkPredTy, 
-                         mkTyConApp, mkAppTys, typeKind )
-import Kind            ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, 
-                         openTypeKind, argTypeKind, splitKindFunTys )
-import Var             ( TyVar, mkTyVar, tyVarName )
-import TyCon           ( TyCon, tyConKind )
-import Class           ( Class, classTyCon )
-import Name            ( Name, mkInternalName )
-import OccName         ( mkOccName, tvName )
+import TcEnv
+import TcMType
+import TcUnify
+import TcIface
+import TcType
+import TysPrim ( ecKind )
+import {- Kind parts of -} Type
+import Var
+import VarSet
+import TyCon
+import Class
+import Name
 import NameSet
-import PrelNames       ( genUnitTyConName )
-import TysWiredIn      ( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon )
-import BasicTypes      ( Boxity(..) )
-import SrcLoc          ( Located(..), unLoc, noLoc, getLoc, srcSpanStart )
-import UniqSupply      ( uniqsFromSupply )
+import TysWiredIn
+import BasicTypes
+import SrcLoc
+import Util
+import UniqSupply
 import Outputable
+import FastString
 \end{code}
 
 
@@ -145,26 +138,74 @@ the TyCon being defined.
 %************************************************************************
 
 \begin{code}
-tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
+tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
   -- Do kind checking, and hoist for-alls to the top
   -- NB: it's important that the foralls that come from the top-level
   --    HsForAllTy in hs_ty occur *first* in the returned type.
   --     See Note [Scoped] with TcSigInfo
 tcHsSigType ctxt hs_ty 
   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
-    do { kinded_ty <- kcTypeType hs_ty
+    tcHsSigTypeNC ctxt hs_ty
+
+tcHsSigTypeNC ctxt hs_ty
+  = do { (kinded_ty, _kind) <- kc_lhs_type hs_ty
+         -- The kind is checked by checkValidType, and isn't necessarily
+         -- of kind * in a Template Haskell quote eg [t| Maybe |]
        ; ty <- tcHsKindedType kinded_ty
        ; checkValidType ctxt ty        
-       ; returnM ty }
+       ; return ty }
+
+tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
+-- Typecheck an instance head.  We can't use 
+-- tcHsSigType, because it's not a valid user type.
+tcHsInstHead (L loc hs_ty)
+  = setSrcSpan loc   $ -- No need for an "In the type..." context
+                        -- because that comes from the caller
+    do { kinded_ty <- kc_inst_head hs_ty
+       ; ds_inst_head kinded_ty }
+  where
+    kc_inst_head ty@(HsPredTy pred@(HsClassP {}))
+      = do { (pred', kind) <- kc_pred pred
+           ; checkExpectedKind ty kind ekLifted
+           ; return (HsPredTy pred') }
+    kc_inst_head (HsForAllTy exp tv_names context (L loc ty))
+      = kcHsTyVars tv_names         $ \ tv_names' ->
+        do { ctxt' <- kcHsContext context
+           ; ty'   <- kc_inst_head ty
+           ; return (HsForAllTy exp tv_names' ctxt' (L loc ty')) }
+    kc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type"))
+
+    ds_inst_head (HsPredTy (HsClassP cls_name tys))
+      = do { clas <- tcLookupClass cls_name
+           ; arg_tys <- dsHsTypes tys
+           ; return ([], [], clas, arg_tys) }
+    ds_inst_head (HsForAllTy _ tvs ctxt (L _ tau))
+      = tcTyVarBndrs tvs  $ \ tvs' ->
+        do { ctxt' <- mapM dsHsLPred (unLoc ctxt)
+           ; (tvs_r, ctxt_r, cls, tys) <- ds_inst_head tau
+           ; return (tvs' ++ tvs_r, ctxt' ++ ctxt_r , cls, tys) }
+    ds_inst_head _ = panic "ds_inst_head"
+
+tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
+-- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
+-- except that we want to keep the tvs separate
+tcHsQuantifiedType tv_names hs_ty
+  = kcHsTyVars tv_names $ \ tv_names' ->
+    do { kc_ty <- kcHsSigType hs_ty
+       ; tcTyVarBndrs tv_names' $ \ tvs ->
+    do { ty <- dsHsType kc_ty
+       ; return (tvs, ty) } }
 
 -- Used for the deriving(...) items
-tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
-tcHsDeriv = addLocM (tc_hs_deriv [])
+tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
+tcHsDeriv = tc_hs_deriv []
 
+tc_hs_deriv :: [LHsTyVarBndr Name] -> HsType Name
+            -> TcM ([TyVar], Class, [Type])
 tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
   = kcHsTyVars tv_names                $ \ tv_names' ->
     do { cls_kind <- kcClass cls_name
-       ; (tys, res_kind) <- kcApps cls_kind (ppr cls_name) hs_tys
+       ; (tys, _res_kind) <- kcApps cls_name cls_kind hs_tys
        ; tcTyVarBndrs tv_names'        $ \ tyvars ->
     do { arg_tys <- dsHsTypes tys
        ; cls <- tcLookupClass cls_name
@@ -177,7 +218,7 @@ tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
     tc_hs_deriv (tv_names1 ++ tv_names2) ty
 
 tc_hs_deriv _ other
-  = failWithTc (ptext SLIT("Illegal deriving item") <+> ppr other)
+  = failWithTc (ptext (sLit "Illegal deriving item") <+> ppr other)
 \end{code}
 
        These functions are used during knot-tying in
@@ -187,12 +228,11 @@ tc_hs_deriv _ other
 \begin{code}
 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
        -- Used for type signatures
-kcHsSigType ty              = kcTypeType ty
-kcHsLiftedSigType ty = kcLiftedType ty
+kcHsSigType ty              = addKcTypeCtxt ty $ kcTypeType ty
+kcHsLiftedSigType ty = addKcTypeCtxt ty $ kcLiftedType ty
 
 tcHsKindedType :: LHsType Name -> TcM Type
-  -- Don't do kind checking, nor validity checking, 
-  --   but do hoist for-alls to the top
+  -- Don't do kind checking, nor validity checking.
   -- This is used in type and class decls, where kinding is
   -- done in advance, and validity checking is done later
   -- [Validity checking done later because of knot-tying issues.]
@@ -200,13 +240,13 @@ tcHsKindedType hs_ty = dsHsType hs_ty
 
 tcHsBangType :: LHsType Name -> TcM Type
 -- Permit a bang, but discard it
-tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
-tcHsBangType ty                      = tcHsKindedType ty
+tcHsBangType (L _ (HsBangTy _ ty)) = tcHsKindedType ty
+tcHsBangType ty                    = tcHsKindedType ty
 
 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
 -- Used when we are expecting a ClassContext (i.e. no implicit params)
 -- Does not do validity checking, like tcHsKindedType
-tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
+tcHsKindedContext hs_theta = addLocM (mapM dsHsLPred) hs_theta
 \end{code}
 
 
@@ -222,43 +262,83 @@ tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
 ---------------------------
 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
 -- The type ty must be a *lifted* *type*
-kcLiftedType ty = kcCheckHsType ty liftedTypeKind
+kcLiftedType ty = kc_check_lhs_type ty ekLifted
     
 ---------------------------
 kcTypeType :: LHsType Name -> TcM (LHsType Name)
 -- The type ty must be a *type*, but it can be lifted or 
 -- unlifted or an unboxed tuple.
-kcTypeType ty = kcCheckHsType ty openTypeKind
+kcTypeType ty = kc_check_lhs_type ty ekOpen
 
 ---------------------------
-kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
+kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)
+kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind
+
+
+kc_check_lhs_type :: LHsType Name -> ExpKind -> TcM (LHsType Name)
 -- Check that the type has the specified kind
 -- Be sure to use checkExpectedKind, rather than simply unifying 
 -- with OpenTypeKind, because it gives better error messages
-kcCheckHsType (L span ty) exp_kind 
-  = setSrcSpan span                            $
-    do { (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
+kc_check_lhs_type (L span ty) exp_kind 
+  = setSrcSpan span $
+    do { ty' <- kc_check_hs_type ty exp_kind
+       ; return (L span ty') }
+
+kc_check_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [LHsType Name]
+kc_check_lhs_types tys_w_kinds
+  = mapM kc_arg tys_w_kinds
+  where
+    kc_arg (arg, arg_kind) = kc_check_lhs_type arg arg_kind
+
+
+---------------------------
+kc_check_hs_type :: HsType Name -> ExpKind -> TcM (HsType Name)
+
+-- First some special cases for better error messages 
+-- when we know the expected kind
+kc_check_hs_type (HsParTy ty) exp_kind
+  = do { ty' <- kc_check_lhs_type ty exp_kind; return (HsParTy ty') }
+
+kc_check_hs_type ty@(HsAppTy ty1 ty2) exp_kind
+  = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
+       ; (fun_ty', fun_kind) <- kc_lhs_type fun_ty
+       ; arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
+       ; return (mkHsAppTys fun_ty' arg_tys') }
+
+-- This is the general case: infer the kind and compare
+kc_check_hs_type ty exp_kind
+  = do { (ty', act_kind) <- kc_hs_type ty
                -- Add the context round the inner check only
                -- because checkExpectedKind already mentions
                -- 'ty' by name in any error message
 
-       ; checkExpectedKind ty act_kind exp_kind
-       ; return (L span ty') }
+       ; checkExpectedKind (strip ty) act_kind exp_kind
+       ; return ty' }
   where
-       -- Wrap a context around only if we want to
-       -- show that contexts.  Omit invisble ones
-       -- and ones user's won't grok (HsPred p).
-    add_ctxt (HsPredTy p)                         thing = thing
-    add_ctxt (HsForAllTy Implicit tvs (L _ []) ty) thing = thing
-    add_ctxt other_ty thing = addErrCtxt (typeCtxt ty) thing
+       -- We infer the kind of the type, and then complain if it's
+       -- not right.  But we don't want to complain about
+       --      (ty) or !(ty) or forall a. ty
+       -- when the real difficulty is with the 'ty' part.
+    strip (HsParTy (L _ ty))          = strip ty
+    strip (HsBangTy _ (L _ ty))       = strip ty
+    strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
+    strip ty                         = ty
 \end{code}
 
        Here comes the main function
 
 \begin{code}
-kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
-kcHsType ty = wrapLocFstM kc_hs_type ty
--- kcHsType *returns* the kind of the type, rather than taking an expected
+kcLHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
+-- Called from outside: set the context
+kcLHsType ty = addKcTypeCtxt ty (kc_lhs_type ty)
+
+kc_lhs_type :: LHsType Name -> TcM (LHsType Name, TcKind)
+kc_lhs_type (L span ty)
+  = setSrcSpan span $
+    do { (ty', kind) <- kc_hs_type ty
+       ; return (L span ty', kind) }
+
+-- kc_hs_type *returns* the kind of the type, rather than taking an expected
 -- kind as argument as tcExpr does.  
 -- Reasons: 
 --     (a) the kind of (->) is
@@ -268,151 +348,189 @@ kcHsType ty = wrapLocFstM kc_hs_type ty
 --
 -- The translated type has explicitly-kinded type-variable binders
 
-kc_hs_type (HsParTy ty)
- = kcHsType ty         `thenM` \ (ty', kind) ->
-   returnM (HsParTy ty', kind)
-
-kc_hs_type (HsTyVar name)
-  = kcTyVar name       `thenM` \ kind ->
-    returnM (HsTyVar name, kind)
+kc_hs_type :: HsType Name -> TcM (HsType Name, TcKind)
+kc_hs_type (HsParTy ty) = do
+   (ty', kind) <- kc_lhs_type ty
+   return (HsParTy ty', kind)
+
+kc_hs_type (HsTyVar name) = do
+    kind <- kcTyVar name
+    return (HsTyVar name, kind)
+
+kc_hs_type (HsListTy ty) = do
+    ty' <- kcLiftedType ty
+    return (HsListTy ty', liftedTypeKind)
+
+kc_hs_type (HsPArrTy ty) = do
+    ty' <- kcLiftedType ty
+    return (HsPArrTy ty', liftedTypeKind)
+
+kc_hs_type (HsModalBoxType ecn ty) = do
+    kc_check_hs_type (HsTyVar ecn) (EK ecKind EkUnk)
+    ty' <- kcLiftedType ty
+    return (HsModalBoxType ecn ty', liftedTypeKind)
+
+kc_hs_type (HsKappaTy ty1 ty2) = do
+    ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)
+    ty2' <- kcTypeType ty2
+    return (HsKappaTy ty1' ty2', liftedTypeKind)
+
+kc_hs_type (HsKindSig ty k) = do
+    ty' <- kc_check_lhs_type ty (EK k EkKindSig)
+    return (HsKindSig ty' k, k)
+
+kc_hs_type (HsTupleTy Boxed tys) = do
+    tys' <- mapM kcLiftedType tys
+    return (HsTupleTy Boxed tys', liftedTypeKind)
+
+kc_hs_type (HsTupleTy Unboxed tys) = do
+    tys' <- mapM kcTypeType tys
+    return (HsTupleTy Unboxed tys', ubxTupleKind)
+
+kc_hs_type (HsFunTy ty1 ty2) = do
+    ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)
+    ty2' <- kcTypeType ty2
+    return (HsFunTy ty1' ty2', liftedTypeKind)
+
+kc_hs_type (HsOpTy ty1 op ty2) = do
+    op_kind <- addLocM kcTyVar op
+    ([ty1',ty2'], res_kind) <- kcApps op op_kind [ty1,ty2]
+    return (HsOpTy ty1' op ty2', res_kind)
+
+kc_hs_type (HsAppTy ty1 ty2) = do
+    let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
+    (fun_ty', fun_kind) <- kc_lhs_type fun_ty
+    (arg_tys', res_kind) <- kcApps fun_ty fun_kind arg_tys
+    return (mkHsAppTys fun_ty' arg_tys', res_kind)
 
-kc_hs_type (HsListTy ty) 
-  = kcLiftedType ty                    `thenM` \ ty' ->
-    returnM (HsListTy ty', liftedTypeKind)
-
-kc_hs_type (HsPArrTy ty)
-  = kcLiftedType ty                    `thenM` \ ty' ->
-    returnM (HsPArrTy ty', liftedTypeKind)
-
-kc_hs_type (HsNumTy n)
-   = returnM (HsNumTy n, liftedTypeKind)
-
-kc_hs_type (HsKindSig ty k) 
-  = kcCheckHsType ty k `thenM` \ ty' ->
-    returnM (HsKindSig ty' k, k)
-
-kc_hs_type (HsTupleTy Boxed tys)
-  = mappM kcLiftedType tys     `thenM` \ tys' ->
-    returnM (HsTupleTy Boxed tys', liftedTypeKind)
-
-kc_hs_type (HsTupleTy Unboxed tys)
-  = mappM kcTypeType tys       `thenM` \ tys' ->
-    returnM (HsTupleTy Unboxed tys', ubxTupleKind)
-
-kc_hs_type (HsFunTy ty1 ty2)
-  = kcCheckHsType ty1 argTypeKind      `thenM` \ ty1' ->
-    kcTypeType ty2                     `thenM` \ ty2' ->
-    returnM (HsFunTy ty1' ty2', liftedTypeKind)
-
-kc_hs_type ty@(HsOpTy ty1 op ty2)
-  = addLocM kcTyVar op                 `thenM` \ op_kind ->
-    kcApps op_kind (ppr op) [ty1,ty2]  `thenM` \ ([ty1',ty2'], res_kind) ->
-    returnM (HsOpTy ty1' op ty2', res_kind)
-
-kc_hs_type ty@(HsAppTy ty1 ty2)
-  = kcHsType fun_ty                      `thenM` \ (fun_ty', fun_kind) ->
-    kcApps fun_kind (ppr fun_ty) arg_tys  `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
-    returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
-  where
-    (fun_ty, arg_tys) = split ty1 [ty2]
-    split (L _ (HsAppTy f a)) as = split f (a:as)
-    split f                  as = (f,as)
-    mk_app fun arg = HsAppTy (noLoc fun) arg   -- Add noLocs for inner nodes of
-                                               -- the application; they are never used
-    
 kc_hs_type (HsPredTy pred)
-  = kcHsPred pred              `thenM` \ pred' ->
-    returnM (HsPredTy pred', liftedTypeKind)
+  = wrongPredErr pred
+
+kc_hs_type (HsCoreTy ty)
+  = return (HsCoreTy ty, typeKind ty)
 
 kc_hs_type (HsForAllTy exp tv_names context ty)
-  = kcHsTyVars tv_names                $ \ tv_names' ->
-    kcHsContext context                `thenM` \ ctxt' ->
-    kcLiftedType ty            `thenM` \ ty' ->
-       -- The body of a forall is usually a type, but in principle
-       -- there's no reason to prohibit *unlifted* types.
-       -- In fact, GHC can itself construct a function with an
-       -- unboxed tuple inside a for-all (via CPR analyis; see 
-       -- typecheck/should_compile/tc170)
-       --
-       -- Still, that's only for internal interfaces, which aren't
-       -- kind-checked, so we only allow liftedTypeKind here
-    returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
+  = kcHsTyVars tv_names         $ \ tv_names' ->
+    do { ctxt' <- kcHsContext context
+       ; ty'   <- kcLiftedType ty
+            -- The body of a forall is usually a type, but in principle
+            -- there's no reason to prohibit *unlifted* types.
+            -- In fact, GHC can itself construct a function with an
+            -- unboxed tuple inside a for-all (via CPR analyis; see 
+            -- typecheck/should_compile/tc170)
+            --
+            -- Still, that's only for internal interfaces, which aren't
+            -- kind-checked, so we only allow liftedTypeKind here
+
+       ; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
 
 kc_hs_type (HsBangTy b ty)
-  = do { (ty', kind) <- kcHsType ty
+  = do { (ty', kind) <- kc_lhs_type ty
        ; return (HsBangTy b ty', kind) }
 
-kc_hs_type ty@(HsSpliceTy _)
-  = failWithTc (ptext SLIT("Unexpected type splice:") <+> ppr ty)
+kc_hs_type ty@(HsRecTy _)
+  = failWithTc (ptext (sLit "Unexpected record type") <+> ppr ty)
+      -- Record types (which only show up temporarily in constructor signatures) 
+      -- should have been removed by now
+
+#ifdef GHCI    /* Only if bootstrapped */
+kc_hs_type (HsSpliceTy sp fvs _) = kcSpliceType sp fvs
+#else
+kc_hs_type ty@(HsSpliceTy {}) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
+#endif
+
+kc_hs_type (HsQuasiQuoteTy {}) = panic "kc_hs_type"    -- Eliminated by renamer
 
+-- remove the doc nodes here, no need to worry about the location since
+-- its the same for a doc node and it's child type node
+kc_hs_type (HsDocTy ty _)
+  = kc_hs_type (unLoc ty) 
 
 ---------------------------
-kcApps :: TcKind                       -- Function kind
-       -> SDoc                         -- Function 
+kcApps :: Outputable a
+       => a 
+       -> TcKind                       -- Function kind
        -> [LHsType Name]               -- Arg types
        -> TcM ([LHsType Name], TcKind) -- Kind-checked args
-kcApps fun_kind ppr_fun args
-  = split_fk fun_kind (length args)    `thenM` \ (arg_kinds, res_kind) ->
-    zipWithM kc_arg args arg_kinds     `thenM` \ args' ->
-    returnM (args', res_kind)
-  where
-    split_fk fk 0 = returnM ([], fk)
-    split_fk fk n = unifyFunKind fk    `thenM` \ mb_fk ->
-                   case mb_fk of 
-                       Nothing       -> failWithTc too_many_args 
-                       Just (ak,fk') -> split_fk fk' (n-1)     `thenM` \ (aks, rk) ->
-                                        returnM (ak:aks, rk)
+kcApps the_fun fun_kind args
+  = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
+       ; args' <- kc_check_lhs_types args_w_kinds
+       ; return (args', res_kind) }
+
+kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
+           -> HsType Name     -- The type being checked (for err messages only)
+           -> ExpKind         -- Expected kind
+           -> TcM [LHsType Name]
+kcCheckApps the_fun fun_kind args ty exp_kind
+  = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
+       ; checkExpectedKind ty res_kind exp_kind
+                    -- Check the result kind *before* checking argument kinds
+            -- This improves error message; Trac #2994
+       ; kc_check_lhs_types args_w_kinds }
 
-    kc_arg arg arg_kind = kcCheckHsType arg arg_kind
 
-    too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
-                   ptext SLIT("is applied to too many type arguments")
+---------------------------
+splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
+splitFunKind _       _      fk [] = return ([], fk)
+splitFunKind the_fun arg_no fk (arg:args)
+  = do { mb_fk <- matchExpectedFunKind fk
+       ; case mb_fk of
+            Nothing       -> failWithTc too_many_args 
+            Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
+                                ; return ((arg, EK ak (EkArg the_fun arg_no)):aks, rk) } }
+  where
+    too_many_args = quotes the_fun <+>
+                   ptext (sLit "is applied to too many type arguments")
 
 ---------------------------
 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
-kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt
+kcHsContext ctxt = wrapLocM (mapM kcHsLPred) ctxt
 
 kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
 kcHsLPred = wrapLocM kcHsPred
 
 kcHsPred :: HsPred Name -> TcM (HsPred Name)
-kcHsPred pred  -- Checks that the result is of kind liftedType
-  = kc_pred pred                               `thenM` \ (pred', kind) ->
-    checkExpectedKind pred kind liftedTypeKind `thenM_` 
-    returnM pred'
+kcHsPred pred = do      -- Checks that the result is a type kind
+    (pred', kind) <- kc_pred pred
+    checkExpectedKind pred kind ekOpen
+    return pred'
     
 ---------------------------
 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)    
        -- Does *not* check for a saturated
        -- application (reason: used from TcDeriv)
-kc_pred pred@(HsIParam name ty)
-  = kcHsType ty                `thenM` \ (ty', kind) ->
-    returnM (HsIParam name ty', kind)
-
-kc_pred pred@(HsClassP cls tys)
-  = kcClass cls                        `thenM` \ kind ->
-    kcApps kind (ppr cls) tys  `thenM` \ (tys', res_kind) ->
-    returnM (HsClassP cls tys', res_kind)
+kc_pred (HsIParam name ty)
+  = do { (ty', kind) <- kc_lhs_type ty
+       ; return (HsIParam name ty', kind) }
+kc_pred (HsClassP cls tys)
+  = do { kind <- kcClass cls
+       ; (tys', res_kind) <- kcApps cls kind tys
+       ; return (HsClassP cls tys', res_kind) }
+kc_pred (HsEqualP ty1 ty2)
+  = do { (ty1', kind1) <- kc_lhs_type ty1
+       ; (ty2', kind2) <- kc_lhs_type ty2
+       ; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
+       ; return (HsEqualP ty1' ty2', unliftedTypeKind) }
 
 ---------------------------
 kcTyVar :: Name -> TcM TcKind
-kcTyVar name   -- Could be a tyvar or a tycon
-  = traceTc (text "lk1" <+> ppr name)  `thenM_`
-    tcLookup name      `thenM` \ thing ->
-    traceTc (text "lk2" <+> ppr name <+> ppr thing)    `thenM_`
+kcTyVar name = do      -- Could be a tyvar or a tycon
+    traceTc "lk1" (ppr name)
+    thing <- tcLookup name
+    traceTc "lk2" (ppr name <+> ppr thing)
     case thing of 
-       ATyVar _ ty             -> returnM (typeKind ty)
-       AThing kind             -> returnM kind
-       AGlobal (ATyCon tc)     -> returnM (tyConKind tc) 
-       other                   -> wrongThingErr "type" thing name
+        ATyVar _ ty             -> return (typeKind ty)
+        AThing kind             -> return kind
+        AGlobal (ATyCon tc)     -> return (tyConKind tc)
+        _                       -> wrongThingErr "type" thing name
 
 kcClass :: Name -> TcM TcKind
-kcClass cls    -- Must be a class
-  = tcLookup cls                               `thenM` \ thing -> 
+kcClass cls = do       -- Must be a class
+    thing <- tcLookup cls
     case thing of
-       AThing kind             -> returnM kind
-       AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
-       other                   -> wrongThingErr "class" thing cls
+        AThing kind             -> return kind
+        AGlobal (AClass cls)    -> return (tyConKind (classTyCon cls))
+        _                       -> wrongThingErr "class" thing cls
 \end{code}
 
 
@@ -437,64 +555,84 @@ dsHsType :: LHsType Name -> TcM Type
 -- All HsTyVarBndrs in the intput type are kind-annotated
 dsHsType ty = ds_type (unLoc ty)
 
-ds_type ty@(HsTyVar name)
+ds_type :: HsType Name -> TcM Type
+ds_type ty@(HsTyVar _)
   = ds_app ty []
 
 ds_type (HsParTy ty)           -- Remove the parentheses markers
   = dsHsType ty
 
-ds_type ty@(HsBangTy _ _)      -- No bangs should be here
-  = failWithTc (ptext SLIT("Unexpected strictness annotation:") <+> ppr ty)
+ds_type ty@(HsBangTy {})    -- No bangs should be here
+  = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
 
-ds_type (HsKindSig ty k)
-  = dsHsType ty        -- Kind checking done already
-
-ds_type (HsListTy ty)
-  = dsHsType ty                        `thenM` \ tau_ty ->
-    checkWiredInTyCon listTyCon        `thenM_`
-    returnM (mkListTy tau_ty)
+ds_type ty@(HsRecTy {})            -- No bangs should be here
+  = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
 
-ds_type (HsPArrTy ty)
-  = dsHsType ty                        `thenM` \ tau_ty ->
-    checkWiredInTyCon parrTyCon        `thenM_`
-    returnM (mkPArrTy tau_ty)
+ds_type (HsKindSig ty _)
+  = dsHsType ty        -- Kind checking done already
 
-ds_type (HsTupleTy boxity tys)
-  = dsHsTypes tys              `thenM` \ tau_tys ->
-    checkWiredInTyCon tycon    `thenM_`
-    returnM (mkTyConApp tycon tau_tys)
+ds_type (HsListTy ty) = do
+    tau_ty <- dsHsType ty
+    checkWiredInTyCon listTyCon
+    return (mkListTy tau_ty)
+
+ds_type (HsPArrTy ty) = do
+    tau_ty <- dsHsType ty
+    checkWiredInTyCon parrTyCon
+    return (mkPArrTy tau_ty)
+
+ds_type (HsModalBoxType ecn ty) = do
+    tau_ty <- dsHsType ty
+    checkWiredInTyCon hetMetCodeTypeTyCon
+    return (mkHetMetCodeTypeTy (mkTyVar ecn ecKind) tau_ty)
+
+ds_type (HsKappaTy ty1 ty2) = do
+    tau_ty1 <- dsHsType ty1
+    tau_ty2 <- dsHsType ty2
+    return (mkHetMetKappaTy tau_ty1 tau_ty2)
+
+ds_type (HsTupleTy boxity tys) = do
+    tau_tys <- dsHsTypes tys
+    checkWiredInTyCon tycon
+    return (mkTyConApp tycon tau_tys)
   where
     tycon = tupleTyCon boxity (length tys)
 
-ds_type (HsFunTy ty1 ty2)
-  = dsHsType ty1                       `thenM` \ tau_ty1 ->
-    dsHsType ty2                       `thenM` \ tau_ty2 ->
-    returnM (mkFunTy tau_ty1 tau_ty2)
+ds_type (HsFunTy ty1 ty2) = do
+    tau_ty1 <- dsHsType ty1
+    tau_ty2 <- dsHsType ty2
+    return (mkFunTy tau_ty1 tau_ty2)
 
-ds_type (HsOpTy ty1 (L span op) ty2)
-  = dsHsType ty1               `thenM` \ tau_ty1 ->
-    dsHsType ty2               `thenM` \ tau_ty2 ->
+ds_type (HsOpTy ty1 (L span op) ty2) = do
+    tau_ty1 <- dsHsType ty1
+    tau_ty2 <- dsHsType ty2
     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 
-ds_type (HsNumTy n)
-  = ASSERT(n==1)
-    tcLookupTyCon genUnitTyConName     `thenM` \ tc ->
-    returnM (mkTyConApp tc [])
-
 ds_type ty@(HsAppTy _ _)
   = ds_app ty []
 
-ds_type (HsPredTy pred)
-  = dsHsPred pred      `thenM` \ pred' ->
-    returnM (mkPredTy pred')
+ds_type (HsPredTy pred) = do
+    pred' <- dsHsPred pred
+    return (mkPredTy pred')
+
+ds_type (HsForAllTy _ tv_names ctxt ty)
+  = tcTyVarBndrs tv_names               $ \ tyvars -> do
+    theta <- mapM dsHsLPred (unLoc ctxt)
+    tau <- dsHsType ty
+    return (mkSigmaTy tyvars theta tau)
+
+ds_type (HsDocTy ty _)  -- Remove the doc comment
+  = dsHsType ty
 
-ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
-  = tcTyVarBndrs tv_names              $ \ tyvars ->
-    mappM dsHsLPred (unLoc ctxt)       `thenM` \ theta ->
-    dsHsType ty                                `thenM` \ tau ->
-    returnM (mkSigmaTy tyvars theta tau)
+ds_type (HsSpliceTy _ _ kind) 
+  = do { kind' <- zonkTcKindToKind kind
+       ; newFlexiTyVarTy kind' }
 
-dsHsTypes arg_tys = mappM dsHsType arg_tys
+ds_type (HsQuasiQuoteTy {}) = panic "ds_type"  -- Eliminated by renamer
+ds_type (HsCoreTy ty)       = return ty
+
+dsHsTypes :: [LHsType Name] -> TcM [Type]
+dsHsTypes arg_tys = mapM dsHsType arg_tys
 \end{code}
 
 Help functions for type applications
@@ -505,20 +643,20 @@ ds_app :: HsType Name -> [LHsType Name] -> TcM Type
 ds_app (HsAppTy ty1 ty2) tys
   = ds_app (unLoc ty1) (ty2:tys)
 
-ds_app ty tys
-  = dsHsTypes tys                      `thenM` \ arg_tys ->
+ds_app ty tys = do
+    arg_tys <- dsHsTypes tys
     case ty of
        HsTyVar fun -> ds_var_app fun arg_tys
-       other       -> ds_type ty               `thenM` \ fun_ty ->
-                      returnM (mkAppTys fun_ty arg_tys)
+       _           -> do fun_ty <- ds_type ty
+                          return (mkAppTys fun_ty arg_tys)
 
 ds_var_app :: Name -> [Type] -> TcM Type
-ds_var_app name arg_tys 
- = tcLookup name                       `thenM` \ thing ->
+ds_var_app name arg_tys = do
+    thing <- tcLookup name
     case thing of
-       ATyVar _ ty         -> returnM (mkAppTys ty arg_tys)
-       AGlobal (ATyCon tc) -> returnM (mkTyConApp tc arg_tys)
-       other               -> wrongThingErr "type" thing name
+       ATyVar _ ty         -> return (mkAppTys ty arg_tys)
+       AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
+       _                   -> wrongThingErr "type" thing name
 \end{code}
 
 
@@ -529,46 +667,32 @@ Contexts
 dsHsLPred :: LHsPred Name -> TcM PredType
 dsHsLPred pred = dsHsPred (unLoc pred)
 
-dsHsPred pred@(HsClassP class_name tys)
-  = dsHsTypes tys                      `thenM` \ arg_tys ->
-    tcLookupClass class_name           `thenM` \ clas ->
-    returnM (ClassP clas arg_tys)
-
+dsHsPred :: HsPred Name -> TcM PredType
+dsHsPred (HsClassP class_name tys)
+  = do { arg_tys <- dsHsTypes tys
+       ; clas <- tcLookupClass class_name
+       ; return (ClassP clas arg_tys)
+       }
+dsHsPred (HsEqualP ty1 ty2)
+  = do { arg_ty1 <- dsHsType ty1
+       ; arg_ty2 <- dsHsType ty2
+       ; return (EqPred arg_ty1 arg_ty2)
+       }
 dsHsPred (HsIParam name ty)
-  = dsHsType ty                                        `thenM` \ arg_ty ->
-    returnM (IParam name arg_ty)
+  = do { arg_ty <- dsHsType ty
+       ; return (IParam name arg_ty)
+       }
 \end{code}
 
-GADT constructor signatures
-
 \begin{code}
-tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
-tcLHsConResTy ty@(L span _) 
-  = setSrcSpan span $ 
-    addErrCtxt (gadtResCtxt ty) $
-    tc_con_res ty []
-
-tc_con_res (L _ (HsAppTy fun res_ty)) res_tys
-  = do { res_ty' <- dsHsType res_ty
-       ; tc_con_res fun (res_ty' : res_tys) }
-
-tc_con_res ty@(L _ (HsTyVar name)) res_tys
-  = do { thing <- tcLookup name
-       ; case thing of
-           AGlobal (ATyCon tc) -> return (tc, res_tys)
-           other -> failWithTc (badGadtDecl ty)
-       }
-
-tc_con_res ty _ = failWithTc (badGadtDecl ty)
-
-gadtResCtxt ty
-  = hang (ptext SLIT("In the result type of a data constructor:"))
-       2 (ppr ty)
-badGadtDecl ty
-  = hang (ptext SLIT("Malformed constructor result type:"))
-       2 (ppr ty)
-
-typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
+addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
+       -- Wrap a context around only if we want to show that contexts.  
+addKcTypeCtxt (L _ (HsPredTy _)) thing = thing
+       -- Omit invisble ones and ones user's won't grok (HsPred p).
+addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing
+
+typeCtxt :: HsType Name -> SDoc
+typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
 \end{code}
 
 %************************************************************************
@@ -583,15 +707,14 @@ kcHsTyVars :: [LHsTyVarBndr Name]
           -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
                                                -- They scope over the thing inside
           -> TcM r
-kcHsTyVars tvs thing_inside 
-  = mappM (wrapLocM kcHsTyVar) tvs     `thenM` \ bndrs ->
-    tcExtendKindEnvTvs bndrs (thing_inside bndrs)
+kcHsTyVars tvs thing_inside
+  = do { kinded_tvs <- mapM (wrapLocM kcHsTyVar) tvs
+       ; tcExtendKindEnvTvs kinded_tvs thing_inside }
 
 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
        -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it      
-kcHsTyVar (UserTyVar name)        = newKindVar         `thenM` \ kind ->
-                                   returnM (KindedTyVar name kind)
-kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
+kcHsTyVar (UserTyVar name _)  = UserTyVar name <$> newKindVar
+kcHsTyVar tv@(KindedTyVar {}) = return tv
 
 ------------------
 tcTyVarBndrs :: [LHsTyVarBndr Name]    -- Kind-annotated binders, which need kind-zonking
@@ -599,46 +722,65 @@ tcTyVarBndrs :: [LHsTyVarBndr Name]       -- Kind-annotated binders, which need kind-
             -> TcM r
 -- Used when type-checking types/classes/type-decls
 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
-tcTyVarBndrs bndrs thing_inside
-  = mapM (zonk . unLoc) bndrs  `thenM` \ tyvars ->
+tcTyVarBndrs bndrs thing_inside = do
+    tyvars <- mapM (zonk . unLoc) bndrs
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
   where
-    zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
-                                     ; return (mkTyVar name kind') }
-    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
-                           return (mkTyVar name liftedTypeKind)
+    zonk (UserTyVar name kind) = do { kind' <- zonkTcKindToKind kind
+                                   ; return (mkTyVar name kind') }
+    zonk (KindedTyVar name kind) = return (mkTyVar name kind)
 
 -----------------------------------
 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
--- GADT decls can have a (perhpas partial) kind signature
+-- GADT decls can have a (perhaps partial) kind signature
 --     e.g.  data T :: * -> * -> * where ...
 -- This function makes up suitable (kinded) type variables for 
--- the argument kinds, and checks that the result kind is indeed *
+-- the argument kinds, and checks that the result kind is indeed *.
+-- We use it also to make up argument type variables for for data instances.
 tcDataKindSig Nothing = return []
 tcDataKindSig (Just kind)
   = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
        ; span <- getSrcSpanM
        ; us   <- newUniqueSupply 
-       ; let loc   = srcSpanStart span
-             uniqs = uniqsFromSupply us
-       ; return [ mk_tv loc uniq str kind 
-                | ((kind, str), uniq) <- arg_kinds `zip` names `zip` uniqs ] }
+       ; let uniqs = uniqsFromSupply us
+       ; return [ mk_tv span uniq str kind 
+                | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
   where
     (arg_kinds, res_kind) = splitKindFunTys kind
     mk_tv loc uniq str kind = mkTyVar name kind
        where
           name = mkInternalName uniq occ loc
           occ  = mkOccName tvName str
+         
+    dnames = map ('$' :) names -- Note [Avoid name clashes for associated data types]
 
-    names :: [String]  -- a,b,c...aa,ab,ac etc
+    names :: [String]
     names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 
 
 badKindSig :: Kind -> SDoc
 badKindSig kind 
- = hang (ptext SLIT("Kind signature on data type declaration has non-* return kind"))
+ = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
        2 (ppr kind)
 \end{code}
 
+Note [Avoid name clashes for associated data types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider    class C a b where
+               data D b :: * -> *
+When typechecking the decl for D, we'll invent an extra type variable for D,
+to fill out its kind.  We *don't* want this type variable to be 'a', because
+in an .hi file we'd get
+            class C a b where
+               data D b a 
+which makes it look as if there are *two* type indices.  But there aren't!
+So we use $a instead, which cannot clash with a user-written type variable.
+Remember that type variable binders in interface files are just FastStrings,
+not proper Names.
+
+(The tidying phase can't help here because we don't tidy TyCons.  Another
+alternative would be to record the number of indexing parameters in the 
+interface file.)
+
 
 %************************************************************************
 %*                                                                     *
@@ -696,37 +838,35 @@ tcHsPatSigType ctxt hs_ty
                -- should be bound by the pattern signature
          in_scope <- getInLocalScope
        ; let span = getLoc hs_ty
-             sig_tvs = [ L span (UserTyVar n) 
-                       | n <- nameSetToList (extractHsTyVars hs_ty),
-                         not (in_scope n) ]
-
-       -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
-       -- except that we want to keep the tvs separate
-       ; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
-                                   { kinded_ty <- kcTypeType hs_ty
-                                   ; return (kinded_tvs, kinded_ty) }
-       ; tcTyVarBndrs kinded_tvs $ \ tyvars -> do
-       { sig_ty <- dsHsType kinded_ty
+             sig_tvs = userHsTyVarBndrs $ map (L span) $ 
+                       filterOut in_scope $
+                        nameSetToList (extractHsTyVars hs_ty)
+
+       ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
        ; checkValidType ctxt sig_ty 
        ; return (tyvars, sig_ty)
-      } }
+      }
 
 tcPatSig :: UserTypeCtxt
         -> LHsType Name
-        -> BoxySigmaType
+        -> TcSigmaType
         -> TcM (TcType,           -- The type to use for "inside" the signature
-                [(Name,TcType)])  -- The new bit of type environment, binding
+                [(Name, TcType)], -- The new bit of type environment, binding
                                   -- the scoped type variables
+                 HsWrapper)        -- Coercion due to unification with actual ty
+                                   -- Of shape:  res_ty ~ sig_ty
 tcPatSig ctxt sig res_ty
   = do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
+       -- sig_tvs are the type variables free in 'sig', 
+       -- and not already in scope. These are the ones
+       -- that should be brought into scope
 
        ; if null sig_tvs then do {
                -- The type signature binds no type variables, 
                -- and hence is rigid, so use it to zap the res_ty
-                 boxyUnify sig_ty res_ty
-               ; return (sig_ty, [])
-
-       } else do {
+                  wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
+               ; return (sig_ty, [], wrap)
+        } else do {
                -- Type signature binds at least one scoped type variable
        
                -- A pattern binding cannot bind scoped type variables
@@ -735,50 +875,137 @@ tcPatSig ctxt sig res_ty
                -- So we just have an ASSERT here
        ; let in_pat_bind = case ctxt of
                                BindPatSigCtxt -> True
-                               other          -> False
+                               _              -> False
        ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
 
-               -- Check that pat_ty is rigid
-       ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
-
-               -- Now match the pattern signature against res_ty
-               -- For convenience, and uniform-looking error messages
-               -- we do the matching by allocating meta type variables, 
-               -- unifying, and reading out the results.
-               -- This is a strictly local operation.
-       ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
-       ; boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) res_ty
-       ; sig_tv_tys <- mapM readFilledBox box_tvs
-
-               -- Check that each is bound to a distinct type variable,
-               -- and one that is not already in scope
-       ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
-       ; binds_in_scope <- getScopedTyVarBinds
+               -- Check that all newly-in-scope tyvars are in fact
+               -- constrained by the pattern.  This catches tiresome
+               -- cases like   
+               --      type T a = Int
+               --      f :: Int -> Int
+               --      f (x :: T a) = ...
+               -- Here 'a' doesn't get a binding.  Sigh
+       ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
+       ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
+
+       -- Now do a subsumption check of the pattern signature against res_ty
+        ; sig_tvs' <- tcInstSigTyVars sig_tvs
+        ; let sig_ty' = substTyWith sig_tvs sig_tv_tys' sig_ty
+              sig_tv_tys' = mkTyVarTys sig_tvs'
+       ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty'
+
+       -- Check that each is bound to a distinct type variable,
+       -- and one that is not already in scope
+        ; binds_in_scope <- getScopedTyVarBinds
+       ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys'
        ; check binds_in_scope tv_binds
        
-               -- Phew!
-       ; return (res_ty, tv_binds)
-       } }
+       -- Phew!
+        ; return (sig_ty', tv_binds, wrap)
+        } }
   where
-    check in_scope []           = return ()
+    check _ [] = return ()
     check in_scope ((n,ty):rest) = do { check_one in_scope n ty
                                      ; check ((n,ty):in_scope) rest }
 
     check_one in_scope n ty
-       = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
-               -- Must bind to a type variable
-
-            ; checkTc (null dups) (dupInScope n (head dups) ty)
+       = checkTc (null dups) (dupInScope n (head dups) ty)
                -- Must not bind to the same type variable
                -- as some other in-scope type variable
-
-            ; return () }
        where
-         dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
+         dups = [n' | (n',ty') <- in_scope, eqType ty' ty]
 \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}
+-- The ExpKind datatype means "expected kind" and contains 
+-- some info about just why that kind is expected, to improve
+-- the error message on a mis-match
+data ExpKind = EK TcKind EkCtxt
+data EkCtxt  = EkUnk           -- Unknown context
+            | EkEqPred         -- Second argument of an equality predicate
+            | EkKindSig        -- Kind signature
+            | EkArg SDoc Int   -- Function, arg posn, expected kind
+
+
+ekLifted, ekOpen :: ExpKind
+ekLifted = EK liftedTypeKind EkUnk
+ekOpen   = EK openTypeKind   EkUnk
+
+checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> 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 (EK exp_kind ek_ctxt)
+  | 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 _  -> 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 [ expected_herald ek_ctxt <+> ptext (sLit "kind") 
+                                    <+> quotes (pprKind tidy_exp_kind) <> comma,
+                                 ptext (sLit "but") <+> quotes (ppr ty) <+>
+                                     ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
+
+               expected_herald EkUnk     = ptext (sLit "Expected")
+               expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
+               expected_herald EkEqPred  = ptext (sLit "The left argument of the equality predicate had")
+               expected_herald (EkArg fun arg_no)
+                = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
+                  <+> quotes fun <+> ptext (sLit ("should have"))
+
+           failWithTcM (env2, err $$ more_info)
+\end{code}
+
+%************************************************************************
 %*                                                                     *
                Scoped type variables
 %*                                                                     *
@@ -786,31 +1013,32 @@ tcPatSig ctxt sig res_ty
 
 \begin{code}
 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon, 
+pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon, 
                                 nest 2 (pp_sig ctxt) ]
   where
     pp_sig (FunSigCtxt n)  = pp_n_colon n
     pp_sig (ConArgCtxt n)  = pp_n_colon n
     pp_sig (ForSigCtxt n)  = pp_n_colon n
-    pp_sig (RuleSigCtxt n) = pp_n_colon n
-    pp_sig other          = ppr (unLoc hs_ty)
+    pp_sig _               = ppr (unLoc hs_ty)
 
     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
 
-
-wobblyPatSig sig_tvs
-  = hang (ptext SLIT("A pattern type signature cannot bind scoped type variables") 
-               <+> pprQuotedList sig_tvs)
-       2 (ptext SLIT("unless the pattern has a rigid type context"))
-               
-scopedNonVar n ty
-  = vcat [sep [ptext SLIT("The scoped type variable") <+> quotes (ppr n),
-              nest 2 (ptext SLIT("is bound to the type") <+> quotes (ppr ty))],
-         nest 2 (ptext SLIT("You can only bind scoped type variables to type variables"))]
-
-dupInScope n n' ty
-  = hang (ptext SLIT("The scoped type variables") <+> quotes (ppr n) <+> ptext SLIT("and") <+> quotes (ppr n'))
-       2 (vcat [ptext SLIT("are bound to the same type (variable)"),
-               ptext SLIT("Distinct scoped type variables must be distinct")])
+badPatSigTvs :: TcType -> [TyVar] -> SDoc
+badPatSigTvs sig_ty bad_tvs
+  = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, 
+                 quotes (pprWithCommas ppr bad_tvs), 
+                ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
+                ptext (sLit "but are actually discarded by a type synonym") ]
+         , ptext (sLit "To fix this, expand the type synonym") 
+         , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
+
+dupInScope :: Name -> Name -> Type -> SDoc
+dupInScope n n' _
+  = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
+       2 (vcat [ptext (sLit "are bound to the same type (variable)"),
+               ptext (sLit "Distinct scoped type variables must be distinct")])
+
+wrongPredErr :: HsPred Name -> TcM (HsType Name, TcKind)
+wrongPredErr pred = failWithTc (text "Predicate used as a type:" <+> ppr pred)
 \end{code}