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

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

		-- Kind checking
	kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
	kcLHsType, kcCheckLHsType, kcHsContext, 
	
		-- Typechecking kinded types
	tcHsKindedContext, tcHsKindedType, tcHsBangType,
	tcTyVarBndrs, dsHsType, kcHsLPred, dsHsLPred,
	tcDataKindSig, ExpKind(..), EkCtxt(..),

		-- Pattern type signatures
	tcHsPatSigType, tcPatSig
   ) where

#include "HsVersions.h"

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

import HsSyn
import RnHsSyn
import TcRnMonad
import TcEnv
import TcMType
import TcUnify
import TcIface
import TcType
import {- Kind parts of -} Type
import Var
import VarSet
import TyCon
import Class
import Name
import NameSet
import PrelNames
import TysWiredIn
import BasicTypes
import SrcLoc
import Util
import UniqSupply
import Outputable
import FastString
\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, 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) $
    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 }

tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type)
-- Typecheck an instance head.  We can't use 
-- tcHsSigType, because it's not a valid user type.
tcHsInstHead (L loc ty)
  = setSrcSpan loc   $	-- No need for an "In the type..." context
    tc_inst_head ty     -- because that comes from the caller
  where
    -- tc_inst_head expects HsPredTy, which isn't usually even allowed
    tc_inst_head (HsPredTy pred)
      = do { pred'  <- kcHsPred pred
    	   ; pred'' <- dsHsPred pred'
           ; return ([], [], mkPredTy pred'') }

    tc_inst_head (HsForAllTy _ tvs ctxt (L _ (HsPredTy pred)))
      = kcHsTyVars tvs    $ \ tvs' ->
    	do { ctxt' <- kcHsContext ctxt
    	   ; pred' <- kcHsPred    pred
    	   ; tcTyVarBndrs tvs'  $ \ tvs'' ->
    	do { ctxt'' <- mapM dsHsLPred (unLoc ctxt')
    	   ; pred'' <- dsHsPred pred'
    	   ; return (tvs'', ctxt'', mkPredTy pred'') } }

    tc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type"))

tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
-- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
-- except that we want to keep the tvs separate
tcHsQuantifiedType tv_names hs_ty
  = kcHsTyVars tv_names $ \ tv_names' ->
    do	{ kc_ty <- kcHsSigType hs_ty
    	; tcTyVarBndrs tv_names' $ \ tvs ->
    do	{ ty <- dsHsType kc_ty
    	; return (tvs, ty) } }

-- Used for the deriving(...) items
tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
tcHsDeriv = tc_hs_deriv []

tc_hs_deriv :: [LHsTyVarBndr Name] -> HsType Name
            -> TcM ([TyVar], Class, [Type])
tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
  = kcHsTyVars tv_names 		$ \ tv_names' ->
    do	{ cls_kind <- kcClass cls_name
	; (tys, _res_kind) <- kcApps cls_name cls_kind 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 	     = addKcTypeCtxt ty $ kcTypeType ty
kcHsLiftedSigType ty = addKcTypeCtxt ty $ kcLiftedType ty

tcHsKindedType :: LHsType Name -> TcM Type
  -- Don't do kind checking, nor validity checking.
  -- This is used in type and class decls, where kinding is
  -- done in advance, and validity checking is done later
  -- [Validity checking done later because of knot-tying issues.]
tcHsKindedType hs_ty = dsHsType hs_ty

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

tcHsKindedContext :: LHsContext Name -> TcM ThetaType
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsKindedType
tcHsKindedContext hs_theta = addLocM (mapM 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 = kc_check_lhs_type ty ekLifted
    
---------------------------
kcTypeType :: LHsType Name -> TcM (LHsType Name)
-- The type ty must be a *type*, but it can be lifted or 
-- unlifted or an unboxed tuple.
kcTypeType ty = kc_check_lhs_type ty ekOpen

---------------------------
kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)
kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind


kc_check_lhs_type :: LHsType Name -> ExpKind -> TcM (LHsType Name)
-- Check that the type has the specified kind
-- Be sure to use checkExpectedKind, rather than simply unifying 
-- with OpenTypeKind, because it gives better error messages
kc_check_lhs_type (L span ty) exp_kind 
  = setSrcSpan span $
    do { ty' <- kc_check_hs_type ty exp_kind
       ; return (L span ty') }

kc_check_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [LHsType Name]
kc_check_lhs_types tys_w_kinds
  = mapM kc_arg tys_w_kinds
  where
    kc_arg (arg, arg_kind) = kc_check_lhs_type arg arg_kind


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

-- First some special cases for better error messages 
-- when we know the expected kind
kc_check_hs_type (HsParTy ty) exp_kind
  = do { ty' <- kc_check_lhs_type ty exp_kind; return (HsParTy ty') }

kc_check_hs_type ty@(HsAppTy ty1 ty2) exp_kind
  = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 ty2
       ; (fun_ty', fun_kind) <- kc_lhs_type fun_ty
       ; arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
       ; return (mkHsAppTys fun_ty' arg_tys') }

-- This is the general case: infer the kind and compare
kc_check_hs_type ty exp_kind
  = do	{ (ty', act_kind) <- kc_hs_type ty
		-- Add the context round the inner check only
		-- because checkExpectedKind already mentions
		-- 'ty' by name in any error message

	; checkExpectedKind (strip ty) act_kind exp_kind
	; return ty' }
  where
	-- We infer the kind of the type, and then complain if it's
	-- not right.  But we don't want to complain about
	--	(ty) or !(ty) or forall a. ty
	-- when the real difficulty is with the 'ty' part.
    strip (HsParTy (L _ ty))          = strip ty
    strip (HsBangTy _ (L _ ty))       = strip ty
    strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
    strip ty			      = ty
\end{code}

	Here comes the main function

\begin{code}
kcLHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
-- Called from outside: set the context
kcLHsType ty = addKcTypeCtxt ty (kc_lhs_type ty)

kc_lhs_type :: LHsType Name -> TcM (LHsType Name, TcKind)
kc_lhs_type (L span ty)
  = setSrcSpan span $
    do { (ty', kind) <- kc_hs_type ty
       ; return (L span ty', kind) }

-- kc_hs_type *returns* the kind of the type, rather than taking an expected
-- kind as argument as tcExpr does.  
-- Reasons: 
--	(a) the kind of (->) is
--		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 :: HsType Name -> TcM (HsType Name, TcKind)
kc_hs_type (HsParTy ty) = do
   (ty', kind) <- kc_lhs_type ty
   return (HsParTy ty', kind)

kc_hs_type (HsTyVar name) = do
    kind <- kcTyVar name
    return (HsTyVar name, kind)

kc_hs_type (HsListTy ty) = do
    ty' <- kcLiftedType ty
    return (HsListTy ty', liftedTypeKind)

kc_hs_type (HsPArrTy ty) = do
    ty' <- kcLiftedType ty
    return (HsPArrTy ty', liftedTypeKind)

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

kc_hs_type (HsKindSig ty k) = do
    ty' <- kc_check_lhs_type ty (EK k EkKindSig)
    return (HsKindSig ty' k, k)

kc_hs_type (HsTupleTy Boxed tys) = do
    tys' <- mapM kcLiftedType tys
    return (HsTupleTy Boxed tys', liftedTypeKind)

kc_hs_type (HsTupleTy Unboxed tys) = do
    tys' <- mapM kcTypeType tys
    return (HsTupleTy Unboxed tys', ubxTupleKind)

kc_hs_type (HsFunTy ty1 ty2) = do
    ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)
    ty2' <- kcTypeType ty2
    return (HsFunTy ty1' ty2', liftedTypeKind)

kc_hs_type (HsOpTy ty1 op ty2) = do
    op_kind <- addLocM kcTyVar op
    ([ty1',ty2'], res_kind) <- kcApps op op_kind [ty1,ty2]
    return (HsOpTy ty1' op ty2', res_kind)

kc_hs_type (HsAppTy ty1 ty2) = do
    (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 pred)
  = wrongPredErr pred

kc_hs_type (HsCoreTy ty)
  = return (HsCoreTy ty, typeKind ty)

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

  	; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }

kc_hs_type (HsBangTy b ty)
  = do { (ty', kind) <- 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 (HsQuasiQuoteTy {}) = panic "kc_hs_type"	-- Eliminated by renamer

-- remove the doc nodes here, no need to worry about the location since
-- its the same for a doc node and it's child type node
kc_hs_type (HsDocTy ty _)
  = kc_hs_type (unLoc ty) 

---------------------------
kcApps :: Outputable a
       => a 
       -> TcKind			-- Function kind
       -> [LHsType Name]		-- Arg types
       -> TcM ([LHsType Name], TcKind)	-- Kind-checked args
kcApps the_fun fun_kind args
  = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
       ; args' <- kc_check_lhs_types args_w_kinds
       ; return (args', res_kind) }

kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
	    -> HsType Name     -- The type being checked (for err messages only)
	    -> ExpKind 	       -- Expected kind
	    -> TcM [LHsType Name]
kcCheckApps the_fun fun_kind args ty exp_kind
  = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
       ; checkExpectedKind ty res_kind exp_kind
       	     -- Check the result kind *before* checking argument kinds
	     -- This improves error message; Trac #2994
       ; kc_check_lhs_types args_w_kinds }

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 :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
splitFunKind _       _      fk [] = return ([], fk)
splitFunKind the_fun arg_no fk (arg:args)
  = do { mb_fk <- matchExpectedFunKind fk
       ; case mb_fk of
            Nothing       -> failWithTc too_many_args 
            Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
                                ; return ((arg, EK ak (EkArg the_fun arg_no)):aks, rk) } }
  where
    too_many_args = quotes the_fun <+>
		    ptext (sLit "is applied to too many type arguments")

---------------------------
kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
kcHsContext ctxt = wrapLocM (mapM kcHsLPred) ctxt

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

kcHsPred :: HsPred Name -> TcM (HsPred Name)
kcHsPred pred = do	-- Checks that the result is of kind liftedType
    (pred', kind) <- kc_pred pred
    checkExpectedKind pred kind ekLifted
    return pred'
    
---------------------------
kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)	
	-- Does *not* check for a saturated
	-- application (reason: used from TcDeriv)
kc_pred (HsIParam name ty)
  = do { (ty', kind) <- kc_lhs_type ty
       ; return (HsIParam name ty', kind)
       }
kc_pred (HsClassP cls tys)
  = do { kind <- kcClass cls
       ; (tys', res_kind) <- kcApps cls kind tys
       ; return (HsClassP cls tys', res_kind)
       }
kc_pred (HsEqualP ty1 ty2)
  = do { (ty1', kind1) <- kc_lhs_type ty1
--       ; checkExpectedKind ty1 kind1 liftedTypeKind
       ; (ty2', kind2) <- kc_lhs_type ty2
--       ; checkExpectedKind ty2 kind2 liftedTypeKind
       ; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
       ; return (HsEqualP ty1' ty2', liftedTypeKind)
       }

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

kcClass :: Name -> TcM TcKind
kcClass cls = do	-- Must be a class
    thing <- tcLookup cls
    case thing of
        AThing kind             -> return kind
        AGlobal (AClass cls)    -> return (tyConKind (classTyCon cls))
        _                       -> 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 :: HsType Name -> TcM Type
ds_type ty@(HsTyVar _)
  = ds_app ty []

ds_type (HsParTy ty)		-- Remove the parentheses markers
  = dsHsType ty

ds_type ty@(HsBangTy {})    -- No bangs should be here
  = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)

ds_type ty@(HsRecTy {})	    -- No bangs should be here
  = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)

ds_type (HsKindSig ty _)
  = dsHsType ty	-- Kind checking done already

ds_type (HsListTy ty) = do
    tau_ty <- dsHsType ty
    checkWiredInTyCon listTyCon
    return (mkListTy tau_ty)

ds_type (HsPArrTy ty) = do
    tau_ty <- dsHsType ty
    checkWiredInTyCon parrTyCon
    return (mkPArrTy tau_ty)

ds_type (HsTupleTy boxity tys) = do
    tau_tys <- dsHsTypes tys
    checkWiredInTyCon tycon
    return (mkTyConApp tycon tau_tys)
  where
    tycon = tupleTyCon boxity (length tys)

ds_type (HsFunTy ty1 ty2) = do
    tau_ty1 <- dsHsType ty1
    tau_ty2 <- dsHsType ty2
    return (mkFunTy tau_ty1 tau_ty2)

ds_type (HsOpTy ty1 (L span op) ty2) = do
    tau_ty1 <- dsHsType ty1
    tau_ty2 <- dsHsType ty2
    setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])

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

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

ds_type (HsPredTy pred) = do
    pred' <- dsHsPred pred
    return (mkPredTy pred')

ds_type (HsForAllTy _ tv_names ctxt ty)
  = tcTyVarBndrs tv_names               $ \ tyvars -> do
    theta <- mapM dsHsLPred (unLoc ctxt)
    tau <- dsHsType ty
    return (mkSigmaTy tyvars theta tau)

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

ds_type (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}

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 = do
    arg_tys <- dsHsTypes tys
    case ty of
	HsTyVar fun -> ds_var_app fun arg_tys
	_           -> do fun_ty <- ds_type ty
                          return (mkAppTys fun_ty arg_tys)

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


Contexts
~~~~~~~~

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

dsHsPred :: HsPred Name -> TcM PredType
dsHsPred (HsClassP class_name tys)
  = do { arg_tys <- dsHsTypes tys
       ; clas <- tcLookupClass class_name
       ; return (ClassP clas arg_tys)
       }
dsHsPred (HsEqualP ty1 ty2)
  = do { arg_ty1 <- dsHsType ty1
       ; arg_ty2 <- dsHsType ty2
       ; return (EqPred arg_ty1 arg_ty2)
       }
dsHsPred (HsIParam name ty)
  = do { arg_ty <- dsHsType ty
       ; return (IParam name arg_ty)
       }
\end{code}

\begin{code}
addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
	-- Wrap a context around only if we want to show that contexts.  
addKcTypeCtxt (L _ (HsPredTy _)) thing = thing
	-- Omit invisble ones and ones user's won't grok (HsPred p).
addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing

typeCtxt :: HsType Name -> SDoc
typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
\end{code}

%************************************************************************
%*									*
		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
  = do { kinded_tvs <- mapM (wrapLocM kcHsTyVar) tvs
       ; tcExtendKindEnvTvs kinded_tvs thing_inside }

kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
	-- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it	
kcHsTyVar (UserTyVar name _)  = UserTyVar name <$> newKindVar
kcHsTyVar tv@(KindedTyVar {}) = return tv

------------------
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 = do
    tyvars <- mapM (zonk . unLoc) bndrs
    tcExtendTyVarEnv tyvars (thing_inside tyvars)
  where
    zonk (UserTyVar name kind) = do { kind' <- zonkTcKindToKind kind
				    ; return (mkTyVar name kind') }
    zonk (KindedTyVar name kind) = return (mkTyVar name kind)

-----------------------------------
tcDataKindSig :: Maybe Kind -> TcM [TyVar]
-- GADT decls can have a (perhaps partial) kind signature
--	e.g.  data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for 
-- the argument kinds, and checks that the result kind is indeed *.
-- We use it also to make up argument type variables for for data instances.
tcDataKindSig Nothing = return []
tcDataKindSig (Just kind)
  = do	{ checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
	; span <- getSrcSpanM
	; us   <- newUniqueSupply 
	; let uniqs = uniqsFromSupply us
	; return [ mk_tv span uniq str kind 
		 | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
  where
    (arg_kinds, res_kind) = splitKindFunTys kind
    mk_tv loc uniq str kind = mkTyVar name kind
	where
	   name = mkInternalName uniq occ loc
	   occ  = mkOccName tvName str
	  
    dnames = map ('$' :) names	-- Note [Avoid name clashes for associated data types]

    names :: [String]
    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}

Note [Avoid name clashes for associated data types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider    class C a b where
               data D b :: * -> *
When typechecking the decl for D, we'll invent an extra type variable for D,
to fill out its kind.  We *don't* want this type variable to be 'a', because
in an .hi file we'd get
            class C a b where
               data D b a 
which makes it look as if there are *two* type indices.  But there aren't!
So we use $a instead, which cannot clash with a user-written type variable.
Remember that type variable binders in interface files are just FastStrings,
not proper Names.

(The tidying phase can't help here because we don't tidy TyCons.  Another
alternative would be to record the number of indexing parameters in the 
interface file.)


%************************************************************************
%*									*
		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 = userHsTyVarBndrs $ map (L span) $ 
			filterOut in_scope $
                        nameSetToList (extractHsTyVars hs_ty)

	; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
	; checkValidType ctxt sig_ty 
	; return (tyvars, sig_ty)
      }

tcPatSig :: UserTypeCtxt
	 -> LHsType Name
	 -> TcSigmaType
	 -> TcM (TcType,	   -- The type to use for "inside" the signature
		 [(Name, TcType)], -- The new bit of type environment, binding
				   -- the scoped type variables
                 HsWrapper)        -- Coercion due to unification with actual ty
		 		   -- Of shape:  res_ty ~ sig_ty
tcPatSig ctxt sig res_ty
  = do	{ (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
    	-- sig_tvs are the type variables free in 'sig', 
	-- and not already in scope. These are the ones
	-- that should be brought into scope

	; if null sig_tvs then do {
		-- The type signature binds no type variables, 
		-- and hence is rigid, so use it to zap the res_ty
         	  wrap <- tcSubType PatSigOrigin (SigSkol 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
		-- 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
				_              -> False
	; ASSERT( not in_pat_bind || null sig_tvs ) return ()

		-- 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 (SigSkol ctxt) res_ty sig_ty'

	-- Check that each is bound to a distinct type variable,
	-- and one that is not already in scope
	; binds_in_scope <- getScopedTyVarBinds
	; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys'
	; check binds_in_scope tv_binds
	
	-- Phew!
	; return (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
	= checkTc (null dups) (dupInScope n (head dups) ty)
		-- Must not bind to the same type variable
		-- as some other in-scope type variable
	where
	  dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
\end{code}


%************************************************************************
%*                                                                      *
        Checking kinds
%*                                                                      *
%************************************************************************

We would like to get a decent error message from
  (a) Under-applied type constructors
             f :: (Maybe, Maybe)
  (b) Over-applied type constructors
             f :: Int x -> Int x

\begin{code}
-- The ExpKind datatype means "expected kind" and contains 
-- some info about just why that kind is expected, to improve
-- the error message on a mis-match
data ExpKind = EK TcKind EkCtxt
data EkCtxt  = EkUnk		-- Unknown context
      	     | EkEqPred		-- Second argument of an equality predicate
      	     | EkKindSig	-- Kind signature
     	     | EkArg SDoc Int   -- Function, arg posn, expected kind


ekLifted, ekOpen :: ExpKind
ekLifted = EK liftedTypeKind EkUnk
ekOpen   = EK openTypeKind   EkUnk

checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
-- A fancy wrapper for 'unifyKind', which tries
-- to give decent error messages.
--      (checkExpectedKind ty act_kind exp_kind)
-- checks that the actual kind act_kind is compatible
--      with the expected kind exp_kind
-- The first argument, ty, is used only in the error message generation
checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
  | act_kind `isSubKind` exp_kind -- Short cut for a very common case
  = return ()
  | otherwise = do
    (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
    case mb_r of
        Just _  -> return ()  -- Unification succeeded
        Nothing -> do

        -- So there's definitely an error
        -- Now to find out what sort
           exp_kind <- zonkTcKind exp_kind
           act_kind <- zonkTcKind act_kind

           env0 <- tcInitTidyEnv
           let (exp_as, _) = splitKindFunTys exp_kind
               (act_as, _) = splitKindFunTys act_kind
               n_exp_as = length exp_as
               n_act_as = length act_as

               (env1, tidy_exp_kind) = tidyKind env0 exp_kind
               (env2, tidy_act_kind) = tidyKind env1 act_kind

               err | n_exp_as < n_act_as     -- E.g. [Maybe]
                   = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")

                     -- Now n_exp_as >= n_act_as. In the next two cases,
                     -- n_exp_as == 0, and hence so is n_act_as
                   | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
                   = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
                       <+> ptext (sLit "is unlifted")

                   | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
                   = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
                       <+> ptext (sLit "is lifted")

                   | otherwise               -- E.g. Monad [Int]
                   = ptext (sLit "Kind mis-match")

               more_info = sep [ expected_herald ek_ctxt <+> ptext (sLit "kind") 
                                    <+> quotes (pprKind tidy_exp_kind) <> comma,
                                 ptext (sLit "but") <+> quotes (ppr ty) <+>
                                     ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]

               expected_herald EkUnk     = ptext (sLit "Expected")
               expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
               expected_herald EkEqPred  = ptext (sLit "The left argument of the equality predicate had")
               expected_herald (EkArg fun arg_no)
	         = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
		   <+> quotes fun <+> ptext (sLit ("should have"))

           failWithTcM (env2, err $$ more_info)
\end{code}

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

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

    pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)

badPatSigTvs :: TcType -> [TyVar] -> SDoc
badPatSigTvs sig_ty bad_tvs
  = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, 
                 quotes (pprWithCommas ppr bad_tvs), 
          	 ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
	  	 ptext (sLit "but are actually discarded by a type synonym") ]
         , ptext (sLit "To fix this, expand the type synonym") 
         , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]

dupInScope :: Name -> Name -> Type -> SDoc
dupInScope n n' _
  = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
       2 (vcat [ptext (sLit "are bound to the same type (variable)"),
		ptext (sLit "Distinct scoped type variables must be distinct")])

wrongPredErr :: HsPred Name -> TcM (HsType Name, TcKind)
wrongPredErr pred = failWithTc (text "Predicate used as a type:" <+> ppr pred)
\end{code}