fix haddock submodule pointer

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

diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index b29dc9a..4fe6b60 100644 (file)
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -5,10 +5,8 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}

-{-# LANGUAGE RelaxedPolyRec #-}
-

 module TcHsType (
 module TcHsType (

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

        tcHsInstHead, tcHsQuantifiedType,
        UserTypeCtxt(..), 
 
        tcHsInstHead, tcHsQuantifiedType,
        UserTypeCtxt(..), 
 

@@ -18,8 +16,8 @@ module TcHsType (
        
                -- 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

@@ -27,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

@@ -35,23 +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 Coercion
+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 FastString
 import UniqSupply
 import Outputable
 import FastString

-
-import Control.Monad

 \end{code}
 
 
 \end{code}
 
 

@@ -138,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),

@@ -234,20 +262,20 @@ 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 = kc_check_lhs_type 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 = kc_check_lhs_type ty openTypeKind
+kcTypeType ty = kc_check_lhs_type ty ekOpen

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

-kcCheckLHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
+kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)

 kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind
 
 
 kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind
 
 

-kc_check_lhs_type :: LHsType Name -> TcKind -> TcM (LHsType Name)
+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

@@ -256,7 +284,7 @@ kc_check_lhs_type (L span ty) exp_kind
     do { ty' <- kc_check_hs_type ty exp_kind
        ; return (L span ty') }
 
     do { ty' <- kc_check_hs_type ty exp_kind
        ; return (L span ty') }
 

-kc_check_lhs_types :: [(LHsType Name,TcKind)] -> TcM [LHsType Name]
+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_check_lhs_types tys_w_kinds
   = mapM kc_arg tys_w_kinds
   where

@@ -264,7 +292,7 @@ kc_check_lhs_types tys_w_kinds
 
 
 ---------------------------
 
 
 ---------------------------

-kc_check_hs_type :: HsType Name -> TcKind -> TcM (HsType Name)
+kc_check_hs_type :: HsType Name -> ExpKind -> TcM (HsType Name)

 
 -- First some special cases for better error messages 
 -- when we know the expected kind
 
 -- First some special cases for better error messages 
 -- when we know the expected kind

@@ -272,16 +300,11 @@ 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 { 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
+  = 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') }
 
        ; (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') }
 

-kc_check_hs_type ty@(HsPredTy (HsClassP cls tys)) exp_kind
-  = do { cls_kind <- kcClass cls
-       ; tys' <- kcCheckApps cls cls_kind tys ty exp_kind
-       ; return (HsPredTy (HsClassP cls 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
 -- 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

@@ -300,7 +323,6 @@ kc_check_hs_type ty exp_kind
     strip (HsBangTy _ (L _ ty))       = strip ty
     strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
     strip ty                         = ty
     strip (HsBangTy _ (L _ ty))       = strip ty
     strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
     strip ty                         = ty

-

 \end{code}
 
        Here comes the main function
 \end{code}
 
        Here comes the main function

@@ -343,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' <- kc_check_lhs_type 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

@@ -359,7 +388,7 @@ 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' <- kc_check_lhs_type 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)
 

@@ -369,18 +398,16 @@ kc_hs_type (HsOpTy ty1 op ty2) = do
     return (HsOpTy ty1' op ty2', res_kind)
 
 kc_hs_type (HsAppTy ty1 ty2) = do
     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)
     (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)

-  where
-    (fun_ty, arg_tys) = splitHsAppTys ty1 ty2

 
 

-kc_hs_type (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' ->

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

@@ -416,47 +453,33 @@ kcApps :: Outputable a
        -> [LHsType Name]               -- Arg types
        -> TcM ([LHsType Name], TcKind) -- Kind-checked args
 kcApps the_fun fun_kind args
        -> [LHsType Name]               -- Arg types
        -> TcM ([LHsType Name], TcKind) -- Kind-checked args
 kcApps the_fun fun_kind args

-  = do { (args_w_kinds, res_kind) <- splitFunKind 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)
        ; 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)

-           -> TcKind          -- Expected kind
+           -> ExpKind         -- Expected kind

            -> TcM [LHsType Name]
 kcCheckApps the_fun fun_kind args ty exp_kind
            -> TcM [LHsType Name]
 kcCheckApps the_fun fun_kind args ty exp_kind

-  = do { (args_w_kinds, res_kind) <- splitFunKind the_fun fun_kind args
+  = 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 }
 
        ; 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 }
 

-splitHsAppTys :: LHsType Name -> LHsType Name -> (LHsType Name, [LHsType Name])
-splitHsAppTys fun_ty arg_ty = split fun_ty [arg_ty]
-  where
-    split (L _ (HsAppTy f a)) as = split f (a:as)
-    split f                  as = (f,as)
-
-mkHsAppTys :: LHsType Name -> [LHsType Name] -> HsType Name
-mkHsAppTys fun_ty [] = pprPanic "mkHsAppTys" (ppr fun_ty)
-mkHsAppTys fun_ty (arg_ty:arg_tys)
-  = foldl mk_app (HsAppTy fun_ty arg_ty) arg_tys
-  where
-    mk_app fun arg = HsAppTy (noLoc fun) arg   -- Add noLocs for inner nodes of
-                                               -- the application; they are
-                                               -- never used 

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

-splitFunKind :: Outputable a => a -> TcKind -> [b] -> TcM ([(b,TcKind)], TcKind)
-splitFunKind _       fk [] = return ([], fk)
-splitFunKind the_fun fk (arg:args)
-  = do { mb_fk <- unifyFunKind fk
+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 
        ; case mb_fk of
             Nothing       -> failWithTc too_many_args 

-            Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun fk' args
-                                ; return ((arg,ak):aks, rk) } }
+            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
   where

-    too_many_args = quotes (ppr the_fun) <+>
+    too_many_args = quotes the_fun <+>

                    ptext (sLit "is applied to too many type arguments")
 
 ---------------------------
                    ptext (sLit "is applied to too many type arguments")
 
 ---------------------------

@@ -467,9 +490,9 @@ 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'
     
 ---------------------------
     return pred'
     
 ---------------------------

@@ -478,28 +501,23 @@ kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
        -- application (reason: used from TcDeriv)
 kc_pred (HsIParam name ty)
   = do { (ty', kind) <- kc_lhs_type ty
        -- application (reason: used from TcDeriv)
 kc_pred (HsIParam name ty)
   = do { (ty', kind) <- kc_lhs_type ty

-       ; return (HsIParam name ty', kind)
-       }
+       ; return (HsIParam name ty', kind) }

 kc_pred (HsClassP cls tys)
   = do { kind <- kcClass cls
        ; (tys', res_kind) <- kcApps cls kind tys
 kc_pred (HsClassP cls tys)
   = do { kind <- kcClass cls
        ; (tys', res_kind) <- kcApps cls kind tys

-       ; return (HsClassP cls tys', res_kind)
-       }
+       ; return (HsClassP cls tys', res_kind) }

 kc_pred (HsEqualP ty1 ty2)
   = do { (ty1', kind1) <- kc_lhs_type ty1
 kc_pred (HsEqualP ty1 ty2)
   = do { (ty1', kind1) <- kc_lhs_type ty1

---       ; checkExpectedKind ty1 kind1 liftedTypeKind

        ; (ty2', kind2) <- kc_lhs_type ty2
        ; (ty2', kind2) <- kc_lhs_type ty2

---       ; checkExpectedKind ty2 kind2 liftedTypeKind
-       ; checkExpectedKind ty2 kind2 kind1
-       ; return (HsEqualP ty1' ty2', liftedTypeKind)
-       }
+       ; 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
     case thing of 
         ATyVar _ ty             -> return (typeKind ty)
         AThing kind             -> return kind

@@ -544,9 +562,12 @@ ds_type ty@(HsTyVar _)
 ds_type (HsParTy ty)           -- Remove the parentheses markers
   = dsHsType ty
 
 ds_type (HsParTy ty)           -- Remove the parentheses markers
   = dsHsType ty
 

-ds_type ty@(HsBangTy _ _)      -- No bangs should be here
+ds_type ty@(HsBangTy {})    -- No bangs should be here

   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
 
   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
 

+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 (HsKindSig ty _)
   = dsHsType ty        -- Kind checking done already
 

@@ -560,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

@@ -577,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 []
 

@@ -595,11 +621,16 @@ ds_type (HsForAllTy _ tv_names ctxt ty)
     tau <- dsHsType ty
     return (mkSigmaTy tyvars theta tau)
 
     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 :: [LHsType Name] -> TcM [Type]
 dsHsTypes arg_tys = mapM dsHsType arg_tys
 \end{code}

@@ -653,35 +684,7 @@ 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')
-                       _ -> failWithTc (badGadtDecl res_ty) }
-          _ -> 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 _ tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
-    get_args ty                        args = (ty, args)
-
-badGadtDecl :: HsType Name -> SDoc
-badGadtDecl ty
-  = hang (ptext (sLit "Malformed constructor result type:"))
-       2 (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
 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
        -- Wrap a context around only if we want to show that contexts.  
 addKcTypeCtxt (L _ (HsPredTy _)) thing = thing

@@ -704,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

@@ -723,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]

@@ -836,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 

@@ -847,21 +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
                 [(Name, TcType)], -- The new bit of type environment, binding
                                   -- the scoped type variables
         -> TcM (TcType,           -- The type to use for "inside" the signature
                 [(Name, TcType)], -- The new bit of type environment, binding
                                   -- the scoped type variables

-                 CoercionI)        -- Coercion due to unification with actual ty
+                 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

-                 coi <- boxyUnify sig_ty res_ty
-               ; return (sig_ty, [], coi)
-
-       } 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

@@ -873,48 +878,134 @@ tcPatSig ctxt sig res_ty
                                _              -> False
        ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
 
                                _              -> 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
-       ; coi <- 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, coi)
-       } }
+       -- Phew!
+        ; return (sig_ty', tv_binds, wrap)
+        } }

   where
     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
   where
     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
                -- 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
 %*                                                                     *

@@ -922,7 +1013,7 @@ 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
                                 nest 2 (pp_sig ctxt) ]
   where
     pp_sig (FunSigCtxt n)  = pp_n_colon n

@@ -932,17 +1023,14 @@ pprHsSigCtxt ctxt hs_ty = vcat [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> c
 
     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
 
 
     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
 

-wobblyPatSig :: [Var] -> SDoc
-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 :: Name -> Type -> SDoc
-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"))]
+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' _
 
 dupInScope :: Name -> Name -> Type -> SDoc
 dupInScope n n' _

@@ -950,8 +1038,7 @@ dupInScope n n' _
        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
                ptext (sLit "Distinct scoped type variables must be distinct")])
 
        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
                ptext (sLit "Distinct scoped type variables must be distinct")])
 

-wrongEqualityErr :: TcM (HsType Name, TcKind)
-wrongEqualityErr
-  = failWithTc (text "Equality predicate used as a type")
+wrongPredErr :: HsPred Name -> TcM (HsType Name, TcKind)
+wrongPredErr pred = failWithTc (text "Predicate used as a type:" <+> ppr pred)

 \end{code}
 
 \end{code}