TcHsType.lhs 27.6 KB
Newer Older
1 2
%
% (c) The University of Glasgow 2006
3 4 5 6 7 8
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section[TcMonoType]{Typechecking user-specified @MonoTypes@}

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

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

21 22
		-- Pattern type signatures
	tcHsPatSigType, tcPatSig
23 24 25 26
   ) where

#include "HsVersions.h"

27 28
import HsSyn
import RnHsSyn
29
import TcRnMonad
30 31 32 33 34 35 36 37 38 39 40
import TcEnv
import TcMType
import TcUnify
import TcIface
import TcType
import {- Kind parts of -} Type
import Var
import TyCon
import Class
import Name
import OccName
41
import NameSet
42 43 44 45 46
import PrelNames
import TysWiredIn
import BasicTypes
import SrcLoc
import UniqSupply
47 48 49 50 51 52 53 54 55 56 57 58 59 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
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}
134
tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
135
  -- Do kind checking, and hoist for-alls to the top
136 137 138
  -- 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
139
tcHsSigType ctxt hs_ty 
140
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
141 142 143 144
    do	{ kinded_ty <- kcTypeType hs_ty
	; ty <- tcHsKindedType kinded_ty
	; checkValidType ctxt ty	
	; returnM ty }
145

146 147 148 149
-- Used for the deriving(...) items
tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
tcHsDeriv = addLocM (tc_hs_deriv [])

150
tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
  = 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)
167 168 169 170 171 172 173
\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}
174
kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
175 176 177 178
	-- Used for type signatures
kcHsSigType ty 	     = kcTypeType ty
kcHsLiftedSigType ty = kcLiftedType ty

179
tcHsKindedType :: LHsType Name -> TcM Type
180
  -- Don't do kind checking, nor validity checking.
181 182 183
  -- 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.]
184
tcHsKindedType hs_ty = dsHsType hs_ty
185

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

191
tcHsKindedContext :: LHsContext Name -> TcM ThetaType
192 193
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsKindedType
194
tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
195 196 197 198 199 200 201 202 203 204 205 206 207
\end{code}


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

\begin{code}
---------------------------
208
kcLiftedType :: LHsType Name -> TcM (LHsType Name)
209
-- The type ty must be a *lifted* *type*
210 211 212
kcLiftedType ty = kcCheckHsType ty liftedTypeKind
    
---------------------------
213
kcTypeType :: LHsType Name -> TcM (LHsType Name)
214 215 216
-- The type ty must be a *type*, but it can be lifted or 
-- unlifted or an unboxed tuple.
kcTypeType ty = kcCheckHsType ty openTypeKind
217 218

---------------------------
219
kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
220
-- Check that the type has the specified kind
221 222 223
-- Be sure to use checkExpectedKind, rather than simply unifying 
-- with OpenTypeKind, because it gives better error messages
kcCheckHsType (L span ty) exp_kind 
224
  = setSrcSpan span				$
225
    do	{ (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
226 227 228
		-- Add the context round the inner check only
		-- because checkExpectedKind already mentions
		-- 'ty' by name in any error message
229

230
	; checkExpectedKind (strip ty) act_kind exp_kind
231
	; return (L span ty') }
232
  where
233
	-- Wrap a context around only if we want to show that contexts.  
234
    add_ctxt (HsPredTy p)		 thing = thing
235
	-- Omit invisble ones and ones user's won't grok (HsPred p).
236 237 238 239 240 241
    add_ctxt (HsForAllTy _ _ (L _ []) _) thing = thing
	-- Omit wrapping if the theta-part is empty
	-- Reason: the recursive call to kcLiftedType, in the ForAllTy
	--	   case of kc_hs_type, will do the wrapping instead
	--	   and we don't want to duplicate
    add_ctxt other_ty thing = addErrCtxt (typeCtxt other_ty) thing
242 243 244 245 246 247 248 249 250

	-- 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
251 252 253 254 255
\end{code}

	Here comes the main function

\begin{code}
256 257
kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
kcHsType ty = wrapLocFstM kc_hs_type ty
258 259 260 261 262 263 264 265 266 267
-- 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

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

272
kc_hs_type (HsTyVar name)
273 274 275
  = kcTyVar name	`thenM` \ kind ->
    returnM (HsTyVar name, kind)

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

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

284
kc_hs_type (HsNumTy n)
285 286
   = returnM (HsNumTy n, liftedTypeKind)

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

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

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

299
kc_hs_type (HsFunTy ty1 ty2)
300 301
  = kcCheckHsType ty1 argTypeKind	`thenM` \ ty1' ->
    kcTypeType ty2			`thenM` \ ty2' ->
302 303
    returnM (HsFunTy ty1' ty2', liftedTypeKind)

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

309
kc_hs_type ty@(HsAppTy ty1 ty2)
310
  = kcHsType fun_ty			  `thenM` \ (fun_ty', fun_kind) ->
311 312
    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)
313 314
  where
    (fun_ty, arg_tys) = split ty1 [ty2]
315 316 317 318 319 320
    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)
321 322 323
  = kcHsPred pred		`thenM` \ pred' ->
    returnM (HsPredTy pred', liftedTypeKind)

324
kc_hs_type (HsForAllTy exp tv_names context ty)
325
  = kcHsTyVars tv_names		$ \ tv_names' ->
326 327 328 329 330 331 332 333 334 335 336 337
    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) }
338

339 340 341 342 343 344 345
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)

346 347 348 349
-- 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) 
350

351
---------------------------
352 353 354 355
kcApps :: TcKind			-- Function kind
       -> SDoc				-- Function 
       -> [LHsType Name]		-- Arg types
       -> TcM ([LHsType Name], TcKind)	-- Kind-checked args
356 357
kcApps fun_kind ppr_fun args
  = split_fk fun_kind (length args)	`thenM` \ (arg_kinds, res_kind) ->
358
    zipWithM kc_arg args arg_kinds	`thenM` \ args' ->
359 360 361 362 363 364 365 366 367
    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)

368
    kc_arg arg arg_kind = kcCheckHsType arg arg_kind
369 370 371 372 373

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

---------------------------
374
kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
375 376 377 378
kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt

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

380 381 382
kcHsPred :: HsPred Name -> TcM (HsPred Name)
kcHsPred pred	-- Checks that the result is of kind liftedType
  = kc_pred pred				`thenM` \ (pred', kind) ->
383
    checkExpectedKind pred kind liftedTypeKind	`thenM_` 
384
    returnM pred'
385 386 387 388 389 390
    
---------------------------
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)
391 392 393
  = do { (ty', kind) <- kcHsType ty
       ; returnM (HsIParam name ty', kind)
       }
394
kc_pred pred@(HsClassP cls tys)
395 396 397 398 399 400 401 402 403 404 405
  = do { kind <- kcClass cls
       ; (tys', res_kind) <- kcApps kind (ppr cls) tys
       ; returnM (HsClassP cls tys', res_kind)
       }
kc_pred pred@(HsEqualP ty1 ty2)
  = do { (ty1', kind1) <- kcHsType ty1
       ; checkExpectedKind ty1 kind1 liftedTypeKind
       ; (ty2', kind2) <- kcHsType ty2
       ; checkExpectedKind ty2 kind2 liftedTypeKind
       ; returnM (HsEqualP ty1 ty2, liftedTypeKind)
       }
406 407 408 409

---------------------------
kcTyVar :: Name -> TcM TcKind
kcTyVar name	-- Could be a tyvar or a tycon
410 411 412
  = traceTc (text "lk1" <+> ppr name) 	`thenM_`
    tcLookup name	`thenM` \ thing ->
    traceTc (text "lk2" <+> ppr name <+> ppr thing) 	`thenM_`
413
    case thing of 
414
	ATyVar _ ty	    	-> returnM (typeKind ty)
415
	AThing kind		-> returnM kind
416
	AGlobal (ATyCon tc) 	-> returnM (tyConKind tc) 
417
	other			-> wrongThingErr "type" thing name
418 419 420 421 422

kcClass :: Name -> TcM TcKind
kcClass cls	-- Must be a class
  = tcLookup cls 				`thenM` \ thing -> 
    case thing of
423
	AThing kind		-> returnM kind
424
	AGlobal (AClass cls)    -> returnM (tyConKind (classTyCon cls))
425
	other		        -> wrongThingErr "class" thing cls
426 427 428 429 430 431 432 433 434 435 436 437 438 439
\end{code}


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

The type desugarer

	* Transforms from HsType to Type
	* Zonks any kinds

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

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

450
ds_type ty@(HsTyVar name)
451 452
  = ds_app ty []

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

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

459
ds_type (HsKindSig ty k)
460 461
  = dsHsType ty	-- Kind checking done already

462
ds_type (HsListTy ty)
463 464
  = dsHsType ty			`thenM` \ tau_ty ->
    checkWiredInTyCon listTyCon	`thenM_`
465 466
    returnM (mkListTy tau_ty)

467
ds_type (HsPArrTy ty)
468 469
  = dsHsType ty			`thenM` \ tau_ty ->
    checkWiredInTyCon parrTyCon	`thenM_`
470 471
    returnM (mkPArrTy tau_ty)

472
ds_type (HsTupleTy boxity tys)
473 474 475 476 477
  = dsHsTypes tys		`thenM` \ tau_tys ->
    checkWiredInTyCon tycon	`thenM_`
    returnM (mkTyConApp tycon tau_tys)
  where
    tycon = tupleTyCon boxity (length tys)
478

479
ds_type (HsFunTy ty1 ty2)
480 481 482 483
  = dsHsType ty1			`thenM` \ tau_ty1 ->
    dsHsType ty2			`thenM` \ tau_ty2 ->
    returnM (mkFunTy tau_ty1 tau_ty2)

484 485 486
ds_type (HsOpTy ty1 (L span op) ty2)
  = dsHsType ty1 		`thenM` \ tau_ty1 ->
    dsHsType ty2 		`thenM` \ tau_ty2 ->
487
    setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
488

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

494 495
ds_type ty@(HsAppTy _ _)
  = ds_app ty []
496

497
ds_type (HsPredTy pred)
498 499 500
  = dsHsPred pred	`thenM` \ pred' ->
    returnM (mkPredTy pred')

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

507 508
ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"

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

512 513 514 515 516 517 518
dsHsTypes arg_tys = mappM dsHsType arg_tys
\end{code}

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

\begin{code}
519
ds_app :: HsType Name -> [LHsType Name] -> TcM Type
520
ds_app (HsAppTy ty1 ty2) tys
521
  = ds_app (unLoc ty1) (ty2:tys)
522 523 524 525 526

ds_app ty tys
  = dsHsTypes tys			`thenM` \ arg_tys ->
    case ty of
	HsTyVar fun -> ds_var_app fun arg_tys
527
	other	    -> ds_type ty		`thenM` \ fun_ty ->
528 529 530 531 532 533
		       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
534
	ATyVar _ ty 	    -> returnM (mkAppTys ty arg_tys)
535
	AGlobal (ATyCon tc) -> returnM (mkTyConApp tc arg_tys)
536
	other		    -> wrongThingErr "type" thing name
537 538 539 540 541
\end{code}


Contexts
~~~~~~~~
542

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

547
dsHsPred pred@(HsClassP class_name tys)
548 549 550 551 552 553 554 555 556
  = do { arg_tys <- dsHsTypes tys
       ; clas <- tcLookupClass class_name
       ; returnM (ClassP clas arg_tys)
       }
dsHsPred pred@(HsEqualP ty1 ty2)
  = do { arg_ty1 <- dsHsType ty1
       ; arg_ty2 <- dsHsType ty2
       ; returnM (EqPred arg_ty1 arg_ty2)
       }
557
dsHsPred (HsIParam name ty)
558 559 560
  = do { arg_ty <- dsHsType ty
       ; returnM (IParam name arg_ty)
       }
561 562
\end{code}

563 564 565
GADT constructor signatures

\begin{code}
566
tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584
tcLHsConResTy res_ty
  = addErrCtxt (gadtResCtxt res_ty) $
    case get_largs res_ty [] of
	   (HsTyVar tc_name, args) 
	      -> do { args' <- mapM dsHsType args
		    ; thing <- tcLookup tc_name
		    ; case thing of
		        AGlobal (ATyCon tc) -> return (tc, args')
		        other -> failWithTc (badGadtDecl res_ty) }
	   other -> failWithTc (badGadtDecl res_ty)
  where
	-- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
	-- because that causes a black hole, and for good reason.  Building
	-- the type means expanding type synonyms, and we can't do that
	-- inside the "knot".  So we have to work by steam.
    get_largs (L _ ty) args = get_args ty args
    get_args (HsAppTy fun arg) 		  args = get_largs fun (arg:args)
    get_args (HsParTy ty)      		  args = get_largs ty  args
585 586
    get_args (HsOpTy ty1 (L span tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
    get_args ty  	     		  args = (ty, args)
587

588 589
gadtResCtxt ty
  = hang (ptext SLIT("In the result type of a data constructor:"))
590 591
       2 (ppr ty)
badGadtDecl ty
592
  = hang (ptext SLIT("Malformed constructor result type:"))
593
       2 (ppr ty)
594 595

typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
596
\end{code}
597 598 599 600 601 602 603 604 605

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


\begin{code}
606 607
kcHsTyVars :: [LHsTyVarBndr Name] 
	   -> ([LHsTyVarBndr Name] -> TcM r) 	-- These binders are kind-annotated
608 609 610
						-- They scope over the thing inside
	   -> TcM r
kcHsTyVars tvs thing_inside 
611
  = mappM (wrapLocM kcHsTyVar) tvs	`thenM` \ bndrs ->
612
    tcExtendKindEnvTvs bndrs (thing_inside bndrs)
613 614 615 616 617 618 619 620

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)

------------------
621
tcTyVarBndrs :: [LHsTyVarBndr Name] 	-- Kind-annotated binders, which need kind-zonking
622 623 624 625 626
	     -> ([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
627
  = mapM (zonk . unLoc) bndrs	`thenM` \ tyvars ->
628 629
    tcExtendTyVarEnv tyvars (thing_inside tyvars)
  where
630 631
    zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
				      ; return (mkTyVar name kind') }
632
    zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
633
			    return (mkTyVar name liftedTypeKind)
634 635 636

-----------------------------------
tcDataKindSig :: Maybe Kind -> TcM [TyVar]
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
637
-- GADT decls can have a (perhaps partial) kind signature
638 639
--	e.g.  data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for 
640 641
-- 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.
642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664
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)
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 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707
\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}
708 709 710 711 712 713 714 715
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
716

717 718 719 720 721 722 723 724
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) 
725 726 727
			| n <- nameSetToList (extractHsTyVars hs_ty),
			  not (in_scope n) ]

728 729
	-- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
	-- except that we want to keep the tvs separate
730 731 732
	; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
				    { kinded_ty <- kcTypeType hs_ty
				    ; return (kinded_tvs, kinded_ty) }
733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786
	; 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)
	} }
787
  where
788 789 790
    check in_scope []		 = return ()
    check in_scope ((n,ty):rest) = do { check_one in_scope n ty
				      ; check ((n,ty):in_scope) rest }
791

792 793 794
    check_one in_scope n ty
	= do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
		-- Must bind to a type variable
795

796 797 798
	     ; checkTc (null dups) (dupInScope n (head dups) ty)
		-- Must not bind to the same type variable
		-- as some other in-scope type variable
799

800 801 802
	     ; return () }
	where
	  dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
803 804 805 806 807
\end{code}


%************************************************************************
%*									*
808
		Scoped type variables
809 810 811 812
%*									*
%************************************************************************

\begin{code}
813 814 815
pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon, 
				 nest 2 (pp_sig ctxt) ]
816
  where
817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838
    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 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")])
839 840
\end{code}