fix haddock submodule pointer

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

diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 66102a6..4fe6b60 100644 (file)
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -5,26 +5,19 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \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 TcHsType (
 module TcHsType (

-       tcHsSigType, tcHsDeriv, 
+       tcHsSigType, tcHsSigTypeNC, tcHsDeriv, 

        tcHsInstHead, tcHsQuantifiedType,
        UserTypeCtxt(..), 
 
                -- Kind checking
        kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
        tcHsInstHead, tcHsQuantifiedType,
        UserTypeCtxt(..), 
 
                -- Kind checking
        kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 

-       kcCheckHsType, kcHsContext, kcHsType, 
+       kcLHsType, kcCheckLHsType, kcHsContext, 

        
                -- Typechecking kinded types
        tcHsKindedContext, tcHsKindedType, tcHsBangType,
        
                -- Typechecking kinded types
        tcHsKindedContext, tcHsKindedType, tcHsBangType,

-       tcTyVarBndrs, dsHsType, tcLHsConResTy,
-       tcDataKindSig,
+       tcTyVarBndrs, dsHsType, kcHsLPred, dsHsLPred,
+       tcDataKindSig, ExpKind(..), EkCtxt(..),

 
                -- Pattern type signatures
        tcHsPatSigType, tcPatSig
 
                -- Pattern type signatures
        tcHsPatSigType, tcPatSig

@@ -32,6 +25,10 @@ module TcHsType (
 
 #include "HsVersions.h"
 
 
 #include "HsVersions.h"
 

+#ifdef GHCI    /* Only if bootstrapped */
+import {-# SOURCE #-}  TcSplice( kcSpliceType )
+#endif
+

 import HsSyn
 import RnHsSyn
 import TcRnMonad
 import HsSyn
 import RnHsSyn
 import TcRnMonad

@@ -40,21 +37,21 @@ import TcMType
 import TcUnify
 import TcIface
 import TcType
 import TcUnify
 import TcIface
 import TcType

+import TysPrim ( ecKind )

 import {- Kind parts of -} Type
 import Var
 import {- Kind parts of -} Type
 import Var

+import VarSet

 import TyCon
 import Class
 import Name
 import TyCon
 import Class
 import Name

-import OccName

 import NameSet
 import NameSet

-import PrelNames

 import TysWiredIn
 import BasicTypes
 import SrcLoc
 import TysWiredIn
 import BasicTypes
 import SrcLoc

+import Util

 import UniqSupply
 import Outputable
 import UniqSupply
 import Outputable

-
-import Control.Monad
+import FastString

 \end{code}
 
 
 \end{code}
 
 

@@ -141,25 +138,53 @@ the TyCon being defined.
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \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 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        
        ; return ty }
 
        ; ty <- tcHsKindedType kinded_ty
        ; checkValidType ctxt ty        
        ; return ty }
 

-tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type)
+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.
 -- Typecheck an instance head.  We can't use 
 -- tcHsSigType, because it's not a valid user type.

-tcHsInstHead hs_ty
-  = do { kinded_ty <- kcHsSigType hs_ty
-       ; poly_ty   <- tcHsKindedType kinded_ty
-       ; return (tcSplitSigmaTy poly_ty) }
+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),
 
 tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
 -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),

@@ -172,13 +197,15 @@ tcHsQuantifiedType tv_names hs_ty
        ; return (tvs, ty) } }
 
 -- Used for the deriving(...) items
        ; 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
 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
        ; tcTyVarBndrs tv_names'        $ \ tyvars ->
     do { arg_tys <- dsHsTypes tys
        ; cls <- tcLookupClass cls_name

@@ -191,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
     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
 \end{code}
 
        These functions are used during knot-tying in

@@ -201,8 +228,8 @@ tc_hs_deriv _ other
 \begin{code}
 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
        -- Used for type signatures
 \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.
 
 tcHsKindedType :: LHsType Name -> TcM Type
   -- Don't do kind checking, nor validity checking.

@@ -213,8 +240,8 @@ tcHsKindedType hs_ty = dsHsType hs_ty
 
 tcHsBangType :: LHsType Name -> TcM Type
 -- Permit a bang, but discard it
 
 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)
 
 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
 -- Used when we are expecting a ClassContext (i.e. no implicit params)

@@ -235,39 +262,59 @@ tcHsKindedContext hs_theta = addLocM (mapM dsHsLPred) hs_theta
 ---------------------------
 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
 -- The type ty must be a *lifted* *type*
 ---------------------------
 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 :: 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
 -- 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 (strip ty) act_kind exp_kind
                -- Add the context round the inner check only
                -- because checkExpectedKind already mentions
                -- 'ty' by name in any error message
 
        ; checkExpectedKind (strip ty) act_kind exp_kind

-       ; return (L span ty') }
+       ; return ty' }

   where
   where

-       -- Wrap a context around only if we want to show that contexts.  
-    add_ctxt (HsPredTy p)               thing = thing
-       -- Omit invisble ones and ones user's won't grok (HsPred p).
-    add_ctxt (HsForAllTy _ _ (L _ []) _) thing = thing
-       -- Omit wrapping if the theta-part is empty
-       -- Reason: the recursive call to kcLiftedType, in the ForAllTy
-       --         case of kc_hs_type, will do the wrapping instead
-       --         and we don't want to duplicate
-    add_ctxt other_ty thing = addErrCtxt (typeCtxt other_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
        -- 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

@@ -281,9 +328,17 @@ kcCheckHsType (L span ty) exp_kind
        Here comes the main function
 
 \begin{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
 -- kind as argument as tcExpr does.  
 -- Reasons: 
 --     (a) the kind of (->) is

@@ -293,8 +348,9 @@ kcHsType ty = wrapLocFstM kc_hs_type ty
 --
 -- The translated type has explicitly-kinded type-variable binders
 
 --
 -- The translated type has explicitly-kinded type-variable binders
 

+kc_hs_type :: HsType Name -> TcM (HsType Name, TcKind)

 kc_hs_type (HsParTy ty) = do
 kc_hs_type (HsParTy ty) = do

-   (ty', kind) <- kcHsType ty
+   (ty', kind) <- kc_lhs_type ty

    return (HsParTy ty', kind)
 
 kc_hs_type (HsTyVar name) = do
    return (HsParTy ty', kind)
 
 kc_hs_type (HsTyVar name) = do

@@ -309,11 +365,18 @@ kc_hs_type (HsPArrTy ty) = do
     ty' <- kcLiftedType ty
     return (HsPArrTy ty', liftedTypeKind)
 
     ty' <- kcLiftedType ty
     return (HsPArrTy ty', liftedTypeKind)
 

-kc_hs_type (HsNumTy n)
-   = return (HsNumTy n, 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
 
 kc_hs_type (HsKindSig ty k) = do

-    ty' <- kcCheckHsType ty k
+    ty' <- kc_check_lhs_type ty (EK k EkKindSig)

     return (HsKindSig ty' k, k)
 
 kc_hs_type (HsTupleTy Boxed tys) = do
     return (HsKindSig ty' k, k)
 
 kc_hs_type (HsTupleTy Boxed tys) = do

@@ -325,33 +388,26 @@ kc_hs_type (HsTupleTy Unboxed tys) = do
     return (HsTupleTy Unboxed tys', ubxTupleKind)
 
 kc_hs_type (HsFunTy ty1 ty2) = do
     return (HsTupleTy Unboxed tys', ubxTupleKind)
 
 kc_hs_type (HsFunTy ty1 ty2) = do

-    ty1' <- kcCheckHsType ty1 argTypeKind
+    ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)

     ty2' <- kcTypeType ty2
     return (HsFunTy ty1' ty2', liftedTypeKind)
 
     ty2' <- kcTypeType ty2
     return (HsFunTy ty1' ty2', liftedTypeKind)
 

-kc_hs_type ty@(HsOpTy ty1 op ty2) = do
+kc_hs_type (HsOpTy ty1 op ty2) = do

     op_kind <- addLocM kcTyVar op
     op_kind <- addLocM kcTyVar op

-    ([ty1',ty2'], res_kind) <- kcApps op_kind (ppr op) [ty1,ty2]
+    ([ty1',ty2'], res_kind) <- kcApps op op_kind [ty1,ty2]

     return (HsOpTy ty1' op ty2', res_kind)
 
     return (HsOpTy ty1' op ty2', res_kind)
 

-kc_hs_type ty@(HsAppTy ty1 ty2) = do
-    (fun_ty', fun_kind) <- kcHsType fun_ty
-    ((arg_ty':arg_tys'), res_kind) <- kcApps fun_kind (ppr fun_ty) arg_tys
-    return (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 (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 ty@(HsPredTy (HsEqualP _ _))
-  = wrongEqualityErr
+kc_hs_type (HsPredTy pred)
+  = wrongPredErr pred

 
 

-kc_hs_type (HsPredTy pred) = do
-    pred' <- kcHsPred pred
-    return (HsPredTy pred', liftedTypeKind)
+kc_hs_type (HsCoreTy ty)
+  = return (HsCoreTy ty, typeKind ty)

 
 kc_hs_type (HsForAllTy exp tv_names context ty)
   = kcHsTyVars tv_names         $ \ tv_names' ->
 
 kc_hs_type (HsForAllTy exp tv_names context ty)
   = kcHsTyVars tv_names         $ \ tv_names' ->

@@ -368,12 +424,22 @@ kc_hs_type (HsForAllTy exp tv_names context ty)
 
        ; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
 
 
        ; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
 

-kc_hs_type (HsBangTy b ty) = do
-    (ty', kind) <- kcHsType ty
-    return (HsBangTy b ty', kind)
+kc_hs_type (HsBangTy b ty)
+  = do { (ty', kind) <- kc_lhs_type ty
+       ; return (HsBangTy b ty', kind) }
+
+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

 
 

-kc_hs_type ty@(HsSpliceTy _)
-  = failWithTc (ptext SLIT("Unexpected type splice:") <+> ppr ty)
+#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
 
 -- 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

@@ -381,26 +447,40 @@ kc_hs_type (HsDocTy ty _)
   = kc_hs_type (unLoc 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
        -> [LHsType Name]               -- Arg types
        -> TcM ([LHsType Name], TcKind) -- Kind-checked args

-kcApps fun_kind ppr_fun args = do
-    (arg_kinds, res_kind) <- split_fk fun_kind (length args)
-    args' <- zipWithM kc_arg args arg_kinds
-    return (args', res_kind)
-  where
-    split_fk fk 0 = return ([], fk)
-    split_fk fk n = do mb_fk <- unifyFunKind fk
-                       case mb_fk of
-                          Nothing       -> failWithTc too_many_args 
-                          Just (ak,fk') -> do (aks, rk) <- split_fk fk' (n-1)
-                                              return (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 :: LHsContext Name -> TcM (LHsContext Name)

@@ -410,44 +490,39 @@ kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
 kcHsLPred = wrapLocM kcHsPred
 
 kcHsPred :: HsPred Name -> TcM (HsPred Name)
 kcHsLPred = wrapLocM kcHsPred
 
 kcHsPred :: HsPred Name -> TcM (HsPred Name)

-kcHsPred pred = do     -- Checks that the result is of kind liftedType
+kcHsPred pred = do      -- Checks that the result is a type kind

     (pred', kind) <- kc_pred pred
     (pred', kind) <- kc_pred pred

-    checkExpectedKind pred kind liftedTypeKind
+    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)
     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)
-  = do { (ty', kind) <- kcHsType ty
-       ; return (HsIParam name ty', kind)
-       }
-kc_pred pred@(HsClassP cls tys)
+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
   = do { kind <- kcClass cls

-       ; (tys', res_kind) <- kcApps kind (ppr cls) tys
-       ; return (HsClassP cls tys', res_kind)
-       }
-kc_pred pred@(HsEqualP ty1 ty2)
-  = do { (ty1', kind1) <- kcHsType ty1
---       ; checkExpectedKind ty1 kind1 liftedTypeKind
-       ; (ty2', kind2) <- kcHsType ty2
---       ; checkExpectedKind ty2 kind2 liftedTypeKind
-       ; checkExpectedKind ty2 kind2 kind1
-       ; return (HsEqualP ty1' ty2', liftedTypeKind)
-       }
+       ; (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 = do      -- Could be a tyvar or a tycon
 
 ---------------------------
 kcTyVar :: Name -> TcM TcKind
 kcTyVar name = do      -- Could be a tyvar or a tycon

-    traceTc (text "lk1" <+> ppr name)
+    traceTc "lk1" (ppr name)

     thing <- tcLookup name
     thing <- tcLookup name

-    traceTc (text "lk2" <+> ppr name <+> ppr thing)
+    traceTc "lk2" (ppr name <+> ppr thing)

     case thing of 
         ATyVar _ ty             -> return (typeKind ty)
         AThing kind             -> return kind
         AGlobal (ATyCon tc)     -> return (tyConKind tc)
     case thing of 
         ATyVar _ ty             -> return (typeKind ty)
         AThing kind             -> return kind
         AGlobal (ATyCon tc)     -> return (tyConKind tc)

-        other                   -> wrongThingErr "type" thing name
+        _                       -> wrongThingErr "type" thing name

 
 kcClass :: Name -> TcM TcKind
 kcClass cls = do       -- Must be a class
 
 kcClass :: Name -> TcM TcKind
 kcClass cls = do       -- Must be a class

@@ -455,7 +530,7 @@ kcClass cls = do    -- Must be a class
     case thing of
         AThing kind             -> return kind
         AGlobal (AClass cls)    -> return (tyConKind (classTyCon cls))
     case thing of
         AThing kind             -> return kind
         AGlobal (AClass cls)    -> return (tyConKind (classTyCon cls))

-        other                   -> wrongThingErr "class" thing cls
+        _                       -> wrongThingErr "class" thing cls

 \end{code}
 
 
 \end{code}
 
 

@@ -480,16 +555,20 @@ dsHsType :: LHsType Name -> TcM Type
 -- All HsTyVarBndrs in the intput type are kind-annotated
 dsHsType ty = ds_type (unLoc ty)
 
 -- 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_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)
+ds_type ty@(HsRecTy {})            -- No bangs should be here
+  = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
+
+ds_type (HsKindSig ty _)

   = dsHsType ty        -- Kind checking done already
 
 ds_type (HsListTy ty) = do
   = dsHsType ty        -- Kind checking done already
 
 ds_type (HsListTy ty) = do

@@ -502,6 +581,16 @@ ds_type (HsPArrTy ty) = do
     checkWiredInTyCon parrTyCon
     return (mkPArrTy tau_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
 ds_type (HsTupleTy boxity tys) = do
     tau_tys <- dsHsTypes tys
     checkWiredInTyCon tycon

@@ -519,11 +608,6 @@ ds_type (HsOpTy ty1 (L span op) ty2) = do
     tau_ty2 <- dsHsType ty2
     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 
     tau_ty2 <- dsHsType ty2
     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 

-ds_type (HsNumTy n)
-  = ASSERT(n==1) do
-    tc <- tcLookupTyCon genUnitTyConName
-    return (mkTyConApp tc [])
-

 ds_type ty@(HsAppTy _ _)
   = ds_app ty []
 
 ds_type ty@(HsAppTy _ _)
   = ds_app ty []
 

@@ -531,17 +615,23 @@ ds_type (HsPredTy pred) = do
     pred' <- dsHsPred pred
     return (mkPredTy pred')
 
     pred' <- dsHsPred pred
     return (mkPredTy pred')
 

-ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
+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)
 
   = tcTyVarBndrs tv_names               $ \ tyvars -> do
     theta <- mapM dsHsLPred (unLoc ctxt)
     tau <- dsHsType ty
     return (mkSigmaTy tyvars theta tau)
 

-ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"
-

 ds_type (HsDocTy ty _)  -- Remove the doc comment
   = dsHsType ty
 
 ds_type (HsDocTy ty _)  -- Remove the doc comment
   = dsHsType ty
 

+ds_type (HsSpliceTy _ _ kind) 
+  = do { kind' <- zonkTcKindToKind kind
+       ; newFlexiTyVarTy kind' }
+
+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}
 
 dsHsTypes arg_tys = mapM dsHsType arg_tys
 \end{code}
 

@@ -557,16 +647,16 @@ ds_app ty tys = do
     arg_tys <- dsHsTypes tys
     case ty of
        HsTyVar fun -> ds_var_app fun arg_tys
     arg_tys <- dsHsTypes tys
     case ty of
        HsTyVar fun -> ds_var_app fun arg_tys

-       other       -> do fun_ty <- ds_type ty
+       _           -> 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 = do
     thing <- tcLookup name
     case thing of
                           return (mkAppTys fun_ty arg_tys)
 
 ds_var_app :: Name -> [Type] -> TcM Type
 ds_var_app name arg_tys = do
     thing <- tcLookup name
     case thing of

-       ATyVar _ ty         -> return (mkAppTys ty arg_tys)
+       ATyVar _ ty         -> return (mkAppTys ty arg_tys)

        AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
        AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)

-       other               -> wrongThingErr "type" thing name
+       _                   -> wrongThingErr "type" thing name

 \end{code}
 
 
 \end{code}
 
 

@@ -577,12 +667,13 @@ Contexts
 dsHsLPred :: LHsPred Name -> TcM PredType
 dsHsLPred pred = dsHsPred (unLoc pred)
 
 dsHsLPred :: LHsPred Name -> TcM PredType
 dsHsLPred pred = dsHsPred (unLoc pred)
 

-dsHsPred pred@(HsClassP class_name 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)
        }
   = do { arg_tys <- dsHsTypes tys
        ; clas <- tcLookupClass class_name
        ; return (ClassP clas arg_tys)
        }

-dsHsPred pred@(HsEqualP ty1 ty2)
+dsHsPred (HsEqualP ty1 ty2)

   = do { arg_ty1 <- dsHsType ty1
        ; arg_ty2 <- dsHsType ty2
        ; return (EqPred arg_ty1 arg_ty2)
   = do { arg_ty1 <- dsHsType ty1
        ; arg_ty2 <- dsHsType ty2
        ; return (EqPred arg_ty1 arg_ty2)

@@ -593,35 +684,15 @@ dsHsPred (HsIParam name ty)
        }
 \end{code}
 
        }
 \end{code}
 

-GADT constructor signatures
-

 \begin{code}
 \begin{code}

-tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
-tcLHsConResTy (L span res_ty)
-  = setSrcSpan span $
-    case get_args res_ty [] of
-          (HsTyVar tc_name, args) 
-             -> do { args' <- mapM dsHsType args
-                   ; thing <- tcLookup tc_name
-                   ; case thing of
-                       AGlobal (ATyCon tc) -> return (tc, args')
-                       other -> failWithTc (badGadtDecl res_ty) }
-          other -> failWithTc (badGadtDecl res_ty)
-  where
-       -- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
-       -- because that causes a black hole, and for good reason.  Building
-       -- the type means expanding type synonyms, and we can't do that
-       -- inside the "knot".  So we have to work by steam.
-    get_args (HsAppTy (L _ fun) arg)     args = get_args fun (arg:args)
-    get_args (HsParTy (L _ ty))          args = get_args ty  args
-    get_args (HsOpTy ty1 (L span tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
-    get_args ty                          args = (ty, args)
-
-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}
 
 %************************************************************************
 \end{code}
 
 %************************************************************************

@@ -636,14 +707,14 @@ kcHsTyVars :: [LHsTyVarBndr Name]
           -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
                                                -- They scope over the thing inside
           -> TcM r
           -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
                                                -- They scope over the thing inside
           -> TcM r

-kcHsTyVars tvs thing_inside  = do
-    bndrs <- mapM (wrapLocM kcHsTyVar) tvs
-    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 :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
        -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it      

-kcHsTyVar (UserTyVar name)        = KindedTyVar name <$> newKindVar
-kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind)
+kcHsTyVar (UserTyVar name _)  = UserTyVar name <$> newKindVar
+kcHsTyVar tv@(KindedTyVar {}) = return tv

 
 ------------------
 tcTyVarBndrs :: [LHsTyVarBndr Name]    -- Kind-annotated binders, which need kind-zonking
 
 ------------------
 tcTyVarBndrs :: [LHsTyVarBndr Name]    -- Kind-annotated binders, which need kind-zonking

@@ -655,10 +726,9 @@ tcTyVarBndrs bndrs thing_inside = do
     tyvars <- mapM (zonk . unLoc) bndrs
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
   where
     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) = WARN( True, ptext SLIT("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]
 
 -----------------------------------
 tcDataKindSig :: Maybe Kind -> TcM [TyVar]

@@ -674,23 +744,43 @@ tcDataKindSig (Just kind)
        ; us   <- newUniqueSupply 
        ; let uniqs = uniqsFromSupply us
        ; return [ mk_tv span uniq str kind 
        ; us   <- newUniqueSupply 
        ; let uniqs = uniqsFromSupply us
        ; return [ mk_tv span uniq str kind 

-                | ((kind, str), uniq) <- arg_kinds `zip` names `zip` uniqs ] }
+                | ((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
   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 
     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}
 
        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.)
+

 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *

@@ -748,9 +838,9 @@ tcHsPatSigType ctxt hs_ty
                -- should be bound by the pattern signature
          in_scope <- getInLocalScope
        ; let span = getLoc 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) ]
+             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 
 
        ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
        ; checkValidType ctxt sig_ty 

@@ -759,20 +849,24 @@ tcHsPatSigType ctxt hs_ty
 
 tcPatSig :: UserTypeCtxt
         -> LHsType Name
 
 tcPatSig :: UserTypeCtxt
         -> LHsType Name

-        -> BoxySigmaType
+        -> TcSigmaType

         -> TcM (TcType,           -- The type to use for "inside" the signature
         -> 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
                                   -- 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
 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
 
        ; 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
                -- Type signature binds at least one scoped type variable
        
                -- A pattern binding cannot bind scoped type variables

@@ -781,50 +875,137 @@ tcPatSig ctxt sig res_ty
                -- So we just have an ASSERT here
        ; let in_pat_bind = case ctxt of
                                BindPatSigCtxt -> True
                -- 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 ()
 
        ; 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
        
        ; check binds_in_scope tv_binds
        

-               -- Phew!
-       ; return (res_ty, tv_binds)
-       } }
+       -- Phew!
+        ; return (sig_ty', tv_binds, wrap)
+        } }

   where
   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
     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
                -- Must not bind to the same type variable
                -- as some other in-scope type variable

-
-            ; return () }

        where
        where

-         dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
+         dups = [n' | (n',ty') <- in_scope, eqType ty' ty]

 \end{code}
 
 
 %************************************************************************
 \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
 %*                                                                     *
 %*                                                                     *
                Scoped type variables
 %*                                                                     *

@@ -832,33 +1013,32 @@ tcPatSig ctxt sig res_ty
 
 \begin{code}
 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
 
 \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
                                 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 other          = ppr (unLoc hs_ty)
+    pp_sig _               = ppr (unLoc hs_ty)

 
     pp_n_colon n = ppr n <+> dcolon <+> 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")])
-
-wrongEqualityErr
-  = failWithTc (text "Equality predicate used as a type")
+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}
 
 \end{code}