path: root/ghc/compiler/typecheck/TcHsType.lhs

% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section[TcMonoType]{Typechecking user-specified @MonoTypes@}

\begin{code}
module TcHsType (
	tcHsSigType, tcHsDeriv,
	UserTypeCtxt(..), 

		-- Kind checking
	kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
	kcCheckHsType, kcHsContext, kcHsType, 
	
		-- Typechecking kinded types
	tcHsKindedContext, tcHsKindedType, tcHsBangType,
	tcTyVarBndrs, dsHsType, tcLHsConResTy,
	tcDataKindSig,

		-- Pattern type signatures
	tcHsPatSigType, tcPatSig
   ) where

#include "HsVersions.h"

import HsSyn		( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, 
			  LHsContext, HsPred(..), LHsPred, HsExplicitForAll(..) )
import RnHsSyn		( extractHsTyVars )
import TcRnMonad
import TcEnv		( tcExtendTyVarEnv, tcExtendKindEnvTvs, 
			  tcLookup, tcLookupClass, tcLookupTyCon,
		 	  TyThing(..), getInLocalScope, getScopedTyVarBinds,
			  wrongThingErr
			)
import TcMType		( newKindVar, 
			  zonkTcKindToKind, 
			  tcInstBoxyTyVar, readFilledBox,
			  checkValidType
			)
import TcUnify		( boxyUnify, unifyFunKind, checkExpectedKind )
import TcIface		( checkWiredInTyCon )
import TcType		( Type, PredType(..), ThetaType, BoxySigmaType,
			  TcType, TcKind, isRigidTy,
			  UserTypeCtxt(..), pprUserTypeCtxt,
			  substTyWith, mkTyVarTys, tcEqType,
		 	  tcIsTyVarTy, mkFunTy, mkSigmaTy, mkPredTy, 
			  mkTyConApp, mkAppTys, typeKind )
import Kind 		( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, 
			  openTypeKind, argTypeKind, splitKindFunTys )
import Var		( TyVar, mkTyVar, tyVarName )
import TyCon		( TyCon, tyConKind )
import Class		( Class, classTyCon )
import Name		( Name, mkInternalName )
import OccName		( mkOccName, tvName )
import NameSet
import PrelNames	( genUnitTyConName )
import TysWiredIn	( mkListTy, listTyCon, mkPArrTy, parrTyCon, tupleTyCon )
import BasicTypes	( Boxity(..) )
import SrcLoc		( Located(..), unLoc, noLoc, getLoc, srcSpanStart )
import UniqSupply	( uniqsFromSupply )
import Outputable
\end{code}


	----------------------------
		General notes
	----------------------------

Generally speaking we now type-check types in three phases

  1.  kcHsType: kind check the HsType
	*includes* performing any TH type splices;
	so it returns a translated, and kind-annotated, type

  2.  dsHsType: convert from HsType to Type:
	perform zonking
	expand type synonyms [mkGenTyApps]
	hoist the foralls [tcHsType]

  3.  checkValidType: check the validity of the resulting type

Often these steps are done one after the other (tcHsSigType).
But in mutually recursive groups of type and class decls we do
	1 kind-check the whole group
	2 build TyCons/Classes in a knot-tied way
	3 check the validity of types in the now-unknotted TyCons/Classes

For example, when we find
	(forall a m. m a -> m a)
we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
an environment that binds a and m suitably.

The kind checker passed to tcHsTyVars needs to look at enough to
establish the kind of the tyvar:
  * For a group of type and class decls, it's just the group, not
	the rest of the program
  * For a tyvar bound in a pattern type signature, its the types
	mentioned in the other type signatures in that bunch of patterns
  * For a tyvar bound in a RULE, it's the type signatures on other
	universally quantified variables in the rule

Note that this may occasionally give surprising results.  For example:

	data T a b = MkT (a b)

Here we deduce			a::*->*,       b::*
But equally valid would be	a::(*->*)-> *, b::*->*


Validity checking
~~~~~~~~~~~~~~~~~
Some of the validity check could in principle be done by the kind checker, 
but not all:

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
  e.g. 	type T k = k Int
	type S a = a
  Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
  and then S is saturated.  This is a GHC extension.

- Similarly, also a GHC extension, we look through synonyms before complaining
  about the form of a class or instance declaration

- Ambiguity checks involve functional dependencies, and it's easier to wait
  until knots have been resolved before poking into them

Also, in a mutually recursive group of types, we can't look at the TyCon until we've
finished building the loop.  So to keep things simple, we postpone most validity
checking until step (3).

Knot tying
~~~~~~~~~~
During step (1) we might fault in a TyCon defined in another module, and it might
(via a loop) refer back to a TyCon defined in this module. So when we tie a big
knot around type declarations with ARecThing, so that the fault-in code can get
the TyCon being defined.


%************************************************************************
%*									*
\subsection{Checking types}
%*									*
%************************************************************************

\begin{code}
tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
  -- Do kind checking, and hoist for-alls to the top
  -- NB: it's important that the foralls that come from the top-level
  --	 HsForAllTy in hs_ty occur *first* in the returned type.
  --     See Note [Scoped] with TcSigInfo
tcHsSigType ctxt hs_ty 
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
    do	{ kinded_ty <- kcTypeType hs_ty
	; ty <- tcHsKindedType kinded_ty
	; checkValidType ctxt ty	
	; returnM ty }

-- 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
	type and class declarations, when we have to
 	separate kind-checking, desugaring, and validity checking

\begin{code}
kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
	-- Used for type signatures
kcHsSigType ty 	     = kcTypeType ty
kcHsLiftedSigType ty = kcLiftedType ty

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
  -- done in advance, and validity checking is done later
  -- [Validity checking done later because of knot-tying issues.]
tcHsKindedType hs_ty = dsHsType hs_ty

tcHsBangType :: LHsType Name -> TcM Type
-- Permit a bang, but discard it
tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
tcHsBangType ty 		      = tcHsKindedType ty

tcHsKindedContext :: LHsContext Name -> TcM ThetaType
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsKindedType
tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
\end{code}


%************************************************************************
%*									*
		The main kind checker: kcHsType
%*									*
%************************************************************************
	
	First a couple of simple wrappers for kcHsType

\begin{code}
---------------------------
kcLiftedType :: LHsType Name -> TcM (LHsType Name)
-- The type ty must be a *lifted* *type*
kcLiftedType ty = kcCheckHsType ty liftedTypeKind
    
---------------------------
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 :: LHsType Name -> TcKind -> TcM (LHsType Name)
-- Check that the type has the specified kind
-- Be sure to use checkExpectedKind, rather than simply unifying 
-- with OpenTypeKind, because it gives better error messages
kcCheckHsType (L span ty) exp_kind 
  = setSrcSpan span				$
    do	{ (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
		-- Add the context round the inner check only
		-- because checkExpectedKind already mentions
		-- 'ty' by name in any error message

	; checkExpectedKind ty act_kind exp_kind
	; return (L span ty') }
  where
	-- Wrap a context around only if we want to
	-- show that contexts.  Omit invisble ones
	-- and ones user's won't grok (HsPred p).
    add_ctxt (HsPredTy p)		    	   thing = thing
    add_ctxt (HsForAllTy Implicit tvs (L _ []) ty) thing = thing
    add_ctxt other_ty thing = addErrCtxt (typeCtxt ty) thing
\end{code}

	Here comes the main function

\begin{code}
kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
kcHsType ty = wrapLocFstM kc_hs_type ty
-- kcHsType *returns* the kind of the type, rather than taking an expected
-- kind as argument as tcExpr does.  
-- Reasons: 
--	(a) the kind of (->) is
--		forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
--  	    so we'd need to generate huge numbers of bx variables.
--	(b) kinds are so simple that the error messages are fine
--
-- The translated type has explicitly-kinded type-variable binders

kc_hs_type (HsParTy ty)
 = kcHsType ty		`thenM` \ (ty', kind) ->
   returnM (HsParTy ty', kind)

kc_hs_type (HsTyVar name)
  = kcTyVar name	`thenM` \ kind ->
    returnM (HsTyVar name, kind)

kc_hs_type (HsListTy ty) 
  = kcLiftedType ty			`thenM` \ ty' ->
    returnM (HsListTy ty', liftedTypeKind)

kc_hs_type (HsPArrTy ty)
  = kcLiftedType ty			`thenM` \ ty' ->
    returnM (HsPArrTy ty', liftedTypeKind)

kc_hs_type (HsNumTy n)
   = returnM (HsNumTy n, liftedTypeKind)

kc_hs_type (HsKindSig ty k) 
  = kcCheckHsType ty k	`thenM` \ ty' ->
    returnM (HsKindSig ty' k, k)

kc_hs_type (HsTupleTy Boxed tys)
  = mappM kcLiftedType tys	`thenM` \ tys' ->
    returnM (HsTupleTy Boxed tys', liftedTypeKind)

kc_hs_type (HsTupleTy Unboxed tys)
  = mappM kcTypeType tys	`thenM` \ tys' ->
    returnM (HsTupleTy Unboxed tys', ubxTupleKind)

kc_hs_type (HsFunTy ty1 ty2)
  = kcCheckHsType ty1 argTypeKind	`thenM` \ ty1' ->
    kcTypeType ty2			`thenM` \ ty2' ->
    returnM (HsFunTy ty1' ty2', liftedTypeKind)

kc_hs_type ty@(HsOpTy ty1 op ty2)
  = addLocM kcTyVar op			`thenM` \ op_kind ->
    kcApps op_kind (ppr op) [ty1,ty2]	`thenM` \ ([ty1',ty2'], res_kind) ->
    returnM (HsOpTy ty1' op ty2', res_kind)

kc_hs_type ty@(HsAppTy ty1 ty2)
  = kcHsType fun_ty			  `thenM` \ (fun_ty', fun_kind) ->
    kcApps fun_kind (ppr fun_ty) arg_tys  `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
    returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
  where
    (fun_ty, arg_tys) = split ty1 [ty2]
    split (L _ (HsAppTy f a)) as = split f (a:as)
    split f       	      as = (f,as)
    mk_app fun arg = HsAppTy (noLoc fun) arg	-- Add noLocs for inner nodes of
						-- the application; they are never used
    
kc_hs_type (HsPredTy pred)
  = kcHsPred pred		`thenM` \ pred' ->
    returnM (HsPredTy pred', liftedTypeKind)

kc_hs_type (HsForAllTy exp tv_names context ty)
  = kcHsTyVars tv_names		$ \ tv_names' ->
    kcHsContext context		`thenM`	\ ctxt' ->
    kcLiftedType ty		`thenM` \ ty' ->
	-- The body of a forall is usually a type, but in principle
	-- there's no reason to prohibit *unlifted* types.
	-- In fact, GHC can itself construct a function with an
	-- unboxed tuple inside a for-all (via CPR analyis; see 
	-- typecheck/should_compile/tc170)
	--
	-- Still, that's only for internal interfaces, which aren't
	-- kind-checked, so we only allow liftedTypeKind here
    returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)

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 
       -> [LHsType Name]		-- Arg types
       -> TcM ([LHsType Name], TcKind)	-- Kind-checked args
kcApps fun_kind ppr_fun args
  = split_fk fun_kind (length args)	`thenM` \ (arg_kinds, res_kind) ->
    zipWithM kc_arg args arg_kinds	`thenM` \ args' ->
    returnM (args', res_kind)
  where
    split_fk fk 0 = returnM ([], fk)
    split_fk fk n = unifyFunKind fk	`thenM` \ mb_fk ->
		    case mb_fk of 
			Nothing       -> failWithTc too_many_args 
			Just (ak,fk') -> split_fk fk' (n-1)	`thenM` \ (aks, rk) ->
					 returnM (ak:aks, rk)

    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 :: LHsContext Name -> TcM (LHsContext Name)
kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt

kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
kcHsLPred = wrapLocM kcHsPred

kcHsPred :: HsPred Name -> TcM (HsPred Name)
kcHsPred pred	-- Checks that the result is of kind liftedType
  = kc_pred pred				`thenM` \ (pred', kind) ->
    checkExpectedKind pred kind liftedTypeKind	`thenM_` 
    returnM pred'
    
---------------------------
kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)	
	-- Does *not* check for a saturated
	-- application (reason: used from TcDeriv)
kc_pred pred@(HsIParam name ty)
  = kcHsType ty		`thenM` \ (ty', kind) ->
    returnM (HsIParam name ty', kind)

kc_pred pred@(HsClassP cls tys)
  = kcClass cls			`thenM` \ kind ->
    kcApps kind (ppr cls) tys	`thenM` \ (tys', res_kind) ->
    returnM (HsClassP cls tys', res_kind)

---------------------------
kcTyVar :: Name -> TcM TcKind
kcTyVar name	-- Could be a tyvar or a tycon
  = traceTc (text "lk1" <+> ppr name) 	`thenM_`
    tcLookup name	`thenM` \ thing ->
    traceTc (text "lk2" <+> ppr name <+> ppr thing) 	`thenM_`
    case thing of 
	ATyVar _ ty	    	-> returnM (typeKind ty)
	AThing kind		-> returnM kind
	AGlobal (ATyCon tc) 	-> returnM (tyConKind tc) 
	other			-> wrongThingErr "type" thing name

kcClass :: Name -> TcM TcKind
kcClass cls	-- Must be a class
  = tcLookup cls 				`thenM` \ thing -> 
    case thing of
	AThing kind		-> returnM kind
	AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
	other		        -> wrongThingErr "class" thing cls
\end{code}


%************************************************************************
%*									*
		Desugaring
%*									*
%************************************************************************

The type desugarer

	* Transforms from HsType to Type
	* Zonks any kinds

It cannot fail, and does no validity checking, except for 
structural matters, such as
	(a) spurious ! annotations.
	(b) a class used as a type

\begin{code}
dsHsType :: LHsType Name -> TcM Type
-- All HsTyVarBndrs in the intput type are kind-annotated
dsHsType ty = ds_type (unLoc ty)

ds_type ty@(HsTyVar name)
  = ds_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 (HsKindSig ty k)
  = dsHsType ty	-- Kind checking done already

ds_type (HsListTy ty)
  = dsHsType ty			`thenM` \ tau_ty ->
    checkWiredInTyCon listTyCon	`thenM_`
    returnM (mkListTy tau_ty)

ds_type (HsPArrTy ty)
  = dsHsType ty			`thenM` \ tau_ty ->
    checkWiredInTyCon parrTyCon	`thenM_`
    returnM (mkPArrTy tau_ty)

ds_type (HsTupleTy boxity tys)
  = dsHsTypes tys		`thenM` \ tau_tys ->
    checkWiredInTyCon tycon	`thenM_`
    returnM (mkTyConApp tycon tau_tys)
  where
    tycon = tupleTyCon boxity (length tys)

ds_type (HsFunTy ty1 ty2)
  = dsHsType ty1			`thenM` \ tau_ty1 ->
    dsHsType ty2			`thenM` \ tau_ty2 ->
    returnM (mkFunTy tau_ty1 tau_ty2)

ds_type (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])

ds_type (HsNumTy n)
  = ASSERT(n==1)
    tcLookupTyCon genUnitTyConName	`thenM` \ tc ->
    returnM (mkTyConApp tc [])

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

ds_type (HsPredTy pred)
  = dsHsPred pred	`thenM` \ pred' ->
    returnM (mkPredTy pred')

ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
  = tcTyVarBndrs tv_names		$ \ tyvars ->
    mappM dsHsLPred (unLoc ctxt)	`thenM` \ theta ->
    dsHsType ty				`thenM` \ tau ->
    returnM (mkSigmaTy tyvars theta tau)

dsHsTypes arg_tys = mappM dsHsType arg_tys
\end{code}

Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

\begin{code}
ds_app :: HsType Name -> [LHsType Name] -> TcM Type
ds_app (HsAppTy ty1 ty2) tys
  = ds_app (unLoc ty1) (ty2:tys)

ds_app ty tys
  = dsHsTypes tys			`thenM` \ arg_tys ->
    case ty of
	HsTyVar fun -> ds_var_app fun arg_tys
	other	    -> ds_type ty		`thenM` \ fun_ty ->
		       returnM (mkAppTys fun_ty arg_tys)

ds_var_app :: Name -> [Type] -> TcM Type
ds_var_app name arg_tys 
 = tcLookup name			`thenM` \ thing ->
    case thing of
	ATyVar _ ty 	    -> returnM (mkAppTys ty arg_tys)
	AGlobal (ATyCon tc) -> returnM (mkTyConApp tc arg_tys)
	other		    -> wrongThingErr "type" thing name
\end{code}


Contexts
~~~~~~~~

\begin{code}
dsHsLPred :: LHsPred Name -> TcM PredType
dsHsLPred pred = dsHsPred (unLoc pred)

dsHsPred pred@(HsClassP class_name tys)
  = dsHsTypes tys			`thenM` \ arg_tys ->
    tcLookupClass class_name		`thenM` \ clas ->
    returnM (ClassP clas arg_tys)

dsHsPred (HsIParam name ty)
  = dsHsType ty					`thenM` \ arg_ty ->
    returnM (IParam name arg_ty)
\end{code}

GADT constructor signatures

\begin{code}
tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
tcLHsConResTy ty@(L span _) 
  = setSrcSpan span $ 
    addErrCtxt (gadtResCtxt ty) $
    tc_con_res ty []

tc_con_res (L _ (HsAppTy fun res_ty)) res_tys
  = do	{ res_ty' <- dsHsType res_ty
	; tc_con_res fun (res_ty' : res_tys) }

tc_con_res ty@(L _ (HsTyVar name)) res_tys
  = do	{ thing <- tcLookup name
	; case thing of
	    AGlobal (ATyCon tc) -> return (tc, res_tys)
	    other -> failWithTc (badGadtDecl ty)
	}

tc_con_res ty _ = failWithTc (badGadtDecl ty)

gadtResCtxt ty
  = hang (ptext SLIT("In the result type of a data constructor:"))
       2 (ppr ty)
badGadtDecl ty
  = hang (ptext SLIT("Malformed constructor result type:"))
       2 (ppr ty)

typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
\end{code}

%************************************************************************
%*									*
		Type-variable binders
%*									*
%************************************************************************


\begin{code}
kcHsTyVars :: [LHsTyVarBndr Name] 
	   -> ([LHsTyVarBndr Name] -> TcM r) 	-- These binders are kind-annotated
						-- They scope over the thing inside
	   -> TcM r
kcHsTyVars tvs thing_inside 
  = mappM (wrapLocM kcHsTyVar) tvs	`thenM` \ bndrs ->
    tcExtendKindEnvTvs bndrs (thing_inside bndrs)

kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
	-- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it	
kcHsTyVar (UserTyVar name)        = newKindVar 	`thenM` \ kind ->
				    returnM (KindedTyVar name kind)
kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)

------------------
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 . unLoc) bndrs	`thenM` \ tyvars ->
    tcExtendTyVarEnv tyvars (thing_inside tyvars)
  where
    zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
				      ; return (mkTyVar name kind') }
    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
			    return (mkTyVar name liftedTypeKind)

-----------------------------------
tcDataKindSig :: Maybe Kind -> TcM [TyVar]
-- GADT decls can have a (perhpas partial) kind signature
--	e.g.  data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for 
-- the argument kinds, and checks that the result kind is indeed *
tcDataKindSig Nothing = return []
tcDataKindSig (Just kind)
  = do	{ checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
	; span <- getSrcSpanM
	; us   <- newUniqueSupply 
	; let loc   = srcSpanStart span
	      uniqs = uniqsFromSupply us
	; return [ mk_tv loc uniq str kind 
		 | ((kind, str), uniq) <- arg_kinds `zip` names `zip` uniqs ] }
  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

    names :: [String]	-- a,b,c...aa,ab,ac etc
    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"))
	2 (ppr kind)
\end{code}


%************************************************************************
%*									*
		Scoped type variables
%*									*
%************************************************************************


tcAddScopedTyVars is used for scoped type variables added by pattern
type signatures
	e.g.  \ ((x::a), (y::a)) -> x+y
They never have explicit kinds (because this is source-code only)
They are mutable (because they can get bound to a more specific type).

Usually we kind-infer and expand type splices, and then
tupecheck/desugar the type.  That doesn't work well for scoped type
variables, because they scope left-right in patterns.  (e.g. in the
example above, the 'a' in (y::a) is bound by the 'a' in (x::a).

The current not-very-good plan is to
  * find all the types in the patterns
  * find their free tyvars
  * do kind inference
  * bring the kinded type vars into scope
  * BUT throw away the kind-checked type
  	(we'll kind-check it again when we type-check the pattern)

This is bad because throwing away the kind checked type throws away
its splices.  But too bad for now.  [July 03]

Historical note:
    We no longer specify that these type variables must be univerally 
    quantified (lots of email on the subject).  If you want to put that 
    back in, you need to
	a) Do a checkSigTyVars after thing_inside
	b) More insidiously, don't pass in expected_ty, else
	   we unify with it too early and checkSigTyVars barfs
	   Instead you have to pass in a fresh ty var, and unify
	   it with expected_ty afterwards

\begin{code}
tcHsPatSigType :: UserTypeCtxt
	       -> LHsType Name 		-- The type signature
	       -> TcM ([TyVar], 	-- Newly in-scope type variables
			Type)		-- The signature
-- Used for type-checking type signatures in
-- (a) patterns 	  e.g  f (x::Int) = e
-- (b) result signatures  e.g. g x :: Int = e
-- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x

tcHsPatSigType ctxt hs_ty 
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
    do	{ 	-- Find the type variables that are mentioned in the type
		-- but not already in scope.  These are the ones that
		-- should be bound by the pattern signature
 	  in_scope <- getInLocalScope
	; let span = getLoc hs_ty
	      sig_tvs = [ L span (UserTyVar n) 
			| n <- nameSetToList (extractHsTyVars hs_ty),
			  not (in_scope n) ]

	-- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
	-- except that we want to keep the tvs separate
	; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
				    { kinded_ty <- kcTypeType hs_ty
				    ; return (kinded_tvs, kinded_ty) }
	; tcTyVarBndrs kinded_tvs $ \ tyvars -> do
	{ sig_ty <- dsHsType kinded_ty
	; checkValidType ctxt sig_ty 
	; return (tyvars, sig_ty)
      } }

tcPatSig :: UserTypeCtxt
	 -> LHsType Name
	 -> BoxySigmaType
	 -> TcM (TcType,	   -- The type to use for "inside" the signature
		 [(Name,TcType)])  -- The new bit of type environment, binding
				   -- the scoped type variables
tcPatSig ctxt sig res_ty
  = do	{ (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig

	; 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 {
		-- Type signature binds at least one scoped type variable
	
		-- A pattern binding cannot bind scoped type variables
		-- The renamer fails with a name-out-of-scope error 
		-- if a pattern binding tries to bind a type variable,
		-- So we just have an ASSERT here
	; let in_pat_bind = case ctxt of
				BindPatSigCtxt -> True
				other	       -> False
	; ASSERT( not in_pat_bind || null sig_tvs ) return ()

	  	-- Check that pat_ty is rigid
	; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)

		-- Now match the pattern signature against res_ty
		-- For convenience, and uniform-looking error messages
		-- we do the matching by allocating meta type variables, 
		-- unifying, and reading out the results.
		-- This is a strictly local operation.
	; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
	; boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) res_ty
	; sig_tv_tys <- mapM readFilledBox box_tvs

		-- Check that each is bound to a distinct type variable,
		-- and one that is not already in scope
	; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
	; binds_in_scope <- getScopedTyVarBinds
	; check binds_in_scope tv_binds
	
		-- Phew!
	; return (res_ty, tv_binds)
	} }
  where
    check in_scope []		 = 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)
		-- Must not bind to the same type variable
		-- as some other in-scope type variable

	     ; return () }
	where
	  dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
\end{code}


%************************************************************************
%*									*
		Scoped type variables
%*									*
%************************************************************************

\begin{code}
pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon, 
				 nest 2 (pp_sig ctxt) ]
  where
    pp_sig (FunSigCtxt n)  = pp_n_colon n
    pp_sig (ConArgCtxt n)  = pp_n_colon n
    pp_sig (ForSigCtxt n)  = pp_n_colon n
    pp_sig (RuleSigCtxt n) = pp_n_colon n
    pp_sig other	   = ppr (unLoc hs_ty)

    pp_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")])
\end{code}