TcHsType.lhs 27.4 KB
Newer Older
1 2 3 4 5 6 7

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

\begin{code}
module TcHsType (
8
	tcHsSigType, tcHsDeriv,
9 10 11 12
	UserTypeCtxt(..), 

		-- Kind checking
	kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
13
	kcCheckHsType, kcHsContext, kcHsType, 
14 15
	
		-- Typechecking kinded types
16
	tcHsKindedContext, tcHsKindedType, tcHsBangType,
17
	tcTyVarBndrs, dsHsType, tcLHsConSig, tcDataKindSig,
18

19
	tcHsPatSigType, tcAddLetBoundTyVars,
20
	
21
	TcSigInfo(..), TcSigFun, lookupSig 
22 23 24 25
   ) where

#include "HsVersions.h"

26 27 28
import HsSyn		( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, HsBang,
			  LHsContext, HsPred(..), LHsPred, LHsBinds,
			  getBangStrictness, collectSigTysFromHsBinds )
29
import RnHsSyn		( extractHsTyVars )
30
import TcRnMonad
31
import TcEnv		( tcExtendTyVarEnv, tcExtendKindEnv,
32
			  tcLookup, tcLookupClass, tcLookupTyCon,
33
		 	  TyThing(..), getInLocalScope, wrongThingErr
34
			)
35
import TcMType		( newKindVar, newMetaTyVar, zonkTcKindToKind, 
36
			  checkValidType, UserTypeCtxt(..), pprHsSigCtxt
37
			)
38
import TcUnify		( unifyFunKind, checkExpectedKind )
39
import TcType		( Type, PredType(..), ThetaType, 
40
			  MetaDetails(Flexi), hoistForAllTys,
41
			  TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
42
		 	  mkFunTy, 
43
			  mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, 
44
			  typeKind )
45 46
import Kind 		( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, 
			  openTypeKind, argTypeKind, splitKindFunTys )
47 48
import Id		( idName )
import Var		( TyVar, mkTyVar )
49
import TyCon		( TyCon, tyConKind )
50
import Class		( Class, classTyCon )
51 52
import Name		( Name, mkInternalName )
import OccName		( mkOccName, tvName )
53 54 55
import NameSet
import PrelNames	( genUnitTyConName )
import TysWiredIn	( mkListTy, mkPArrTy, mkTupleTy )
56
import Bag		( bagToList )
57
import BasicTypes	( Boxity(..) )
58 59
import SrcLoc		( Located(..), unLoc, noLoc, srcSpanStart )
import UniqSupply	( uniqsFromSupply )
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146
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}
147
tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
148
  -- Do kind checking, and hoist for-alls to the top
149 150 151
  -- 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
152
tcHsSigType ctxt hs_ty 
153
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
154 155 156 157
    do	{ kinded_ty <- kcTypeType hs_ty
	; ty <- tcHsKindedType kinded_ty
	; checkValidType ctxt ty	
	; returnM ty }
158

159 160 161 162
-- Used for the deriving(...) items
tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
tcHsDeriv = addLocM (tc_hs_deriv [])

163
tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
  = 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)
180 181 182 183 184 185 186
\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}
187
kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
188 189 190 191
	-- Used for type signatures
kcHsSigType ty 	     = kcTypeType ty
kcHsLiftedSigType ty = kcLiftedType ty

192
tcHsKindedType :: LHsType Name -> TcM Type
193 194 195 196 197 198 199 200 201
  -- 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 
  = do	{ ty <- dsHsType hs_ty
	; return (hoistForAllTys ty) }

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

207
tcHsKindedContext :: LHsContext Name -> TcM ThetaType
208 209
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsKindedType
210
tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
211 212 213 214 215 216 217 218 219 220 221 222 223
\end{code}


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

\begin{code}
---------------------------
224
kcLiftedType :: LHsType Name -> TcM (LHsType Name)
225
-- The type ty must be a *lifted* *type*
226 227 228
kcLiftedType ty = kcCheckHsType ty liftedTypeKind
    
---------------------------
229
kcTypeType :: LHsType Name -> TcM (LHsType Name)
230 231 232
-- The type ty must be a *type*, but it can be lifted or 
-- unlifted or an unboxed tuple.
kcTypeType ty = kcCheckHsType ty openTypeKind
233 234

---------------------------
235
kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
236
-- Check that the type has the specified kind
237 238 239
-- Be sure to use checkExpectedKind, rather than simply unifying 
-- with OpenTypeKind, because it gives better error messages
kcCheckHsType (L span ty) exp_kind 
240
  = setSrcSpan span				$
241
    kc_hs_type ty				`thenM` \ (ty', act_kind) ->
242
    checkExpectedKind ty act_kind exp_kind	`thenM_`
243
    returnM (L span ty')
244 245 246 247 248
\end{code}

	Here comes the main function

\begin{code}
249 250
kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
kcHsType ty = wrapLocFstM kc_hs_type ty
251 252 253 254 255 256 257 258 259 260
-- 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

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

265
kc_hs_type (HsTyVar name)
266 267 268
  = kcTyVar name	`thenM` \ kind ->
    returnM (HsTyVar name, kind)

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

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

277
kc_hs_type (HsNumTy n)
278 279
   = returnM (HsNumTy n, liftedTypeKind)

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

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

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

292
kc_hs_type (HsFunTy ty1 ty2)
293 294
  = kcCheckHsType ty1 argTypeKind	`thenM` \ ty1' ->
    kcTypeType ty2			`thenM` \ ty2' ->
295 296
    returnM (HsFunTy ty1' ty2', liftedTypeKind)

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

302
kc_hs_type ty@(HsAppTy ty1 ty2)
303
  = kcHsType fun_ty			  `thenM` \ (fun_ty', fun_kind) ->
304 305
    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)
306 307
  where
    (fun_ty, arg_tys) = split ty1 [ty2]
308 309 310 311 312 313
    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)
314 315 316
  = kcHsPred pred		`thenM` \ pred' ->
    returnM (HsPredTy pred', liftedTypeKind)

317
kc_hs_type (HsForAllTy exp tv_names context ty)
318 319
  = kcHsTyVars tv_names		$ \ tv_names' ->
    kcHsContext context		`thenM`	\ ctxt' ->
320
    kcLiftedType ty		`thenM` \ ty' ->
321
	-- The body of a forall is usually a type, but in principle
322 323 324 325 326
	-- 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)
	--
327 328 329
	-- 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)
330

331 332 333 334 335 336 337 338
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)


339
---------------------------
340 341 342 343
kcApps :: TcKind			-- Function kind
       -> SDoc				-- Function 
       -> [LHsType Name]		-- Arg types
       -> TcM ([LHsType Name], TcKind)	-- Kind-checked args
344 345
kcApps fun_kind ppr_fun args
  = split_fk fun_kind (length args)	`thenM` \ (arg_kinds, res_kind) ->
346
    zipWithM kc_arg args arg_kinds	`thenM` \ args' ->
347 348 349 350 351 352 353 354 355
    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)

356
    kc_arg arg arg_kind = kcCheckHsType arg arg_kind
357 358 359 360 361

    too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
		    ptext SLIT("is applied to too many type arguments")

---------------------------
362
kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
363 364 365 366
kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt

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

368 369 370
kcHsPred :: HsPred Name -> TcM (HsPred Name)
kcHsPred pred	-- Checks that the result is of kind liftedType
  = kc_pred pred				`thenM` \ (pred', kind) ->
371
    checkExpectedKind pred kind liftedTypeKind	`thenM_` 
372
    returnM pred'
373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389
    
---------------------------
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
390 391 392
  = traceTc (text "lk1" <+> ppr name) 	`thenM_`
    tcLookup name	`thenM` \ thing ->
    traceTc (text "lk2" <+> ppr name <+> ppr thing) 	`thenM_`
393
    case thing of 
394
	ATyVar _ ty	    	-> returnM (typeKind ty)
395
	AThing kind		-> returnM kind
396
	AGlobal (ATyCon tc) 	-> returnM (tyConKind tc) 
397
	other			-> wrongThingErr "type" thing name
398 399 400 401 402

kcClass :: Name -> TcM TcKind
kcClass cls	-- Must be a class
  = tcLookup cls 				`thenM` \ thing -> 
    case thing of
403
	AThing kind		-> returnM kind
404
	AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
405
	other		        -> wrongThingErr "class" thing cls
406 407 408 409 410 411 412 413 414 415 416 417 418 419
\end{code}


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

The type desugarer

	* Transforms from HsType to Type
	* Zonks any kinds

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

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

430
ds_type ty@(HsTyVar name)
431 432
  = ds_app ty []

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

436 437 438
ds_type ty@(HsBangTy _ _)	-- No bangs should be here
  = failWithTc (ptext SLIT("Unexpected strictness annotation:") <+> ppr ty)

439
ds_type (HsKindSig ty k)
440 441
  = dsHsType ty	-- Kind checking done already

442
ds_type (HsListTy ty)
443 444 445
  = dsHsType ty				`thenM` \ tau_ty ->
    returnM (mkListTy tau_ty)

446
ds_type (HsPArrTy ty)
447 448 449
  = dsHsType ty				`thenM` \ tau_ty ->
    returnM (mkPArrTy tau_ty)

450
ds_type (HsTupleTy boxity tys)
451 452 453
  = dsHsTypes tys			`thenM` \ tau_tys ->
    returnM (mkTupleTy boxity (length tys) tau_tys)

454
ds_type (HsFunTy ty1 ty2)
455 456 457 458
  = dsHsType ty1			`thenM` \ tau_ty1 ->
    dsHsType ty2			`thenM` \ tau_ty2 ->
    returnM (mkFunTy tau_ty1 tau_ty2)

459 460 461
ds_type (HsOpTy ty1 (L span op) ty2)
  = dsHsType ty1 		`thenM` \ tau_ty1 ->
    dsHsType ty2 		`thenM` \ tau_ty2 ->
462
    setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
463

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

469 470
ds_type ty@(HsAppTy _ _)
  = ds_app ty []
471

472
ds_type (HsPredTy pred)
473 474 475
  = dsHsPred pred	`thenM` \ pred' ->
    returnM (mkPredTy pred')

476
ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
477
  = tcTyVarBndrs tv_names		$ \ tyvars ->
478
    mappM dsHsLPred (unLoc ctxt)	`thenM` \ theta ->
479 480 481 482 483 484 485 486 487 488
    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}
489
ds_app :: HsType Name -> [LHsType Name] -> TcM Type
490
ds_app (HsAppTy ty1 ty2) tys
491
  = ds_app (unLoc ty1) (ty2:tys)
492 493 494 495 496

ds_app ty tys
  = dsHsTypes tys			`thenM` \ arg_tys ->
    case ty of
	HsTyVar fun -> ds_var_app fun arg_tys
497
	other	    -> ds_type ty		`thenM` \ fun_ty ->
498 499 500 501 502 503
		       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
504 505 506
	ATyVar _ ty 	    -> returnM (mkAppTys ty arg_tys)
	AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
	other		    -> wrongThingErr "type" thing name
507 508 509 510 511
\end{code}


Contexts
~~~~~~~~
512

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

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

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

527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579
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}
580 581 582 583 584 585 586 587 588

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


\begin{code}
589 590
kcHsTyVars :: [LHsTyVarBndr Name] 
	   -> ([LHsTyVarBndr Name] -> TcM r) 	-- These binders are kind-annotated
591 592 593
						-- They scope over the thing inside
	   -> TcM r
kcHsTyVars tvs thing_inside 
594
  = mappM (wrapLocM kcHsTyVar) tvs	`thenM` \ bndrs ->
595 596
    tcExtendKindEnv [(n,k) | L _ (KindedTyVar n k) <- bndrs]
		    (thing_inside bndrs)
597 598 599 600 601 602 603 604

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)

------------------
605
tcTyVarBndrs :: [LHsTyVarBndr Name] 	-- Kind-annotated binders, which need kind-zonking
606 607 608 609 610
	     -> ([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
611
  = mapM (zonk . unLoc) bndrs	`thenM` \ tyvars ->
612 613 614 615
    tcExtendTyVarEnv tyvars (thing_inside tyvars)
  where
    zonk (KindedTyVar name kind) = zonkTcKindToKind kind	`thenM` \ kind' ->
				   returnM (mkTyVar name kind')
616
    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
617
			    returnM (mkTyVar name liftedTypeKind)
618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647

-----------------------------------
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)
648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690
\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}
691 692 693 694 695 696 697 698 699 700 701 702 703
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

704 705 706
	-- Behave like kcHsType on a ForAll type
	-- i.e. make kinded tyvars with mutable kinds, 
	--      and kind-check the enclosed types
707 708 709
	; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
				    { kinded_ty <- kcTypeType hs_ty
				    ; return (kinded_tvs, kinded_ty) }
710 711

	-- Zonk the mutable kinds and bring the tyvars into scope
712 713
	-- Just like the call to tcTyVarBndrs in ds_type (HsForAllTy case), 
	-- except that it brings *meta* tyvars into scope, not regular ones
714
	--
715
	-- 	[Out of date, but perhaps should be resurrected]
716 717 718 719 720 721
	-- 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
722 723
	; tyvars <- mapM (zonk . unLoc) kinded_tvs
	; return (tyvars, kinded_ty) }
724 725
  where
    zonk (KindedTyVar name kind) = zonkTcKindToKind kind	`thenM` \ kind' ->
726 727 728
				   newMetaTyVar name kind' Flexi
	-- Scoped type variables are bound to a *type*, hence Flexi
    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
729
			    returnM (mkTyVar name liftedTypeKind)
730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756

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) }
757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776
\end{code}


%************************************************************************
%*									*
\subsection{Signatures}
%*									*
%************************************************************************

@tcSigs@ checks the signatures for validity, and returns a list of
{\em freshly-instantiated} signatures.  That is, the types are already
split up, and have fresh type variables installed.  All non-type-signature
"RenamedSigs" are ignored.

The @TcSigInfo@ contains @TcTypes@ because they are unified with
the variable's type, and after that checked to see whether they've
been instantiated.

\begin{code}
data TcSigInfo
777
  = TcSigInfo {
778 779 780 781 782 783 784 785 786 787 788 789
	sig_id     :: TcId,		-- *Polymorphic* binder for this value...

	sig_scoped :: [Name],		-- Names for any scoped type variables
					-- Invariant: correspond 1-1 with an initial
					-- segment of sig_tvs (see Note [Scoped])

	sig_tvs    :: [TcTyVar],	-- Instantiated type variables
					-- See Note [Instantiate sig]

	sig_theta  :: TcThetaType,	-- Instantiated theta
	sig_tau    :: TcTauType,	-- Instantiated tau
	sig_loc    :: InstLoc	 	-- The location of the signature
790
    }
791

792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813
-- 	Note [Scoped]
-- There may be more instantiated type variables than scoped 
-- ones.  For example:
--	type T a = forall b. b -> (a,b)
--	f :: forall c. T c
-- Here, the signature for f will have one scoped type variable, c,
-- but two instantiated type variables, c' and b'.  
--
-- We assume that the scoped ones are at the *front* of sig_tvs,
-- and remember the names from the original HsForAllTy in sig_scoped

-- 	Note [Instantiate sig]
-- It's vital to instantiate a type signature with fresh variable.
-- For example:
--	type S = forall a. a->a
--	f,g :: S
--	f = ...
--	g = ...
-- Here, we must use distinct type variables when checking f,g's right hand sides.
-- (Instantiation is only necessary because of type synonyms.  Otherwise,
-- it's all cool; each signature has distinct type variables from the renamer.)

814
type TcSigFun = Name -> Maybe TcSigInfo
815 816

instance Outputable TcSigInfo where
817 818
    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
819

820 821 822 823 824
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
825 826
\end{code}