[project @ 2004-09-30 10:35:15 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcHsType.lhs
index 9a73ff3..08effa7 100644 (file)
@@ -5,62 +5,64 @@
 
 \begin{code}
 module TcHsType (
-       tcHsSigType, tcHsPred,
+       tcHsSigType, tcHsDeriv,
        UserTypeCtxt(..), 
 
                -- Kind checking
        kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
-       kcCheckHsType, kcHsContext,
+       kcCheckHsType, kcHsContext, kcHsType, 
        
                -- Typechecking kinded types
-       tcHsKindedContext, tcHsKindedType, tcTyVarBndrs, dsHsType, 
+       tcHsKindedContext, tcHsKindedType, tcHsBangType,
+       tcTyVarBndrs, dsHsType, tcLHsConSig,
 
-       tcAddScopedTyVars, 
+       tcHsPatSigType, tcAddLetBoundTyVars,
        
-       TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
+       TcSigInfo(..), mkTcSig, 
+       TcSigFun, lookupSig 
    ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), HsTyVarBndr(..), HsContext, Sig(..), HsPred(..) )
-import RnHsSyn         ( RenamedHsType, RenamedContext, RenamedSig, extractHsTyVars )
+import HsSyn           ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, HsBang,
+                         LHsContext, HsPred(..), LHsPred, LHsBinds,
+                         getBangStrictness, collectSigTysFromHsBinds )
+import RnHsSyn         ( extractHsTyVars )
 import TcHsSyn         ( TcId )
 
 import TcRnMonad
-import TcEnv           ( tcExtendTyVarEnv, tcExtendTyVarKindEnv,
+import TcEnv           ( tcExtendTyVarEnv, tcExtendKindEnv,
                          tcLookup, tcLookupClass, tcLookupTyCon,
                          TyThing(..), TcTyThing(..), 
-                         getInLocalScope
+                         getInLocalScope, wrongThingErr
                        )
-import TcMType         ( newKindVar, tcInstType, newMutTyVar,
-                         zonkTcType, zonkTcKindToKind,
+import TcMType         ( newKindVar, tcSkolType, newMetaTyVar, 
+                         zonkTcKindToKind, 
                          checkValidType, UserTypeCtxt(..), pprHsSigCtxt
                        )
-import TcUnify         ( unifyKind, unifyFunKind, unifyTypeKind )
-import TcType          ( Type, PredType(..), ThetaType, TyVarDetails(..),
-                         TcTyVar, TcKind, TcThetaType, TcTauType,
-                         mkTyVarTy, mkTyVarTys, mkFunTy, 
+import TcUnify         ( unifyFunKind, checkExpectedKind )
+import TcType          ( Type, PredType(..), ThetaType, 
+                         SkolemInfo(SigSkol), MetaDetails(Flexi),
+                         TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
+                         mkTyVarTy, mkFunTy, 
                          mkForAllTys, mkFunTys, tcEqType, isPredTy,
                          mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, 
-                         liftedTypeKind, unliftedTypeKind, eqKind,
-                         tcSplitFunTy_maybe, tcSplitForAllTys, tcSplitSigmaTy
-                       )
-import PprType         ( pprKind, pprThetaArrow )
-import qualified Type  ( splitFunTys )
-import Inst            ( Inst, InstOrigin(..), newMethod, instToId )
+                         tcSplitFunTy_maybe, tcSplitForAllTys )
+import Kind            ( liftedTypeKind, ubxTupleKind, openTypeKind, argTypeKind )
+import Inst            ( InstOrigin(..) )
 
-import Id              ( mkLocalId, idName, idType )
+import Id              ( idName, idType )
 import Var             ( TyVar, mkTyVar, tyVarKind )
-import ErrUtils                ( Message )
 import TyCon           ( TyCon, tyConKind )
-import Class           ( classTyCon )
+import Class           ( Class, classTyCon )
 import Name            ( Name )
 import NameSet
 import PrelNames       ( genUnitTyConName )
-import Subst           ( deShadowTy )
+import Type            ( deShadowTy )
 import TysWiredIn      ( mkListTy, mkPArrTy, mkTupleTy )
+import Bag             ( bagToList )
 import BasicTypes      ( Boxity(..) )
-import SrcLoc          ( SrcLoc )
+import SrcLoc          ( Located(..), unLoc, noLoc )
 import Outputable
 import List            ( nubBy )
 \end{code}
@@ -149,7 +151,7 @@ the TyCon being defined.
 %************************************************************************
 
 \begin{code}
-tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
+tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
   -- Do kind checking, and hoist for-alls to the top
 tcHsSigType ctxt hs_ty 
   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
@@ -157,13 +159,27 @@ tcHsSigType ctxt hs_ty
        ; ty <- tcHsKindedType kinded_ty
        ; checkValidType ctxt ty        
        ; returnM ty }
-
--- tcHsPred is happy with a partial application, e.g. (ST s)
--- Used from TcDeriv
-tcHsPred pred 
-  = do { (kinded_pred,_) <- kc_pred pred       -- kc_pred rather than kcHsPred
-                                               -- to avoid the partial application check
-       ; dsHsPred kinded_pred }
+-- Used for the deriving(...) items
+tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
+tcHsDeriv = addLocM (tc_hs_deriv [])
+
+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
+       ; tcTyVarBndrs tv_names'        $ \ tyvars ->
+    do { arg_tys <- dsHsTypes tys
+       ; cls <- tcLookupClass cls_name
+       ; return (tyvars, cls, arg_tys) }}
+
+tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
+  =    -- Funny newtype deriving form
+       --      forall a. C [a]
+       -- where C has arity 2.  Hence can't use regular functions
+    tc_hs_deriv (tv_names1 ++ tv_names2) ty
+
+tc_hs_deriv _ other
+  = failWithTc (ptext SLIT("Illegal deriving item") <+> ppr other)
 \end{code}
 
        These functions are used during knot-tying in
@@ -171,12 +187,12 @@ tcHsPred pred
        separate kind-checking, desugaring, and validity checking
 
 \begin{code}
-kcHsSigType, kcHsLiftedSigType :: HsType Name -> TcM (HsType Name)
+kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
        -- Used for type signatures
 kcHsSigType ty              = kcTypeType ty
 kcHsLiftedSigType ty = kcLiftedType ty
 
-tcHsKindedType :: RenamedHsType -> TcM Type
+tcHsKindedType :: LHsType Name -> TcM Type
   -- Don't do kind checking, nor validity checking, 
   --   but do hoist for-alls to the top
   -- This is used in type and class decls, where kinding is
@@ -186,10 +202,15 @@ tcHsKindedType hs_ty
   = do { ty <- dsHsType hs_ty
        ; return (hoistForAllTys ty) }
 
-tcHsKindedContext :: RenamedContext -> TcM ThetaType
+tcHsBangType :: LHsType Name -> TcM Type
+-- Permit a bang, but discard it
+tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
+tcHsBangType ty                      = tcHsKindedType ty
+
+tcHsKindedContext :: LHsContext Name -> TcM ThetaType
 -- Used when we are expecting a ClassContext (i.e. no implicit params)
 -- Does not do validity checking, like tcHsKindedType
-tcHsKindedContext hs_theta = mappM dsHsPred hs_theta
+tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
 \end{code}
 
 
@@ -203,31 +224,33 @@ tcHsKindedContext hs_theta = mappM dsHsPred hs_theta
 
 \begin{code}
 ---------------------------
-kcLiftedType :: HsType Name -> TcM (HsType 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
     
 ---------------------------
-kcTypeType :: HsType Name -> TcM (HsType Name)
-       -- The type ty must be a *type*, but it can be lifted or unlifted
-kcTypeType ty
-  = kcHsType ty                        `thenM` \ (ty', kind) ->
-    unifyTypeKind kind         `thenM_`
-    returnM ty'
+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
 
 ---------------------------
-kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name)
+kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
 -- Check that the type has the specified kind
-kcCheckHsType ty exp_kind
-  = kcHsType ty                                                `thenM` \ (ty', act_kind) ->
-    checkExpectedKind (ppr ty) act_kind exp_kind       `thenM_`
-    returnM ty'
+-- 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                            $
+    kc_hs_type ty                              `thenM` \ (ty', act_kind) ->
+    checkExpectedKind ty act_kind exp_kind     `thenM_`
+    returnM (L span ty')
 \end{code}
 
        Here comes the main function
 
 \begin{code}
-kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
+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
 -- kind as argument as tcExpr does.  
 -- Reasons: 
@@ -238,77 +261,92 @@ kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
 --
 -- The translated type has explicitly-kinded type-variable binders
 
-kcHsType (HsParTy ty)
+kc_hs_type (HsParTy ty)
  = kcHsType ty         `thenM` \ (ty', kind) ->
    returnM (HsParTy ty', kind)
 
-kcHsType (HsTyVar name)
+kc_hs_type (HsTyVar name)
   = kcTyVar name       `thenM` \ kind ->
     returnM (HsTyVar name, kind)
 
-kcHsType (HsListTy ty) 
+kc_hs_type (HsListTy ty) 
   = kcLiftedType ty                    `thenM` \ ty' ->
     returnM (HsListTy ty', liftedTypeKind)
 
-kcHsType (HsPArrTy ty)
+kc_hs_type (HsPArrTy ty)
   = kcLiftedType ty                    `thenM` \ ty' ->
     returnM (HsPArrTy ty', liftedTypeKind)
 
-kcHsType (HsNumTy n)
+kc_hs_type (HsNumTy n)
    = returnM (HsNumTy n, liftedTypeKind)
 
-kcHsType (HsKindSig ty k) 
+kc_hs_type (HsKindSig ty k) 
   = kcCheckHsType ty k `thenM` \ ty' ->
     returnM (HsKindSig ty' k, k)
 
-kcHsType (HsTupleTy Boxed tys)
+kc_hs_type (HsTupleTy Boxed tys)
   = mappM kcLiftedType tys     `thenM` \ tys' ->
     returnM (HsTupleTy Boxed tys', liftedTypeKind)
 
-kcHsType (HsTupleTy Unboxed tys)
+kc_hs_type (HsTupleTy Unboxed tys)
   = mappM kcTypeType tys       `thenM` \ tys' ->
-    returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
+    returnM (HsTupleTy Unboxed tys', ubxTupleKind)
 
-kcHsType (HsFunTy ty1 ty2)
-  = kcTypeType ty1     `thenM` \ ty1' ->
-    kcTypeType ty2     `thenM` \ ty2' ->
+kc_hs_type (HsFunTy ty1 ty2)
+  = kcCheckHsType ty1 argTypeKind      `thenM` \ ty1' ->
+    kcTypeType ty2                     `thenM` \ ty2' ->
     returnM (HsFunTy ty1' ty2', liftedTypeKind)
 
-kcHsType ty@(HsOpTy ty1 op ty2)
-  = kcTyVar op                         `thenM` \ op_kind ->
+kc_hs_type ty@(HsOpTy ty1 op ty2)
+  = addLocM kcTyVar op                 `thenM` \ op_kind ->
     kcApps op_kind (ppr op) [ty1,ty2]  `thenM` \ ([ty1',ty2'], res_kind) ->
     returnM (HsOpTy ty1' op ty2', res_kind)
 
-kcHsType ty@(HsAppTy ty1 ty2)
+kc_hs_type ty@(HsAppTy ty1 ty2)
   = kcHsType fun_ty                      `thenM` \ (fun_ty', fun_kind) ->
-    kcApps fun_kind (ppr fun_ty) arg_tys  `thenM` \ (arg_tys', res_kind) ->
-    returnM (foldl HsAppTy fun_ty' arg_tys', res_kind)
+    kcApps fun_kind (ppr fun_ty) arg_tys  `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
+    returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
   where
     (fun_ty, arg_tys) = split ty1 [ty2]
-    split (HsAppTy f a) as = split f (a:as)
-    split f             as = (f,as)
-
-kcHsType (HsPredTy pred)
+    split (L _ (HsAppTy f a)) as = split f (a:as)
+    split f                  as = (f,as)
+    mk_app fun arg = HsAppTy (noLoc fun) arg   -- Add noLocs for inner nodes of
+                                               -- the application; they are never used
+    
+kc_hs_type (HsPredTy pred)
   = kcHsPred pred              `thenM` \ pred' ->
     returnM (HsPredTy pred', liftedTypeKind)
 
-kcHsType (HsForAllTy (Just tv_names) context ty)
+kc_hs_type (HsForAllTy exp tv_names context ty)
   = kcHsTyVars tv_names                $ \ tv_names' ->
     kcHsContext context                `thenM` \ ctxt' ->
     kcLiftedType ty            `thenM` \ ty' ->
-       -- The body of a forall must be of kind *
-       -- In principle, I suppose, we could allow unlifted types,
-       -- but it seems simpler to stick to lifted types for now.
-    returnM (HsForAllTy (Just tv_names') ctxt' ty', liftedTypeKind)
+       -- The body of a forall is usually a type, but in principle
+       -- there's no reason to prohibit *unlifted* types.
+       -- In fact, GHC can itself construct a function with an
+       -- unboxed tuple inside a for-all (via CPR analyis; see 
+       -- typecheck/should_compile/tc170)
+       --
+       -- Still, that's only for internal interfaces, which aren't
+       -- kind-checked, so we only allow liftedTypeKind here
+    returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
+
+kc_hs_type (HsBangTy b ty)
+  = do { (ty', kind) <- kcHsType ty
+       ; return (HsBangTy b ty', kind) }
+
+kc_hs_type ty@(HsSpliceTy _)
+  = failWithTc (ptext SLIT("Unexpected type splice:") <+> ppr ty)
+
 
 ---------------------------
-kcApps :: TcKind               -- Function kind
-       -> SDoc                 -- Function 
-       -> [HsType Name]                -- Arg types
-       -> TcM ([HsType Name], TcKind)  -- Kind-checked args
+kcApps :: TcKind                       -- Function kind
+       -> SDoc                         -- Function 
+       -> [LHsType Name]               -- Arg types
+       -> TcM ([LHsType Name], TcKind) -- Kind-checked args
 kcApps fun_kind ppr_fun args
   = split_fk fun_kind (length args)    `thenM` \ (arg_kinds, res_kind) ->
-    mappM kc_arg (args `zip` arg_kinds)        `thenM` \ args' ->
+    zipWithM kc_arg args arg_kinds     `thenM` \ args' ->
     returnM (args', res_kind)
   where
     split_fk fk 0 = returnM ([], fk)
@@ -318,18 +356,22 @@ kcApps fun_kind ppr_fun args
                        Just (ak,fk') -> split_fk fk' (n-1)     `thenM` \ (aks, rk) ->
                                         returnM (ak:aks, rk)
 
-    kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
+    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")
 
 ---------------------------
-kcHsContext :: HsContext Name -> TcM (HsContext Name)
-kcHsContext ctxt = mappM kcHsPred ctxt
+kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
+kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt
 
-kcHsPred pred          -- Checks that the result is of kind liftedType
-  = kc_pred pred                       `thenM` \ (pred', kind) ->
-    checkExpectedKind (ppr pred) kind liftedTypeKind   `thenM_` 
+kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
+kcHsLPred = wrapLocM kcHsPred
+
+kcHsPred :: HsPred Name -> TcM (HsPred Name)
+kcHsPred pred  -- Checks that the result is of kind liftedType
+  = kc_pred pred                               `thenM` \ (pred', kind) ->
+    checkExpectedKind pred kind liftedTypeKind `thenM_` 
     returnM pred'
     
 ---------------------------
@@ -348,80 +390,24 @@ kc_pred pred@(HsClassP cls tys)
 ---------------------------
 kcTyVar :: Name -> TcM TcKind
 kcTyVar name   -- Could be a tyvar or a tycon
-  = tcLookup name      `thenM` \ thing ->
+  = traceTc (text "lk1" <+> ppr name)  `thenM_`
+    tcLookup name      `thenM` \ thing ->
+    traceTc (text "lk2" <+> ppr name <+> ppr thing)    `thenM_`
     case thing of 
        ATyVar tv               -> returnM (tyVarKind tv)
-       ARecTyCon kind          -> returnM kind
+       AThing kind             -> returnM kind
        AGlobal (ATyCon tc)     -> returnM (tyConKind tc) 
-       other                   -> failWithTc (wrongThingErr "type" thing name)
+       other                   -> wrongThingErr "type" thing name
 
 kcClass :: Name -> TcM TcKind
 kcClass cls    -- Must be a class
   = tcLookup cls                               `thenM` \ thing -> 
     case thing of
-       ARecClass kind          -> returnM kind
+       AThing kind             -> returnM kind
        AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
-       other                   -> failWithTc (wrongThingErr "class" thing cls)
+       other                   -> wrongThingErr "class" thing cls
 \end{code}
 
-       Helper functions
-
-
-\begin{code}
----------------------------
--- 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
---
-
-
-checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
--- A fancy wrapper for 'unifyKind', which tries to give 
--- decent error messages.
--- Returns the same kind that it is passed, exp_kind
-checkExpectedKind pp_ty act_kind exp_kind
-  | act_kind `eqKind` exp_kind -- Short cut for a very common case
-  = returnM exp_kind   
-  | otherwise
-  = tryTc (unifyKind exp_kind act_kind)        `thenM` \ (errs, mb_r) ->
-    case mb_r of {
-       Just _  -> returnM exp_kind ;   -- Unification succeeded
-       Nothing ->
-
-       -- So there's definitely an error
-       -- Now to find out what sort
-    zonkTcType exp_kind                `thenM` \ exp_kind ->
-    zonkTcType act_kind                `thenM` \ act_kind ->
-
-    let (exp_as, _) = Type.splitFunTys exp_kind
-        (act_as, _) = Type.splitFunTys act_kind
-               -- Use the Type versions for kinds      
-       n_exp_as = length exp_as
-       n_act_as = length act_as
-
-       err | n_exp_as < n_act_as       -- E.g. [Maybe]
-           = quotes pp_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
-           | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
-           = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty 
-               <+> ptext SLIT("is unlifted")
-
-           | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
-           = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty 
-               <+> ptext SLIT("is lifted")
-
-           | otherwise                 -- E.g. Monad [Int]
-           = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
-                   ptext SLIT("but") <+> quotes pp_ty <+> 
-                       ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
-   in
-   failWithTc (ptext SLIT("Kind error:") <+> err) 
-   }
-\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -434,58 +420,63 @@ The type desugarer
        * Transforms from HsType to Type
        * Zonks any kinds
 
-It cannot fail, and does no validity checking
+It cannot fail, and does no validity checking, except for 
+structural matters, such as spurious ! annotations.
 
 \begin{code}
-dsHsType :: HsType Name        -- All HsTyVarBndrs are kind-annotated
-        -> TcM Type
+dsHsType :: LHsType Name -> TcM Type
+-- All HsTyVarBndrs in the intput type are kind-annotated
+dsHsType ty = ds_type (unLoc ty)
 
-dsHsType ty@(HsTyVar name)
+ds_type ty@(HsTyVar name)
   = ds_app ty []
 
-dsHsType (HsParTy ty)          -- Remove the parentheses markers
+ds_type (HsParTy ty)           -- Remove the parentheses markers
   = dsHsType ty
 
-dsHsType (HsKindSig ty k)
+ds_type ty@(HsBangTy _ _)      -- No bangs should be here
+  = failWithTc (ptext SLIT("Unexpected strictness annotation:") <+> ppr ty)
+
+ds_type (HsKindSig ty k)
   = dsHsType ty        -- Kind checking done already
 
-dsHsType (HsListTy ty)
+ds_type (HsListTy ty)
   = dsHsType ty                                `thenM` \ tau_ty ->
     returnM (mkListTy tau_ty)
 
-dsHsType (HsPArrTy ty)
+ds_type (HsPArrTy ty)
   = dsHsType ty                                `thenM` \ tau_ty ->
     returnM (mkPArrTy tau_ty)
 
-dsHsType (HsTupleTy boxity tys)
+ds_type (HsTupleTy boxity tys)
   = dsHsTypes tys                      `thenM` \ tau_tys ->
     returnM (mkTupleTy boxity (length tys) tau_tys)
 
-dsHsType (HsFunTy ty1 ty2)
+ds_type (HsFunTy ty1 ty2)
   = dsHsType ty1                       `thenM` \ tau_ty1 ->
     dsHsType ty2                       `thenM` \ tau_ty2 ->
     returnM (mkFunTy tau_ty1 tau_ty2)
 
-dsHsType (HsOpTy ty1 op ty2)
-  = dsHsType ty1 `thenM` \ tau_ty1 ->
-    dsHsType ty2 `thenM` \ tau_ty2 ->
-    ds_var_app op [tau_ty1,tau_ty2]
+ds_type (HsOpTy ty1 (L span op) ty2)
+  = dsHsType ty1               `thenM` \ tau_ty1 ->
+    dsHsType ty2               `thenM` \ tau_ty2 ->
+    setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
 
-dsHsType (HsNumTy n)
+ds_type (HsNumTy n)
   = ASSERT(n==1)
     tcLookupTyCon genUnitTyConName     `thenM` \ tc ->
     returnM (mkTyConApp tc [])
 
-dsHsType ty@(HsAppTy ty1 ty2) 
-  = ds_app ty1 [ty2]
+ds_type ty@(HsAppTy _ _)
+  = ds_app ty []
 
-dsHsType (HsPredTy pred)
+ds_type (HsPredTy pred)
   = dsHsPred pred      `thenM` \ pred' ->
     returnM (mkPredTy pred')
 
-dsHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
+ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
   = tcTyVarBndrs tv_names              $ \ tyvars ->
-    mappM dsHsPred ctxt                        `thenM` \ theta ->
+    mappM dsHsLPred (unLoc ctxt)       `thenM` \ theta ->
     dsHsType ty                                `thenM` \ tau ->
     returnM (mkSigmaTy tyvars theta tau)
 
@@ -496,15 +487,15 @@ Help functions for type applications
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 \begin{code}
-ds_app :: HsType Name -> [HsType Name] -> TcM Type
+ds_app :: HsType Name -> [LHsType Name] -> TcM Type
 ds_app (HsAppTy ty1 ty2) tys
-  = ds_app ty1 (ty2:tys)
+  = ds_app (unLoc ty1) (ty2:tys)
 
 ds_app ty tys
   = dsHsTypes tys                      `thenM` \ arg_tys ->
     case ty of
        HsTyVar fun -> ds_var_app fun arg_tys
-       other       -> dsHsType ty              `thenM` \ fun_ty ->
+       other       -> ds_type ty               `thenM` \ fun_ty ->
                       returnM (mkAppTys fun_ty arg_tys)
 
 ds_var_app :: Name -> [Type] -> TcM Type
@@ -513,16 +504,19 @@ ds_var_app name arg_tys
     case thing of
        ATyVar tv            -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
        AGlobal (ATyCon tc)  -> returnM (mkGenTyConApp tc arg_tys)
-       ARecTyCon _          -> tcLookupTyCon name      `thenM` \ tc ->
-                               returnM (mkGenTyConApp tc arg_tys)
+--     AThing _             -> tcLookupTyCon name      `thenM` \ tc ->
+--                             returnM (mkGenTyConApp tc arg_tys)
        other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
 \end{code}
 
 
 Contexts
 ~~~~~~~~
+
 \begin{code}
-dsHsPred :: HsPred Name -> TcM PredType
+dsHsLPred :: LHsPred Name -> TcM PredType
+dsHsLPred pred = dsHsPred (unLoc pred)
+
 dsHsPred pred@(HsClassP class_name tys)
   = dsHsTypes tys                      `thenM` \ arg_tys ->
     tcLookupClass class_name           `thenM` \ clas ->
@@ -533,6 +527,59 @@ dsHsPred (HsIParam name ty)
     returnM (IParam name arg_ty)
 \end{code}
 
+GADT constructor signatures
+
+\begin{code}
+tcLHsConSig :: LHsType Name 
+           -> TcM ([TcTyVar], TcThetaType, 
+                   [HsBang], [TcType],
+                   TyCon, [TcType])
+-- Take apart the type signature for a data constructor
+-- The difference is that there can be bangs at the top of
+-- the argument types, and kind-checking is the right place to check
+tcLHsConSig sig@(L span (HsForAllTy exp tv_names ctxt ty))
+  = setSrcSpan span            $
+    addErrCtxt (gadtSigCtxt sig) $
+    tcTyVarBndrs tv_names      $ \ tyvars ->
+    do { theta <- mappM dsHsLPred (unLoc ctxt)
+       ; (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
+       ; return (tyvars, theta, bangs, arg_tys, tc, res_tys) }
+tcLHsConSig ty 
+  = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
+       ; return ([], [], bangs, arg_tys, tc, res_tys) }
+
+--------
+tc_con_sig_tau (L _ (HsFunTy arg ty))
+  = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
+       ; arg_ty <- tcHsBangType arg
+       ; return (getBangStrictness arg : bangs, 
+                 arg_ty : arg_tys, tc, res_tys) }
+
+tc_con_sig_tau ty
+  = do { (tc, res_tys) <- tc_con_res ty []
+       ; return ([], [], tc, res_tys) }
+
+--------
+tc_con_res (L _ (HsAppTy fun res_ty)) res_tys
+  = do { res_ty' <- dsHsType res_ty
+       ; tc_con_res fun (res_ty' : res_tys) }
+
+tc_con_res ty@(L _ (HsTyVar name)) res_tys
+  = do { thing <- tcLookup name
+       ; case thing of
+           AGlobal (ATyCon tc) -> return (tc, res_tys)
+           other -> failWithTc (badGadtDecl ty)
+       }
+
+tc_con_res ty _ = failWithTc (badGadtDecl ty)
+
+gadtSigCtxt ty
+  = hang (ptext SLIT("In the signature of a data constructor:"))
+       2 (ppr ty)
+badGadtDecl ty
+  = hang (ptext SLIT("Malformed constructor signature:"))
+       2 (ppr ty)
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -542,14 +589,14 @@ dsHsPred (HsIParam name ty)
 
 
 \begin{code}
-kcHsTyVars :: [HsTyVarBndr Name] 
-          -> ([HsTyVarBndr Name] -> TcM r)     -- These binders are kind-annotated
+kcHsTyVars :: [LHsTyVarBndr Name] 
+          -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
                                                -- They scope over the thing inside
           -> TcM r
 kcHsTyVars tvs thing_inside 
-  = mappM kcHsTyVar tvs                `thenM` \ bndrs ->
-    tcExtendTyVarKindEnv bndrs         $
-    thing_inside bndrs
+  = mappM (wrapLocM kcHsTyVar) tvs     `thenM` \ bndrs ->
+    tcExtendKindEnv [(n,k) | L _ (KindedTyVar n k) <- bndrs]
+                   (thing_inside bndrs)
 
 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
        -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it      
@@ -558,18 +605,18 @@ kcHsTyVar (UserTyVar name)        = newKindVar    `thenM` \ kind ->
 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
 
 ------------------
-tcTyVarBndrs :: [HsTyVarBndr Name]     -- Kind-annotated binders, which need kind-zonking
+tcTyVarBndrs :: [LHsTyVarBndr Name]    -- Kind-annotated binders, which need kind-zonking
             -> ([TyVar] -> TcM r)
             -> TcM r
 -- Used when type-checking types/classes/type-decls
 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
 tcTyVarBndrs bndrs thing_inside
-  = mapM zonk bndrs    `thenM` \ tyvars ->
+  = mapM (zonk . unLoc) bndrs  `thenM` \ tyvars ->
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
   where
     zonk (KindedTyVar name kind) = zonkTcKindToKind kind       `thenM` \ kind' ->
                                   returnM (mkTyVar name kind')
-    zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
+    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
                            returnM (mkTyVar name liftedTypeKind)
 \end{code}
 
@@ -614,44 +661,72 @@ Historical note:
           it with expected_ty afterwards
 
 \begin{code}
-tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
-tcAddScopedTyVars [] thing_inside
-  = thing_inside       -- Quick get-out for the empty case
-
-tcAddScopedTyVars sig_tys thing_inside
-  = getInLocalScope                    `thenM` \ in_scope ->
-    let
-       sig_tvs = [ UserTyVar n | ty <- sig_tys,
-                                 n <- nameSetToList (extractHsTyVars ty),
-                                 not (in_scope n) ]
-       -- The tyvars we want are the free type variables of 
-       -- the type that are not already in scope
-    in       
+tcPatSigBndrs :: LHsType Name
+             -> TcM ([TcTyVar],        -- Brought into scope
+                     LHsType Name)     -- Kinded, but not yet desugared
+
+tcPatSigBndrs hs_ty
+  = do { in_scope <- getInLocalScope
+       ; span <- getSrcSpanM
+       ; let sig_tvs = [ L span (UserTyVar n) 
+                       | n <- nameSetToList (extractHsTyVars hs_ty),
+                         not (in_scope n) ]
+               -- The tyvars we want are the free type variables of 
+               -- the type that are not already in scope
+
        -- Behave like kcHsType on a ForAll type
        -- i.e. make kinded tyvars with mutable kinds, 
        --      and kind-check the enclosed types
-    kcHsTyVars sig_tvs (\ kinded_tvs -> do
-                           { mappM kcTypeType sig_tys
-                           ; return kinded_tvs })      `thenM` \ kinded_tvs ->
+       ; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
+                                   { kinded_ty <- kcTypeType hs_ty
+                                   ; return (kinded_tvs, kinded_ty) }
 
        -- Zonk the mutable kinds and bring the tyvars into scope
-       -- Rather like tcTyVarBndrs, except that it brings *mutable* 
-       -- tyvars into scope, not immutable ones
+       -- Just like the call to tcTyVarBndrs in ds_type (HsForAllTy case), 
+       -- except that it brings *meta* tyvars into scope, not regular ones
        --
+       --      [Out of date, but perhaps should be resurrected]
        -- Furthermore, the tyvars are PatSigTvs, which means that we get better
        -- error messages when type variables escape:
        --      Inferred type is less polymorphic than expected
        --      Quantified type variable `t' escapes
        --      It is mentioned in the environment:
        --      t is bound by the pattern type signature at tcfail103.hs:6
-    mapM zonk kinded_tvs       `thenM` \ tyvars ->
-    tcExtendTyVarEnv tyvars thing_inside
-
+       ; tyvars <- mapM (zonk . unLoc) kinded_tvs
+       ; return (tyvars, kinded_ty) }
   where
     zonk (KindedTyVar name kind) = zonkTcKindToKind kind       `thenM` \ kind' ->
-                                  newMutTyVar name kind' PatSigTv
-    zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
+                                  newMetaTyVar name kind' Flexi
+       -- Scoped type variables are bound to a *type*, hence Flexi
+    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
                            returnM (mkTyVar name liftedTypeKind)
+
+tcHsPatSigType :: UserTypeCtxt
+              -> LHsType Name          -- The type signature
+              -> TcM ([TcTyVar],       -- Newly in-scope type variables
+                       TcType)         -- The signature
+
+tcHsPatSigType ctxt hs_ty 
+  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
+    do { (tyvars, kinded_ty) <- tcPatSigBndrs hs_ty
+
+        -- Complete processing of the type, and check its validity
+       ; tcExtendTyVarEnv tyvars $ do
+               { sig_ty <- tcHsKindedType kinded_ty    
+               ; checkValidType ctxt sig_ty 
+               ; return (tyvars, sig_ty) }
+       }
+
+tcAddLetBoundTyVars :: LHsBinds Name -> TcM a -> TcM a
+-- Turgid funciton, used for type variables bound by the patterns of a let binding
+
+tcAddLetBoundTyVars binds thing_inside
+  = go (collectSigTysFromHsBinds (bagToList binds)) thing_inside
+  where
+    go [] thing_inside = thing_inside
+    go (hs_ty:hs_tys) thing_inside
+       = do { (tyvars, _kinded_ty) <- tcPatSigBndrs hs_ty
+            ; tcExtendTyVarEnv tyvars (go hs_tys thing_inside) }
 \end{code}
 
 
@@ -672,50 +747,25 @@ been instantiated.
 
 \begin{code}
 data TcSigInfo
-  = TySigInfo      
-       TcId                    -- *Polymorphic* binder for this value...
-                               -- Has name = N
-
-       [TcTyVar]               -- tyvars
-       TcThetaType             -- theta
-       TcTauType               -- tau
+  = TcSigInfo {
+       sig_id :: TcId,             -- *Polymorphic* binder for this value...
+       sig_tvs   :: [TcTyVar],     -- tyvars
+       sig_theta :: TcThetaType,   -- theta
+       sig_tau   :: TcTauType,     -- tau
+       sig_loc :: InstLoc          -- The location of the signature
+    }
 
-       TcId                    -- *Monomorphic* binder for this value
-                               -- Does *not* have name = N
-                               -- Has type tau
-
-       [Inst]                  -- Empty if theta is null, or
-                               -- (method mono_id) otherwise
-
-       SrcLoc                  -- Of the signature
+type TcSigFun = Name -> Maybe TcSigInfo
 
 instance Outputable TcSigInfo where
-    ppr (TySigInfo id tyvars theta tau _ inst loc) =
-       ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
+    ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
+       = ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
 
-tcSigPolyId :: TcSigInfo -> TcId
-tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
-
-tcSigMonoId :: TcSigInfo -> TcId
-tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
-
-maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
-       -- Search for a particular signature
-maybeSig [] name = Nothing
-maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
-  | name == idName sig_id = Just sig
-  | otherwise            = maybeSig sigs name
-\end{code}
-
-
-\begin{code}
-tcTySig :: RenamedSig -> TcM TcSigInfo
-
-tcTySig (Sig v ty src_loc)
- = addSrcLoc src_loc                   $ 
-   tcHsSigType (FunSigCtxt v) ty       `thenM` \ sigma_tc_ty ->
-   mkTcSig (mkLocalId v sigma_tc_ty)   `thenM` \ sig -> 
-   returnM sig
+lookupSig :: [TcSigInfo] -> TcSigFun   -- Search for a particular signature
+lookupSig [] name = Nothing
+lookupSig (sig : sigs) name
+  | name == idName (sig_id sig) = Just sig
+  | otherwise                  = lookupSig sigs name
 
 mkTcSig :: TcId -> TcM TcSigInfo
 mkTcSig poly_id
@@ -726,18 +776,11 @@ mkTcSig poly_id
        -- the tyvars *do* get unified with something, we want to carry on
        -- typechecking the rest of the program with the function bound
        -- to a pristine type, namely sigma_tc_ty
-   tcInstType SigTv (idType poly_id)           `thenM` \ (tyvars', theta', tau') ->
-
-   getInstLoc SignatureOrigin                  `thenM` \ inst_loc ->
-   newMethod inst_loc poly_id
-            (mkTyVarTys tyvars')
-            theta' tau'                        `thenM` \ inst ->
-       -- We make a Method even if it's not overloaded; no harm
-       -- But do not extend the LIE!  We're just making an Id.
-       
-   getSrcLocM                                  `thenM` \ src_loc ->
-   returnM (TySigInfo poly_id tyvars' theta' tau' 
-                         (instToId inst) [inst] src_loc)
+    do { let rigid_info = SigSkol (idName poly_id)
+       ; (tyvars', theta', tau') <- tcSkolType rigid_info (idType poly_id)
+       ; loc <- getInstLoc (SigOrigin rigid_info)
+       ; return (TcSigInfo { sig_id = poly_id, sig_tvs = tyvars', 
+                             sig_theta = theta', sig_tau = tau', sig_loc = loc }) }
 \end{code}
 
 
@@ -801,23 +844,3 @@ hoistForAllTys ty
        | otherwise = ([], [], ty)
 \end{code}
 
-
-%************************************************************************
-%*                                                                     *
-\subsection{Errors and contexts}
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
-wrongThingErr expected thing name
-  = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
-  where
-    pp_thing (AGlobal (ATyCon _))   = ptext SLIT("Type constructor")
-    pp_thing (AGlobal (AClass _))   = ptext SLIT("Class")
-    pp_thing (AGlobal (AnId   _))   = ptext SLIT("Identifier")
-    pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
-    pp_thing (ATyVar _)            = ptext SLIT("Type variable")
-    pp_thing (ATcId _ _ _)         = ptext SLIT("Local identifier")
-    pp_thing (ARecTyCon _)         = ptext SLIT("Rec tycon")
-    pp_thing (ARecClass _)         = ptext SLIT("Rec class")
-\end{code}