TcTyClsDecls.lhs 51.2 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3
% (c) The AQUA Project, Glasgow University, 1996-1998
4
%
5 6

TcTyClsDecls: Typecheck type and class declarations
7 8 9

\begin{code}
module TcTyClsDecls (
10
	tcTyAndClassDecls, tcFamInstDecl
11 12
    ) where

13
#include "HsVersions.h"
14

15 16 17 18 19
import HsSyn
import HsTypes
import BasicTypes
import HscTypes
import BuildTyCl
20
import TcUnify
21
import TcRnMonad
22 23 24 25 26 27
import TcEnv
import TcTyDecls
import TcClassDcl
import TcHsType
import TcMType
import TcType
28
import FunDeps
29 30 31 32 33 34 35 36 37
import Type
import Generics
import Class
import TyCon
import DataCon
import Var
import VarSet
import Name
import OccName
sof's avatar
sof committed
38
import Outputable
39 40 41 42 43 44 45 46
import Maybes
import Monad
import Unify
import Util
import SrcLoc
import ListSetOps
import Digraph
import DynFlags
47
import FastString
48

49
import Data.List
50
import Control.Monad    ( mplus )
51 52
\end{code}

53 54 55 56 57 58 59

%************************************************************************
%*									*
\subsection{Type checking for type and class declarations}
%*									*
%************************************************************************

60 61
Dealing with a group
~~~~~~~~~~~~~~~~~~~~
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84
Consider a mutually-recursive group, binding 
a type constructor T and a class C.

Step 1: 	getInitialKind
	Construct a KindEnv by binding T and C to a kind variable 

Step 2: 	kcTyClDecl
	In that environment, do a kind check

Step 3: Zonk the kinds

Step 4: 	buildTyConOrClass
	Construct an environment binding T to a TyCon and C to a Class.
	a) Their kinds comes from zonking the relevant kind variable
	b) Their arity (for synonyms) comes direct from the decl
	c) The funcional dependencies come from the decl
	d) The rest comes a knot-tied binding of T and C, returned from Step 4
	e) The variances of the tycons in the group is calculated from 
		the knot-tied stuff

Step 5: 	tcTyClDecl1
	In this environment, walk over the decls, constructing the TyCons and Classes.
	This uses in a strict way items (a)-(c) above, which is why they must
85 86 87
	be constructed in Step 4. Feed the results back to Step 4.
	For this step, pass the is-recursive flag as the wimp-out flag
	to tcTyClDecl1.
88
	
89

90
Step 6:		Extend environment
91 92 93
	We extend the type environment with bindings not only for the TyCons and Classes,
	but also for their "implicit Ids" like data constructors and class selectors

94 95 96 97 98
Step 7:		checkValidTyCl
	For a recursive group only, check all the decls again, just
	to check all the side conditions on validity.  We could not
	do this before because we were in a mutually recursive knot.

99 100
Identification of recursive TyCons
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
101
The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
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
@TyThing@s.

Identifying a TyCon as recursive serves two purposes

1.  Avoid infinite types.  Non-recursive newtypes are treated as
"transparent", like type synonyms, after the type checker.  If we did
this for all newtypes, we'd get infinite types.  So we figure out for
each newtype whether it is "recursive", and add a coercion if so.  In
effect, we are trying to "cut the loops" by identifying a loop-breaker.

2.  Avoid infinite unboxing.  This is nothing to do with newtypes.
Suppose we have
        data T = MkT Int T
        f (MkT x t) = f t
Well, this function diverges, but we don't want the strictness analyser
to diverge.  But the strictness analyser will diverge because it looks
deeper and deeper into the structure of T.   (I believe there are
examples where the function does something sane, and the strictness
analyser still diverges, but I can't see one now.)

Now, concerning (1), the FC2 branch currently adds a coercion for ALL
newtypes.  I did this as an experiment, to try to expose cases in which
the coercions got in the way of optimisations.  If it turns out that we
can indeed always use a coercion, then we don't risk recursive types,
and don't need to figure out what the loop breakers are.

For newtype *families* though, we will always have a coercion, so they
are always loop breakers!  So you can easily adjust the current
algorithm by simply treating all newtype families as loop breakers (and
indeed type families).  I think.
132

133
\begin{code}
134
tcTyAndClassDecls :: ModDetails -> [LTyClDecl Name]
135 136
   	           -> TcM TcGblEnv 	-- Input env extended by types and classes 
					-- and their implicit Ids,DataCons
137 138
-- Fails if there are any errors

139
tcTyAndClassDecls boot_details allDecls
140 141 142
  = checkNoErrs $ 	-- The code recovers internally, but if anything gave rise to
			-- an error we'd better stop now, to avoid a cascade
    do	{       -- Omit instances of type families; they are handled together
143
		-- with the *heads* of class instances
144
        ; let decls = filter (not . isFamInstDecl . unLoc) allDecls
145 146

        	-- First check for cyclic type synonysm or classes
147
		-- See notes with checkCycleErrs
148
	; checkCycleErrs decls
149
	; mod <- getModule
150
	; traceTc (text "tcTyAndCl" <+> ppr mod)
Ian Lynagh's avatar
Ian Lynagh committed
151
	; (syn_tycons, alg_tyclss) <- fixM (\ ~(_rec_syn_tycons, rec_alg_tyclss) ->
152 153 154 155 156
	  do	{ let {	-- Seperate ordinary synonyms from all other type and
			-- class declarations and add all associated type
			-- declarations from type classes.  The latter is
			-- required so that the temporary environment for the
			-- knot includes all associated family declarations.
157
		      ; (syn_decls, alg_decls) = partition (isSynDecl . unLoc)
158 159 160
						   decls
		      ; alg_at_decls           = concatMap addATs alg_decls
		      }
161 162 163
			-- Extend the global env with the knot-tied results
			-- for data types and classes
			-- 
164 165 166 167 168
			-- We must populate the environment with the loop-tied
			-- T's right away, because the kind checker may "fault
			-- in" some type  constructors that recursively
			-- mention T
		; let gbl_things = mkGlobalThings alg_at_decls rec_alg_tyclss
169 170 171 172 173
		; tcExtendRecEnv gbl_things $ do

			-- Kind-check the declarations
		{ (kc_syn_decls, kc_alg_decls) <- kcTyClDecls syn_decls alg_decls

174 175
		; let {	-- Calculate rec-flag
		      ; calc_rec  = calcRecFlags boot_details rec_alg_tyclss
176
		      ; tc_decl   = addLocM (tcTyClDecl calc_rec) }
177

178
			-- Type-check the type synonyms, and extend the envt
179
		; syn_tycons <- tcSynDecls kc_syn_decls
180 181 182
		; tcExtendGlobalEnv syn_tycons $ do

			-- Type-check the data types and classes
183
		{ alg_tyclss <- mapM tc_decl kc_alg_decls
184
		; return (syn_tycons, concat alg_tyclss)
185
	    }}})
186 187
	-- Finished with knot-tying now
	-- Extend the environment with the finished things
188
	; tcExtendGlobalEnv (syn_tycons ++ alg_tyclss) $ do
189 190 191

	-- Perform the validity check
	{ traceTc (text "ready for validity check")
192
	; mapM_ (addLocM checkValidTyCl) decls
193
 	; traceTc (text "done")
194
   
195 196 197
	-- Add the implicit things;
	-- we want them in the environment because 
	-- they may be mentioned in interface files
198 199 200
	-- NB: All associated types and their implicit things will be added a
	--     second time here.  This doesn't matter as the definitions are
	--     the same.
201
	; let {	implicit_things = concatMap implicitTyThings alg_tyclss }
202 203
	; traceTc ((text "Adding" <+> ppr alg_tyclss) 
		   $$ (text "and" <+> ppr implicit_things))
204 205
  	; tcExtendGlobalEnv implicit_things getGblEnv
    }}
206
  where
207 208 209 210 211
    -- Pull associated types out of class declarations, to tie them into the
    -- knot above.  
    -- NB: We put them in the same place in the list as `tcTyClDecl' will
    --	   eventually put the matching `TyThing's.  That's crucial; otherwise,
    --	   the two argument lists of `mkGlobalThings' don't match up.
212 213
    addATs decl@(L _ (ClassDecl {tcdATs = ats})) = decl : ats
    addATs decl				         = [decl]
214

215
mkGlobalThings :: [LTyClDecl Name] 	-- The decls
216 217 218 219 220 221
	       -> [TyThing]		-- Knot-tied, in 1-1 correspondence with the decls
	       -> [(Name,TyThing)]
-- Driven by the Decls, and treating the TyThings lazily
-- make a TypeEnv for the new things
mkGlobalThings decls things
  = map mk_thing (decls `zipLazy` things)
222
  where
223
    mk_thing (L _ (ClassDecl {tcdLName = L _ name}), ~(AClass cl))
224
	 = (name, AClass cl)
225
    mk_thing (L _ decl, ~(ATyCon tc))
226
         = (tcdName decl, ATyCon tc)
Ian Lynagh's avatar
Ian Lynagh committed
227 228 229 230
#if __GLASGOW_HASKELL__ < 605
-- Old GHCs don't understand that ~... matches anything
    mk_thing _ = panic "mkGlobalThings: Can't happen"
#endif
231
\end{code}
232 233


234 235
%************************************************************************
%*									*
236
\subsection{Type checking family instances}
237 238 239
%*									*
%************************************************************************

240 241 242 243
Family instances are somewhat of a hybrid.  They are processed together with
class instance heads, but can contain data constructors and hence they share a
lot of kinding and type checking code with ordinary algebraic data types (and
GADTs).
244 245

\begin{code}
246 247
tcFamInstDecl :: LTyClDecl Name -> TcM (Maybe TyThing)   -- Nothing if error
tcFamInstDecl (L loc decl)
248
  =	-- Prime error recovery, set source location
249
    recoverM (return Nothing)		        $
250 251
    setSrcSpan loc				$
    tcAddDeclCtxt decl				$
252
    do { -- type families require -XTypeFamilies and can't be in an
253
	 -- hs-boot file
Ian Lynagh's avatar
Ian Lynagh committed
254
       ; type_families <- doptM Opt_TypeFamilies
255
       ; is_boot  <- tcIsHsBoot	  -- Are we compiling an hs-boot file?
Ian Lynagh's avatar
Ian Lynagh committed
256
       ; checkTc type_families $ badFamInstDecl (tcdLName decl)
257
       ; checkTc (not is_boot) $ badBootFamInstDeclErr
258

259 260 261 262 263
	 -- Perform kind and type checking
       ; tc <- tcFamInstDecl1 decl
       ; checkValidTyCon tc	-- Remember to check validity;
				-- no recursion to worry about here
       ; return (Just (ATyCon tc))
264 265
       }

266
tcFamInstDecl1 :: TyClDecl Name -> TcM TyCon
267

268 269
  -- "type instance"
tcFamInstDecl1 (decl@TySynonym {tcdLName = L loc tc_name})
270 271 272 273 274
  = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
    do { -- check that the family declaration is for a synonym
	 unless (isSynTyCon family) $
	   addErr (wrongKindOfFamily family)

275
       ; -- (1) kind check the right-hand side of the type equation
276 277
       ; k_rhs <- kcCheckHsType (tcdSynRhs decl) resKind

278 279
         -- we need the exact same number of type parameters as the family
         -- declaration 
280
       ; let famArity = tyConArity family
281 282
       ; checkTc (length k_typats == famArity) $ 
           wrongNumberOfParmsErr famArity
283

284 285
         -- (2) type check type equation
       ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
286
       ; t_typats <- mapM tcHsKindedType k_typats
287 288
       ; t_rhs    <- tcHsKindedType k_rhs

289
         -- (3) check the well-formedness of the instance
290
       ; checkValidTypeInst t_typats t_rhs
291 292

         -- (4) construct representation tycon
293
       ; rep_tc_name <- newFamInstTyConName tc_name loc
294 295
       ; buildSynTyCon rep_tc_name t_tvs (SynonymTyCon t_rhs) 
                       (Just (family, t_typats))
296
       }}
297 298

  -- "newtype instance" and "data instance"
299 300
tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
			     tcdCons = cons})
301
  = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
302
    do { -- check that the family declaration is for the right kind
303
	 unless (isAlgTyCon family) $
304 305 306
	   addErr (wrongKindOfFamily family)

       ; -- (1) kind check the data declaration as usual
307
       ; k_decl <- kcDataDecl decl k_tvs
308 309
       ; let k_ctxt = tcdCtxt k_decl
	     k_cons = tcdCons k_decl
310 311

         -- result kind must be '*' (otherwise, we have too few patterns)
312
       ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr (tyConArity family)
313

314 315
         -- (2) type check indexed data type declaration
       ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
316 317
       ; unbox_strict <- doptM Opt_UnboxStrictFields

318
         -- kind check the type indexes and the context
319
       ; t_typats     <- mapM tcHsKindedType k_typats
320 321 322 323
       ; stupid_theta <- tcHsKindedContext k_ctxt

         -- (3) Check that
         --     - left-hand side contains no type family applications
324 325
         --       (vanilla synonyms are fine, though, and we checked for
         --       foralls earlier)
326
       ; mapM_ checkTyFamFreeness t_typats
327 328

	 --     - we don't use GADT syntax for indexed types
329 330
       ; checkTc h98_syntax (badGadtIdxTyDecl tc_name)

331
	 --     - a newtype has exactly one constructor
332 333
       ; checkTc (new_or_data == DataType || isSingleton k_cons) $
	   newtypeConError tc_name (length k_cons)
334

335
         -- (4) construct representation tycon
336
       ; rep_tc_name <- newFamInstTyConName tc_name loc
337
       ; let ex_ok = True	-- Existentials ok for type families!
338
       ; fixM (\ tycon -> do 
339
	     { data_cons <- mapM (addLocM (tcConDecl unbox_strict ex_ok tycon t_tvs))
340 341 342 343
				  k_cons
	     ; tc_rhs <-
		 case new_or_data of
		   DataType -> return (mkDataTyConRhs data_cons)
344
		   NewType  -> ASSERT( not (null data_cons) )
345
			       mkNewTyConRhs rep_tc_name tycon (head data_cons)
346 347
	     ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
			     False h98_syntax (Just (family, t_typats))
348 349 350 351 352 353 354 355 356 357
                 -- We always assume that indexed types are recursive.  Why?
                 -- (1) Due to their open nature, we can never be sure that a
                 -- further instance might not introduce a new recursive
                 -- dependency.  (2) They are always valid loop breakers as
                 -- they involve a coercion.
	     })
       }}
       where
	 h98_syntax = case cons of 	-- All constructors have same shape
			L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
Ian Lynagh's avatar
Ian Lynagh committed
358 359 360
			_ -> True

tcFamInstDecl1 d = pprPanic "tcFamInstDecl1" (ppr d)
361 362 363 364 365 366 367 368

-- Kind checking of indexed types
-- -

-- Kind check type patterns and kind annotate the embedded type variables.
--
-- * Here we check that a type instance matches its kind signature, but we do
--   not check whether there is a pattern for each type index; the latter
369
--   check is only required for type synonym instances.
370 371
--
kcIdxTyPats :: TyClDecl Name
372
	    -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a)
373 374 375 376
	       -- ^^kinded tvs         ^^kinded ty pats  ^^res kind
	    -> TcM a
kcIdxTyPats decl thing_inside
  = kcHsTyVars (tcdTyVars decl) $ \tvs -> 
377 378
    do { family <- tcLookupLocatedTyCon (tcdLName decl)
       ; let { (kinds, resKind) = splitKindFunTys (tyConKind family)
379
	     ; hs_typats	= fromJust $ tcdTyPats decl }
380 381 382 383 384 385 386

         -- we may not have more parameters than the kind indicates
       ; checkTc (length kinds >= length hs_typats) $
	   tooManyParmsErr (tcdLName decl)

         -- type functions can have a higher-kinded result
       ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
387
       ; typats <- zipWithM kcCheckHsType hs_typats kinds
388
       ; thing_inside tvs typats resultKind family
389
       }
390
  where
391 392 393
\end{code}


394 395
%************************************************************************
%*									*
396
		Kind checking
397 398
%*									*
%************************************************************************
399

400 401
We need to kind check all types in the mutually recursive group
before we know the kind of the type variables.  For example:
402 403 404 405 406 407 408 409 410 411 412

class C a where
   op :: D b => a -> b -> b

class D c where
   bop :: (Monad c) => ...

Here, the kind of the locally-polymorphic type variable "b"
depends on *all the uses of class D*.  For example, the use of
Monad c in bop's type signature means that D must have kind Type->Type.

413 414 415 416 417 418 419 420
However type synonyms work differently.  They can have kinds which don't
just involve (->) and *:
	type R = Int#		-- Kind #
	type S a = Array# a	-- Kind * -> #
	type T a b = (# a,b #)	-- Kind * -> * -> (# a,b #)
So we must infer their kinds from their right-hand sides *first* and then
use them, whereas for the mutually recursive data types D we bring into
scope kind bindings D -> k, where k is a kind variable, and do inference.
421

422
Type families
423 424 425 426
~~~~~~~~~~~~~
This treatment of type synonyms only applies to Haskell 98-style synonyms.
General type functions can be recursive, and hence, appear in `alg_decls'.

427
The kind of a type family is solely determinded by its kind signature;
428 429
hence, only kind signatures participate in the construction of the initial
kind environment (as constructed by `getInitialKind').  In fact, we ignore
430 431
instances of families altogether in the following.  However, we need to
include the kinds of associated families into the construction of the
432 433
initial kind environment.  (This is handled by `allDecls').

434
\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
435 436
kcTyClDecls :: [LTyClDecl Name] -> [Located (TyClDecl Name)]
            -> TcM ([LTyClDecl Name], [Located (TyClDecl Name)])
437
kcTyClDecls syn_decls alg_decls
438 439 440
  = do	{ 	-- First extend the kind env with each data type, class, and
		-- indexed type, mapping them to a type variable
          let initialKindDecls = concat [allDecls decl | L _ decl <- alg_decls]
441
	; alg_kinds <- mapM getInitialKind initialKindDecls
442 443 444 445 446 447 448 449 450 451 452
	; tcExtendKindEnv alg_kinds $ do

		-- Now kind-check the type synonyms, in dependency order
		-- We do these differently to data type and classes,
		-- because a type synonym can be an unboxed type
		--	type Foo = Int#
		-- and a kind variable can't unify with UnboxedTypeKind
		-- So we infer their kinds in dependency order
	{ (kc_syn_decls, syn_kinds) <- kcSynDecls (calcSynCycles syn_decls)
	; tcExtendKindEnv syn_kinds $  do

453 454 455 456
		-- Now kind-check the data type, class, and kind signatures,
		-- returning kind-annotated decls; we don't kind-check
		-- instances of indexed types yet, but leave this to
		-- `tcInstDecls1'
457
	{ kc_alg_decls <- mapM (wrapLocM kcTyClDecl)
458
			    (filter (not . isFamInstDecl . unLoc) alg_decls)
459 460

	; return (kc_syn_decls, kc_alg_decls) }}}
461 462 463 464 465
  where
    -- get all declarations relevant for determining the initial kind
    -- environment
    allDecls (decl@ClassDecl {tcdATs = ats}) = decl : [ at 
						      | L _ at <- ats
466 467 468
						      , isFamilyDecl at]
    allDecls decl | isFamInstDecl decl = []
		  | otherwise	       = [decl]
469

470
------------------------------------------------------------------------
471 472 473
getInitialKind :: TyClDecl Name -> TcM (Name, TcKind)
-- Only for data type, class, and indexed type declarations
-- Get as much info as possible from the data, class, or indexed type decl,
474
-- so as to maximise usefulness of error messages
475
getInitialKind decl
476 477 478 479 480 481 482
  = do 	{ arg_kinds <- mapM (mk_arg_kind . unLoc) (tyClDeclTyVars decl)
	; res_kind  <- mk_res_kind decl
	; return (tcdName decl, mkArrowKinds arg_kinds res_kind) }
  where
    mk_arg_kind (UserTyVar _)        = newKindVar
    mk_arg_kind (KindedTyVar _ kind) = return kind

483 484 485
    mk_res_kind (TyFamily { tcdKind    = Just kind }) = return kind
    mk_res_kind (TyData   { tcdKindSig = Just kind }) = return kind
	-- On GADT-style declarations we allow a kind signature
486
	--	data T :: *->* where { ... }
Ian Lynagh's avatar
Ian Lynagh committed
487
    mk_res_kind _ = return liftedTypeKind
488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504


----------------
kcSynDecls :: [SCC (LTyClDecl Name)] 
	   -> TcM ([LTyClDecl Name], 	-- Kind-annotated decls
		   [(Name,TcKind)])	-- Kind bindings
kcSynDecls []
  = return ([], [])
kcSynDecls (group : groups)
  = do	{ (decl,  nk)  <- kcSynDecl group
	; (decls, nks) <- tcExtendKindEnv [nk] (kcSynDecls groups)
	; return (decl:decls, nk:nks) }
			
----------------
kcSynDecl :: SCC (LTyClDecl Name) 
	   -> TcM (LTyClDecl Name, 	-- Kind-annotated decls
		   (Name,TcKind))	-- Kind bindings
Ian Lynagh's avatar
Ian Lynagh committed
505
kcSynDecl (AcyclicSCC (L loc decl))
506 507 508 509 510 511 512 513 514 515 516 517 518
  = tcAddDeclCtxt decl	$
    kcHsTyVars (tcdTyVars decl) (\ k_tvs ->
    do { traceTc (text "kcd1" <+> ppr (unLoc (tcdLName decl)) <+> brackets (ppr (tcdTyVars decl)) 
			<+> brackets (ppr k_tvs))
       ; (k_rhs, rhs_kind) <- kcHsType (tcdSynRhs decl)
       ; traceTc (text "kcd2" <+> ppr (unLoc (tcdLName decl)))
       ; let tc_kind = foldr (mkArrowKind . kindedTyVarKind) rhs_kind k_tvs
       ; return (L loc (decl { tcdTyVars = k_tvs, tcdSynRhs = k_rhs }),
		 (unLoc (tcdLName decl), tc_kind)) })

kcSynDecl (CyclicSCC decls)
  = do { recSynErr decls; failM }	-- Fail here to avoid error cascade
					-- of out-of-scope tycons
519

Ian Lynagh's avatar
Ian Lynagh committed
520
kindedTyVarKind :: LHsTyVarBndr Name -> Kind
521
kindedTyVarKind (L _ (KindedTyVar _ k)) = k
Ian Lynagh's avatar
Ian Lynagh committed
522
kindedTyVarKind x = pprPanic "kindedTyVarKind" (ppr x)
523

524 525 526
------------------------------------------------------------------------
kcTyClDecl :: TyClDecl Name -> TcM (TyClDecl Name)
	-- Not used for type synonyms (see kcSynDecl)
527

528
kcTyClDecl decl@(TyData {})
529
  = ASSERT( not . isFamInstDecl $ decl )   -- must not be a family instance
530 531
    kcTyClDeclBody decl	$
      kcDataDecl decl
532

533 534
kcTyClDecl decl@(TyFamily {})
  = kcFamilyDecl [] decl      -- the empty list signals a toplevel decl      
535

536
kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats})
537
  = kcTyClDeclBody decl	$ \ tvs' ->
Ian Lynagh's avatar
Ian Lynagh committed
538
    do	{ ctxt' <- kcHsContext ctxt	
539 540
	; ats'  <- mapM (wrapLocM (kcFamilyDecl tvs')) ats
	; sigs' <- mapM (wrapLocM kc_sig) sigs
541 542
	; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdSigs = sigs',
		        tcdATs = ats'}) }
543
  where
544 545
    kc_sig (TypeSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
				   ; return (TypeSig nm op_ty') }
546 547
    kc_sig other_sig	      = return other_sig

548
kcTyClDecl decl@(ForeignType {})
549 550
  = return decl

Ian Lynagh's avatar
Ian Lynagh committed
551 552
kcTyClDecl (TySynonym {}) = panic "kcTyClDecl TySynonym"

553
kcTyClDeclBody :: TyClDecl Name
554
	       -> ([LHsTyVarBndr Name] -> TcM a)
555
	       -> TcM a
556 557 558 559
-- getInitialKind has made a suitably-shaped kind for the type or class
-- Unpack it, and attribute those kinds to the type variables
-- Extend the env with bindings for the tyvars, taken from
-- the kind of the tycon/class.  Give it to the thing inside, and 
560
-- check the result kind matches
561
kcTyClDeclBody decl thing_inside
562
  = tcAddDeclCtxt decl		$
563
    do 	{ tc_ty_thing <- tcLookupLocated (tcdLName decl)
Ian Lynagh's avatar
Ian Lynagh committed
564 565 566
	; let tc_kind	 = case tc_ty_thing of
                           AThing k -> k
                           _ -> pprPanic "kcTyClDeclBody" (ppr tc_ty_thing)
567 568 569 570 571 572
	      (kinds, _) = splitKindFunTys tc_kind
	      hs_tvs 	 = tcdTyVars decl
	      kinded_tvs = ASSERT( length kinds >= length hs_tvs )
			   [ L loc (KindedTyVar (hsTyVarName tv) k)
			   | (L loc tv, k) <- zip hs_tvs kinds]
	; tcExtendKindEnvTvs kinded_tvs (thing_inside kinded_tvs) }
573 574 575 576 577 578 579 580 581

-- Kind check a data declaration, assuming that we already extended the
-- kind environment with the type variables of the left-hand side (these
-- kinded type variables are also passed as the second parameter).
--
kcDataDecl :: TyClDecl Name -> [LHsTyVarBndr Name] -> TcM (TyClDecl Name)
kcDataDecl decl@(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdCons = cons})
	   tvs
  = do	{ ctxt' <- kcHsContext ctxt	
582
	; cons' <- mapM (wrapLocM kc_con_decl) cons
583 584
	; return (decl {tcdTyVars = tvs, tcdCtxt = ctxt', tcdCons = cons'}) }
  where
585 586
    -- doc comments are typechecked to Nothing here
    kc_con_decl (ConDecl name expl ex_tvs ex_ctxt details res _) = do
587 588 589 590 591 592
      kcHsTyVars ex_tvs $ \ex_tvs' -> do
        ex_ctxt' <- kcHsContext ex_ctxt
        details' <- kc_con_details details 
        res'     <- case res of
          ResTyH98 -> return ResTyH98
          ResTyGADT ty -> do { ty' <- kcHsSigType ty; return (ResTyGADT ty') }
593
        return (ConDecl name expl ex_tvs' ex_ctxt' details' res' Nothing)
594 595

    kc_con_details (PrefixCon btys) 
596
	= do { btys' <- mapM kc_larg_ty btys 
597
             ; return (PrefixCon btys') }
598
    kc_con_details (InfixCon bty1 bty2) 
599 600 601
	= do { bty1' <- kc_larg_ty bty1
             ; bty2' <- kc_larg_ty bty2
             ; return (InfixCon bty1' bty2') }
602
    kc_con_details (RecCon fields) 
603
	= do { fields' <- mapM kc_field fields
604
             ; return (RecCon fields') }
605

606 607
    kc_field (ConDeclField fld bty d) = do { bty' <- kc_larg_ty bty
					   ; return (ConDeclField fld bty' d) }
608 609 610 611 612 613 614

    kc_larg_ty bty = case new_or_data of
			DataType -> kcHsSigType bty
			NewType  -> kcHsLiftedSigType bty
	-- Can't allow an unlifted type for newtypes, because we're effectively
	-- going to remove the constructor while coercing it to a lifted type.
	-- And newtypes can't be bang'd
Ian Lynagh's avatar
Ian Lynagh committed
615
kcDataDecl d _ = pprPanic "kcDataDecl" (ppr d)
616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631

-- Kind check a family declaration or type family default declaration.
--
kcFamilyDecl :: [LHsTyVarBndr Name]  -- tyvars of enclosing class decl if any
             -> TyClDecl Name -> TcM (TyClDecl Name)
kcFamilyDecl classTvs decl@(TyFamily {tcdKind = kind})
  = kcTyClDeclBody decl $ \tvs' ->
    do { mapM_ unifyClassParmKinds tvs'
       ; return (decl {tcdTyVars = tvs', 
		       tcdKind = kind `mplus` Just liftedTypeKind})
		       -- default result kind is '*'
       }
  where
    unifyClassParmKinds (L _ (KindedTyVar n k))
      | Just classParmKind <- lookup n classTyKinds = unifyKind k classParmKind
      | otherwise                                   = return ()
Ian Lynagh's avatar
Ian Lynagh committed
632
    unifyClassParmKinds x = pprPanic "kcFamilyDecl/unifyClassParmKinds" (ppr x)
633
    classTyKinds = [(n, k) | L _ (KindedTyVar n k) <- classTvs]
Ian Lynagh's avatar
Ian Lynagh committed
634
kcFamilyDecl _ (TySynonym {})              -- type family defaults
635
  = panic "TcTyClsDecls.kcFamilyDecl: not implemented yet"
Ian Lynagh's avatar
Ian Lynagh committed
636
kcFamilyDecl _ d = pprPanic "kcFamilyDecl" (ppr d)
637 638 639 640 641
\end{code}


%************************************************************************
%*									*
642
\subsection{Type checking}
643 644
%*									*
%************************************************************************
645 646

\begin{code}
647 648 649 650 651
tcSynDecls :: [LTyClDecl Name] -> TcM [TyThing]
tcSynDecls [] = return []
tcSynDecls (decl : decls) 
  = do { syn_tc <- addLocM tcSynDecl decl
       ; syn_tcs <- tcExtendGlobalEnv [syn_tc] (tcSynDecls decls)
652 653
       ; return (syn_tc : syn_tcs) }

654
  -- "type"
Ian Lynagh's avatar
Ian Lynagh committed
655
tcSynDecl :: TyClDecl Name -> TcM TyThing
656
tcSynDecl
657 658 659 660
  (TySynonym {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdSynRhs = rhs_ty})
  = tcTyVarBndrs tvs		$ \ tvs' -> do 
    { traceTc (text "tcd1" <+> ppr tc_name) 
    ; rhs_ty' <- tcHsKindedType rhs_ty
661 662 663
    ; tycon <- buildSynTyCon tc_name tvs' (SynonymTyCon rhs_ty') Nothing
    ; return (ATyCon tycon) 
    }
Ian Lynagh's avatar
Ian Lynagh committed
664
tcSynDecl d = pprPanic "tcSynDecl" (ppr d)
665 666

--------------------
667
tcTyClDecl :: (Name -> RecFlag) -> TyClDecl Name -> TcM [TyThing]
668

669 670
tcTyClDecl calc_isrec decl
  = tcAddDeclCtxt decl (tcTyClDecl1 calc_isrec decl)
671

672
  -- "type family" declarations
Ian Lynagh's avatar
Ian Lynagh committed
673
tcTyClDecl1 :: (Name -> RecFlag) -> TyClDecl Name -> TcM [TyThing]
674
tcTyClDecl1 _calc_isrec 
675 676 677 678 679
  (TyFamily {tcdFlavour = TypeFamily, 
	     tcdLName = L _ tc_name, tcdTyVars = tvs, tcdKind = Just kind})
						      -- NB: kind at latest
						      --     added during
						      --     kind checking
680
  = tcTyVarBndrs tvs  $ \ tvs' -> do 
681
  { traceTc (text "type family: " <+> ppr tc_name) 
682
  ; idx_tys <- doptM Opt_TypeFamilies
683

684
	-- Check that we don't use families without -XTypeFamilies
685
  ; checkTc idx_tys $ badFamInstDecl tc_name
686

687 688
  ; tycon <- buildSynTyCon tc_name tvs' (OpenSynTyCon kind Nothing) Nothing
  ; return [ATyCon tycon]
689
  }
690

691
  -- "data family" declaration
692
tcTyClDecl1 _calc_isrec 
693
  (TyFamily {tcdFlavour = DataFamily, 
694
	     tcdLName = L _ tc_name, tcdTyVars = tvs, tcdKind = mb_kind})
695
  = tcTyVarBndrs tvs  $ \ tvs' -> do 
696
  { traceTc (text "data family: " <+> ppr tc_name) 
697
  ; extra_tvs <- tcDataKindSig mb_kind
698 699
  ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these

700
  ; idx_tys <- doptM Opt_TypeFamilies
701

702
	-- Check that we don't use families without -XTypeFamilies
703
  ; checkTc idx_tys $ badFamInstDecl tc_name
704 705

  ; tycon <- buildAlgTyCon tc_name final_tvs [] 
706
	       mkOpenDataTyConRhs Recursive False True Nothing
707
  ; return [ATyCon tycon]
708 709
  }

710
  -- "newtype" and "data"
711
  -- NB: not used for newtype/data instances (whether associated or not)
712
tcTyClDecl1 calc_isrec
713
  (TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
714 715 716 717
	   tcdLName = L _ tc_name, tcdKindSig = mb_ksig, tcdCons = cons})
  = tcTyVarBndrs tvs	$ \ tvs' -> do 
  { extra_tvs <- tcDataKindSig mb_ksig
  ; let final_tvs = tvs' ++ extra_tvs
718
  ; stupid_theta <- tcHsKindedContext ctxt
719
  ; want_generic <- doptM Opt_Generics
720
  ; unbox_strict <- doptM Opt_UnboxStrictFields
Ian Lynagh's avatar
Ian Lynagh committed
721
  ; empty_data_decls <- doptM Opt_EmptyDataDecls
Ian Lynagh's avatar
Ian Lynagh committed
722
  ; kind_signatures <- doptM Opt_KindSignatures
723
  ; existential_ok <- doptM Opt_ExistentialQuantification
724
  ; gadt_ok      <- doptM Opt_GADTs
725
  ; is_boot	 <- tcIsHsBoot	-- Are we compiling an hs-boot file?
726
  ; let ex_ok = existential_ok || gadt_ok	-- Data cons can have existential context
727 728

	-- Check that we don't use GADT syntax in H98 world
729
  ; checkTc (gadt_ok || h98_syntax) (badGadtDecl tc_name)
730

731
	-- Check that we don't use kind signatures without Glasgow extensions
Ian Lynagh's avatar
Ian Lynagh committed
732
  ; checkTc (kind_signatures || isNothing mb_ksig) (badSigTyDecl tc_name)
733

734 735 736
	-- Check that the stupid theta is empty for a GADT-style declaration
  ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)

737 738 739 740 741 742
	-- Check that a newtype has exactly one constructor
	-- Do this before checking for empty data decls, so that
	-- we don't suggest -XEmptyDataDecls for newtypes
  ; checkTc (new_or_data == DataType || isSingleton cons) 
	    (newtypeConError tc_name (length cons))

743
	-- Check that there's at least one condecl,
Ian Lynagh's avatar
Ian Lynagh committed
744 745
	-- or else we're reading an hs-boot file, or -XEmptyDataDecls
  ; checkTc (not (null cons) || empty_data_decls || is_boot)
746 747
	    (emptyConDeclsErr tc_name)
    
748
  ; tycon <- fixM (\ tycon -> do 
749
	{ data_cons <- mapM (addLocM (tcConDecl unbox_strict ex_ok tycon final_tvs))
750
			     cons
751 752 753 754 755 756
	; tc_rhs <-
	    if null cons && is_boot 	-- In a hs-boot file, empty cons means
	    then return AbstractTyCon	-- "don't know"; hence Abstract
	    else case new_or_data of
		   DataType -> return (mkDataTyConRhs data_cons)
		   NewType  -> 
757
                       ASSERT( not (null data_cons) )
758
                       mkNewTyConRhs tc_name tycon (head data_cons)
759
	; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
760
	    (want_generic && canDoGenerics data_cons) h98_syntax Nothing
761
	})
762
  ; return [ATyCon tycon]
763
  }
764
  where
765
    is_rec   = calc_isrec tc_name
766
    h98_syntax = case cons of 	-- All constructors have same shape
767
			L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
Ian Lynagh's avatar
Ian Lynagh committed
768
			_ -> True
769

770
tcTyClDecl1 calc_isrec 
771
  (ClassDecl {tcdLName = L _ class_name, tcdTyVars = tvs, 
772
	      tcdCtxt = ctxt, tcdMeths = meths,
773
	      tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
774 775
  = tcTyVarBndrs tvs		$ \ tvs' -> do 
  { ctxt' <- tcHsKindedContext ctxt
776 777
  ; fds' <- mapM (addLocM tc_fundep) fundeps
  ; atss <- mapM (addLocM (tcTyClDecl1 (const Recursive))) ats
778 779
            -- NB: 'ats' only contains "type family" and "data family"
            --     declarations as well as type family defaults
780
  ; let ats' = zipWith setTyThingPoss atss (map (tcdTyVars . unLoc) ats)
781 782 783 784
  ; sig_stuff <- tcClassSigs class_name sigs meths
  ; clas <- fixM (\ clas ->
		let 	-- This little knot is just so we can get
			-- hold of the name of the class TyCon, which we
785
			-- need to look up its recursiveness
786 787 788
		    tycon_name = tyConName (classTyCon clas)
		    tc_isrec = calc_isrec tycon_name
		in
789 790
		buildClass False {- Must include unfoldings for selectors -}
			   class_name tvs' ctxt' fds' ats'
791
			   sig_stuff tc_isrec)
792 793 794 795
  ; return (AClass clas : ats')
      -- NB: Order is important due to the call to `mkGlobalThings' when
      --     tying the the type and class declaration type checking knot.
  }
796
  where
797 798
    tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tcLookupTyVar tvs1 ;
				; tvs2' <- mapM tcLookupTyVar tvs2 ;
799
				; return (tvs1', tvs2') }
800

801 802 803
    -- For each AT argument compute the position of the corresponding class
    -- parameter in the class head.  This will later serve as a permutation
    -- vector when checking the validity of instance declarations.
804 805 806 807 808 809 810 811 812
    setTyThingPoss [ATyCon tycon] atTyVars = 
      let classTyVars = hsLTyVarNames tvs
	  poss        =   catMaybes 
			. map (`elemIndex` classTyVars) 
			. hsLTyVarNames 
			$ atTyVars
		     -- There will be no Nothing, as we already passed renaming
      in 
      ATyCon (setTyConArgPoss tycon poss)
813
    setTyThingPoss _		  _ = panic "TcTyClsDecls.setTyThingPoss"
814

Ian Lynagh's avatar
Ian Lynagh committed
815
tcTyClDecl1 _
816
  (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
817
  = return [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
818

Ian Lynagh's avatar
Ian Lynagh committed
819 820
tcTyClDecl1 _ d = pprPanic "tcTyClDecl1" (ppr d)

821
-----------------------------------
822
tcConDecl :: Bool 		-- True <=> -funbox-strict_fields
823
	  -> Bool		-- True <=> -XExistentialQuantificaton or -XGADTs
824 825 826
	  -> TyCon -> [TyVar] 
	  -> ConDecl Name 
	  -> TcM DataCon
827

828
tcConDecl unbox_strict existential_ok tycon tc_tvs	-- Data types
829
	  (ConDecl name _ tvs ctxt details res_ty _)
830 831
  = addErrCtxt (dataConCtxt name)	$ 
    tcTyVarBndrs tvs			$ \ tvs' -> do 
832
    { ctxt' <- tcHsKindedContext ctxt
833 834
    ; checkTc (existential_ok || (null tvs && null (unLoc ctxt)))
	      (badExistential name)
835
    ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
836
    ; let 
837
	-- Tiresome: tidy the tyvar binders, since tc_tvs and tvs' may have the same OccNames
838
	tc_datacon is_infix field_lbls btys
839
	  = do { let bangs = map getBangStrictness btys
840
	       ; arg_tys <- mapM tcHsBangType btys
841
    	       ; buildDataCon (unLoc name) is_infix
842
    		    (argStrictness unbox_strict bangs arg_tys)
843
    		    (map unLoc field_lbls)
844
    		    univ_tvs ex_tvs eq_preds ctxt' arg_tys
845
		    data_tc }
846 847 848
		-- NB:	we put data_tc, the type constructor gotten from the
		--	constructor type signature into the data constructor;
		--	that way checkValidDataCon can complain if it's wrong.
849

850
    ; case details of
851
	PrefixCon btys     -> tc_datacon False [] btys
852 853 854
	InfixCon bty1 bty2 -> tc_datacon True  [] [bty1,bty2]
	RecCon fields      -> tc_datacon False field_names btys
			   where
855 856
			      field_names = map cd_fld_name fields
			      btys        = map cd_fld_type fields
857 858
    }

859 860 861 862 863
tcResultType :: TyCon
	     -> [TyVar] 	-- data T a b c = ...
	     -> [TyVar] 	-- where MkT :: forall a b c. ...
	     -> ResType Name
	     -> TcM ([TyVar],	 	-- Universal
864
		     [TyVar],		-- Existential (distinct OccNames from univs)
865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883
		     [(TyVar,Type)],	-- Equality predicates
		     TyCon)		-- TyCon given in the ResTy
	-- We don't check that the TyCon given in the ResTy is
	-- the same as the parent tycon, becuase we are in the middle
	-- of a recursive knot; so it's postponed until checkValidDataCon

tcResultType decl_tycon tc_tvs dc_tvs ResTyH98
  = return (tc_tvs, dc_tvs, [], decl_tycon)
	-- In H98 syntax the dc_tvs are the existential ones
	--	data T a b c = forall d e. MkT ...
	-- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs

tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
	-- E.g.  data T a b c where
	--	   MkT :: forall x y z. T (x,y) z z
	-- Then we generate
	--	([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)

  = do	{ (dc_tycon, res_tys) <- tcLHsConResTy res_ty
884 885

	; let univ_tvs = choose_univs [] tidy_tc_tvs res_tys
886 887 888 889 890