4affd91663e0cd23c9b0c371a6236cbbc419806c
[ghc.git] / compiler / typecheck / TcHsType.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
6
7 \begin{code}
8 module TcHsType (
9         tcHsSigType, tcHsSigTypeNC, tcHsDeriv, 
10         tcHsInstHead, tcHsQuantifiedType,
11         UserTypeCtxt(..), 
12
13                 -- Kind checking
14         kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
15         kcLHsType, kcCheckLHsType, kcHsContext, kcApps,
16         
17                 -- Typechecking kinded types
18         tcHsKindedContext, tcHsKindedType, tcHsBangType,
19         tcTyVarBndrs, dsHsType,
20         tcDataKindSig,
21
22         ExpKind(..), EkCtxt(..), ekConstraint,
23         checkExpectedKind,
24
25                 -- Pattern type signatures
26         tcHsPatSigType, tcPatSig
27    ) where
28
29 #include "HsVersions.h"
30
31 #ifdef GHCI     /* Only if bootstrapped */
32 import {-# SOURCE #-}   TcSplice( kcSpliceType )
33 #endif
34
35 import HsSyn
36 import RnHsSyn
37 import TcRnMonad
38 import TcEnv
39 import TcMType
40 import TcUnify
41 import TcIface
42 import TcType
43 import {- Kind parts of -} Type
44 import Kind ( isConstraintKind )
45 import Var
46 import VarSet
47 import TyCon
48 import Class
49 import Name
50 import NameSet
51 import TysWiredIn
52 import BasicTypes
53 import SrcLoc
54 import DynFlags ( ExtensionFlag( Opt_ConstraintKinds ) )
55 import Util
56 import UniqSupply
57 import Outputable
58 import FastString
59 \end{code}
60
61
62         ----------------------------
63                 General notes
64         ----------------------------
65
66 Generally speaking we now type-check types in three phases
67
68   1.  kcHsType: kind check the HsType
69         *includes* performing any TH type splices;
70         so it returns a translated, and kind-annotated, type
71
72   2.  dsHsType: convert from HsType to Type:
73         perform zonking
74         expand type synonyms [mkGenTyApps]
75         hoist the foralls [tcHsType]
76
77   3.  checkValidType: check the validity of the resulting type
78
79 Often these steps are done one after the other (tcHsSigType).
80 But in mutually recursive groups of type and class decls we do
81         1 kind-check the whole group
82         2 build TyCons/Classes in a knot-tied way
83         3 check the validity of types in the now-unknotted TyCons/Classes
84
85 For example, when we find
86         (forall a m. m a -> m a)
87 we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
88 a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
89 an environment that binds a and m suitably.
90
91 The kind checker passed to tcHsTyVars needs to look at enough to
92 establish the kind of the tyvar:
93   * For a group of type and class decls, it's just the group, not
94         the rest of the program
95   * For a tyvar bound in a pattern type signature, its the types
96         mentioned in the other type signatures in that bunch of patterns
97   * For a tyvar bound in a RULE, it's the type signatures on other
98         universally quantified variables in the rule
99
100 Note that this may occasionally give surprising results.  For example:
101
102         data T a b = MkT (a b)
103
104 Here we deduce                  a::*->*,       b::*
105 But equally valid would be      a::(*->*)-> *, b::*->*
106
107
108 Validity checking
109 ~~~~~~~~~~~~~~~~~
110 Some of the validity check could in principle be done by the kind checker, 
111 but not all:
112
113 - During desugaring, we normalise by expanding type synonyms.  Only
114   after this step can we check things like type-synonym saturation
115   e.g.  type T k = k Int
116         type S a = a
117   Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
118   and then S is saturated.  This is a GHC extension.
119
120 - Similarly, also a GHC extension, we look through synonyms before complaining
121   about the form of a class or instance declaration
122
123 - Ambiguity checks involve functional dependencies, and it's easier to wait
124   until knots have been resolved before poking into them
125
126 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
127 finished building the loop.  So to keep things simple, we postpone most validity
128 checking until step (3).
129
130 Knot tying
131 ~~~~~~~~~~
132 During step (1) we might fault in a TyCon defined in another module, and it might
133 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
134 knot around type declarations with ARecThing, so that the fault-in code can get
135 the TyCon being defined.
136
137
138 %************************************************************************
139 %*                                                                      *
140 \subsection{Checking types}
141 %*                                                                      *
142 %************************************************************************
143
144 \begin{code}
145 tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
146   -- Do kind checking, and hoist for-alls to the top
147   -- NB: it's important that the foralls that come from the top-level
148   --     HsForAllTy in hs_ty occur *first* in the returned type.
149   --     See Note [Scoped] with TcSigInfo
150 tcHsSigType ctxt hs_ty 
151   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
152     tcHsSigTypeNC ctxt hs_ty
153
154 tcHsSigTypeNC ctxt hs_ty
155   = do  { (kinded_ty, _kind) <- kc_lhs_type hs_ty
156           -- The kind is checked by checkValidType, and isn't necessarily
157           -- of kind * in a Template Haskell quote eg [t| Maybe |]
158         ; ty <- tcHsKindedType kinded_ty
159         ; checkValidType ctxt ty        
160         ; return ty }
161
162 tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
163 -- Typecheck an instance head.  We can't use 
164 -- tcHsSigType, because it's not a valid user type.
165 tcHsInstHead (L loc hs_ty)
166   = setSrcSpan loc   $  -- No need for an "In the type..." context
167                         -- because that comes from the caller
168     kc_ds_inst_head hs_ty
169   where
170     kc_ds_inst_head ty = case splitHsClassTy_maybe cls_ty of
171         Just _ -> do -- Kind-checking first
172           (tvs, ctxt, cls_ty) <- kcHsTyVars tv_names $ \ tv_names' -> do
173             ctxt' <- mapM kcHsLPredType ctxt
174             cls_ty' <- kc_check_hs_type cls_ty ekConstraint
175                -- The body of a forall is usually lifted, but in an instance
176                -- head we only allow something of kind Constraint.
177             return (tv_names', ctxt', cls_ty')
178           -- Now desugar the kind-checked type
179           let Just (cls_name, tys) = splitHsClassTy_maybe cls_ty
180           tcTyVarBndrs tvs  $ \ tvs' -> do
181             ctxt' <- dsHsTypes ctxt
182             clas <- tcLookupClass cls_name
183             tys' <- dsHsTypes tys
184             return (tvs', ctxt', clas, tys')
185         _ -> failWithTc (ptext (sLit "Malformed instance type"))
186       where (tv_names, ctxt, cls_ty) = splitHsForAllTy ty
187
188 tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
189 -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
190 -- except that we want to keep the tvs separate
191 tcHsQuantifiedType tv_names hs_ty
192   = kcHsTyVars tv_names $ \ tv_names' ->
193     do  { kc_ty <- kcHsSigType hs_ty
194         ; tcTyVarBndrs tv_names' $ \ tvs ->
195     do  { ty <- dsHsType kc_ty
196         ; return (tvs, ty) } }
197
198 -- Used for the deriving(...) items
199 tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
200 tcHsDeriv = tc_hs_deriv []
201
202 tc_hs_deriv :: [LHsTyVarBndr Name] -> HsType Name
203             -> TcM ([TyVar], Class, [Type])
204 tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
205   =     -- Funny newtype deriving form
206         --      forall a. C [a]
207         -- where C has arity 2.  Hence can't use regular functions
208     tc_hs_deriv (tv_names1 ++ tv_names2) ty
209
210 tc_hs_deriv tv_names ty
211   | Just (cls_name, hs_tys) <- splitHsClassTy_maybe ty
212   = kcHsTyVars tv_names                 $ \ tv_names' ->
213     do  { cls_kind <- kcClass cls_name
214         ; (tys, _res_kind) <- kcApps cls_name cls_kind hs_tys
215         ; tcTyVarBndrs tv_names'        $ \ tyvars ->
216     do  { arg_tys <- dsHsTypes tys
217         ; cls <- tcLookupClass cls_name
218         ; return (tyvars, cls, arg_tys) }}
219
220   | otherwise
221   = failWithTc (ptext (sLit "Illegal deriving item") <+> ppr ty)
222 \end{code}
223
224         These functions are used during knot-tying in
225         type and class declarations, when we have to
226         separate kind-checking, desugaring, and validity checking
227
228 \begin{code}
229 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
230         -- Used for type signatures
231 kcHsSigType ty       = addKcTypeCtxt ty $ kcTypeType ty
232 kcHsLiftedSigType ty = addKcTypeCtxt ty $ kcLiftedType ty
233
234 tcHsKindedType :: LHsType Name -> TcM Type
235   -- Don't do kind checking, nor validity checking.
236   -- This is used in type and class decls, where kinding is
237   -- done in advance, and validity checking is done later
238   -- [Validity checking done later because of knot-tying issues.]
239 tcHsKindedType hs_ty = dsHsType hs_ty
240
241 tcHsBangType :: LHsType Name -> TcM Type
242 -- Permit a bang, but discard it
243 tcHsBangType (L _ (HsBangTy _ ty)) = tcHsKindedType ty
244 tcHsBangType ty                    = tcHsKindedType ty
245
246 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
247 -- Used when we are expecting a ClassContext (i.e. no implicit params)
248 -- Does not do validity checking, like tcHsKindedType
249 tcHsKindedContext hs_theta = addLocM (mapM dsHsType) hs_theta
250 \end{code}
251
252
253 %************************************************************************
254 %*                                                                      *
255                 The main kind checker: kcHsType
256 %*                                                                      *
257 %************************************************************************
258         
259         First a couple of simple wrappers for kcHsType
260
261 \begin{code}
262 ---------------------------
263 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
264 -- The type ty must be a *lifted* *type*
265 kcLiftedType ty = kc_check_lhs_type ty ekLifted
266     
267 ---------------------------
268 kcTypeType :: LHsType Name -> TcM (LHsType Name)
269 -- The type ty must be a *type*, but it can be lifted or 
270 -- unlifted or an unboxed tuple.
271 kcTypeType ty = kc_check_lhs_type ty ekOpen
272
273 kcArgs :: SDoc -> [LHsType Name] -> Kind -> TcM [LHsType Name]
274 kcArgs what tys kind 
275   = sequence [ kc_check_lhs_type ty (EK kind (EkArg what n)) 
276              | (ty,n) <- tys `zip` [1..] ]
277
278 ---------------------------
279 kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)
280 kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind
281
282
283 kc_check_lhs_type :: LHsType Name -> ExpKind -> TcM (LHsType Name)
284 -- Check that the type has the specified kind
285 -- Be sure to use checkExpectedKind, rather than simply unifying 
286 -- with OpenTypeKind, because it gives better error messages
287 kc_check_lhs_type (L span ty) exp_kind 
288   = setSrcSpan span $
289     do { ty' <- kc_check_hs_type ty exp_kind
290        ; return (L span ty') }
291
292 kc_check_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [LHsType Name]
293 kc_check_lhs_types tys_w_kinds
294   = mapM kc_arg tys_w_kinds
295   where
296     kc_arg (arg, arg_kind) = kc_check_lhs_type arg arg_kind
297
298
299 ---------------------------
300 kc_check_hs_type :: HsType Name -> ExpKind -> TcM (HsType Name)
301
302 -- First some special cases for better error messages 
303 -- when we know the expected kind
304 kc_check_hs_type (HsParTy ty) exp_kind
305   = do { ty' <- kc_check_lhs_type ty exp_kind; return (HsParTy ty') }
306
307 kc_check_hs_type ty@(HsAppTy ty1 ty2) exp_kind
308   = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
309        ; (fun_ty', fun_kind) <- kc_lhs_type fun_ty
310        ; arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
311        ; return (mkHsAppTys fun_ty' arg_tys') }
312
313 -- This is the general case: infer the kind and compare
314 kc_check_hs_type ty exp_kind
315   = do  { (ty', act_kind) <- kc_hs_type ty
316                 -- Add the context round the inner check only
317                 -- because checkExpectedKind already mentions
318                 -- 'ty' by name in any error message
319
320         ; checkExpectedKind (strip ty) act_kind exp_kind
321         ; return ty' }
322   where
323         -- We infer the kind of the type, and then complain if it's
324         -- not right.  But we don't want to complain about
325         --      (ty) or !(ty) or forall a. ty
326         -- when the real difficulty is with the 'ty' part.
327     strip (HsParTy (L _ ty))          = strip ty
328     strip (HsBangTy _ (L _ ty))       = strip ty
329     strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
330     strip ty                          = ty
331 \end{code}
332
333         Here comes the main function
334
335 \begin{code}
336 kcLHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
337 -- Called from outside: set the context
338 kcLHsType ty = addKcTypeCtxt ty (kc_lhs_type ty)
339
340 kc_lhs_type :: LHsType Name -> TcM (LHsType Name, TcKind)
341 kc_lhs_type (L span ty)
342   = setSrcSpan span $
343     do { (ty', kind) <- kc_hs_type ty
344        ; return (L span ty', kind) }
345
346 -- kc_hs_type *returns* the kind of the type, rather than taking an expected
347 -- kind as argument as tcExpr does.  
348 -- Reasons: 
349 --      (a) the kind of (->) is
350 --              forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
351 --          so we'd need to generate huge numbers of bx variables.
352 --      (b) kinds are so simple that the error messages are fine
353 --
354 -- The translated type has explicitly-kinded type-variable binders
355
356 kc_hs_type :: HsType Name -> TcM (HsType Name, TcKind)
357 kc_hs_type (HsParTy ty) = do
358    (ty', kind) <- kc_lhs_type ty
359    return (HsParTy ty', kind)
360
361 kc_hs_type (HsTyVar name)
362   -- Special case for the unit tycon so it benefits from kind overloading
363   | name == tyConName unitTyCon
364   = kc_hs_type (HsTupleTy (HsBoxyTuple placeHolderKind) [])
365   | otherwise = do
366     kind <- kcTyVar name
367     return (HsTyVar name, kind)
368
369 kc_hs_type (HsListTy ty) = do
370     ty' <- kcLiftedType ty
371     return (HsListTy ty', liftedTypeKind)
372
373 kc_hs_type (HsPArrTy ty) = do
374     ty' <- kcLiftedType ty
375     return (HsPArrTy ty', liftedTypeKind)
376
377 kc_hs_type (HsKindSig ty k) = do
378     ty' <- kc_check_lhs_type ty (EK k EkKindSig)
379     return (HsKindSig ty' k, k)
380
381 kc_hs_type (HsTupleTy (HsBoxyTuple _) tys)
382   = do { fact_tup_ok <- xoptM Opt_ConstraintKinds
383        ; k <- if fact_tup_ok
384               then newKindVar
385               else return liftedTypeKind
386        ; tys' <- kcArgs (ptext (sLit "a tuple")) tys k
387        ; return (HsTupleTy (HsBoxyTuple k) tys', k) }
388              -- In some contexts users really "mean" to write
389              -- tuples with Constraint components, rather than * components.
390              --
391              -- This special case of kind-checking does this rewriting 
392              -- when we can detect that we need it.
393
394 kc_hs_type (HsTupleTy HsUnboxedTuple tys)
395   = do { tys' <- kcArgs (ptext (sLit "an unboxed tuple")) tys argTypeKind
396        ; return (HsTupleTy HsUnboxedTuple tys', ubxTupleKind) }
397
398 kc_hs_type (HsFunTy ty1 ty2) = do
399     ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)
400     ty2' <- kcTypeType ty2
401     return (HsFunTy ty1' ty2', liftedTypeKind)
402
403 kc_hs_type (HsOpTy ty1 op ty2) = do
404     op_kind <- addLocM kcTyVar op
405     ([ty1',ty2'], res_kind) <- kcApps op op_kind [ty1,ty2]
406     return (HsOpTy ty1' op ty2', res_kind)
407
408 kc_hs_type (HsAppTy ty1 ty2) = do
409     let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
410     (fun_ty', fun_kind) <- kc_lhs_type fun_ty
411     (arg_tys', res_kind) <- kcApps fun_ty fun_kind arg_tys
412     return (mkHsAppTys fun_ty' arg_tys', res_kind)
413
414 kc_hs_type (HsIParamTy n ty) = do
415     ty' <- kc_check_lhs_type ty (EK liftedTypeKind EkIParam)
416     return (HsIParamTy n ty', constraintKind)
417
418 kc_hs_type (HsEqTy ty1 ty2) = do
419     (ty1', kind1) <- kc_lhs_type ty1
420     (ty2', kind2) <- kc_lhs_type ty2
421     checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
422     return (HsEqTy ty1' ty2', constraintKind)
423
424 kc_hs_type (HsCoreTy ty)
425   = return (HsCoreTy ty, typeKind ty)
426
427 kc_hs_type (HsForAllTy exp tv_names context ty)
428   = kcHsTyVars tv_names         $ \ tv_names' ->
429     do  { ctxt' <- kcHsContext context
430         ; ty'   <- kcLiftedType ty
431              -- The body of a forall is usually a type, but in principle
432              -- there's no reason to prohibit *unlifted* types.
433              -- In fact, GHC can itself construct a function with an
434              -- unboxed tuple inside a for-all (via CPR analyis; see 
435              -- typecheck/should_compile/tc170)
436              --
437              -- Still, that's only for internal interfaces, which aren't
438              -- kind-checked, so we only allow liftedTypeKind here
439
440         ; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
441
442 kc_hs_type (HsBangTy b ty)
443   = do { (ty', kind) <- kc_lhs_type ty
444        ; return (HsBangTy b ty', kind) }
445
446 kc_hs_type ty@(HsRecTy _)
447   = failWithTc (ptext (sLit "Unexpected record type") <+> ppr ty)
448       -- Record types (which only show up temporarily in constructor signatures) 
449       -- should have been removed by now
450
451 #ifdef GHCI     /* Only if bootstrapped */
452 kc_hs_type (HsSpliceTy sp fvs _) = kcSpliceType sp fvs
453 #else
454 kc_hs_type ty@(HsSpliceTy {}) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
455 #endif
456
457 kc_hs_type (HsQuasiQuoteTy {}) = panic "kc_hs_type"     -- Eliminated by renamer
458
459 -- remove the doc nodes here, no need to worry about the location since
460 -- its the same for a doc node and it's child type node
461 kc_hs_type (HsDocTy ty _)
462   = kc_hs_type (unLoc ty) 
463
464 ---------------------------
465 kcApps :: Outputable a
466        => a 
467        -> TcKind                        -- Function kind
468        -> [LHsType Name]                -- Arg types
469        -> TcM ([LHsType Name], TcKind)  -- Kind-checked args
470 kcApps the_fun fun_kind args
471   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
472        ; args' <- kc_check_lhs_types args_w_kinds
473        ; return (args', res_kind) }
474
475 kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
476             -> HsType Name     -- The type being checked (for err messages only)
477             -> ExpKind         -- Expected kind
478             -> TcM [LHsType Name]
479 kcCheckApps the_fun fun_kind args ty exp_kind
480   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
481        ; checkExpectedKind ty res_kind exp_kind
482              -- Check the result kind *before* checking argument kinds
483              -- This improves error message; Trac #2994
484        ; kc_check_lhs_types args_w_kinds }
485
486
487 ---------------------------
488 splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
489 splitFunKind _       _      fk [] = return ([], fk)
490 splitFunKind the_fun arg_no fk (arg:args)
491   = do { mb_fk <- matchExpectedFunKind fk
492        ; case mb_fk of
493             Nothing       -> failWithTc too_many_args 
494             Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
495                                 ; return ((arg, EK ak (EkArg (quotes the_fun) arg_no)):aks, rk) } }
496   where
497     too_many_args = quotes the_fun <+>
498                     ptext (sLit "is applied to too many type arguments")
499
500 ---------------------------
501 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
502 kcHsContext ctxt = wrapLocM (mapM kcHsLPredType) ctxt
503
504 kcHsLPredType :: LHsType Name -> TcM (LHsType Name)
505 kcHsLPredType pred = kc_check_lhs_type pred ekConstraint
506
507 ---------------------------
508 kcTyVar :: Name -> TcM TcKind
509 kcTyVar name = do       -- Could be a tyvar or a tycon
510     traceTc "lk1" (ppr name)
511     thing <- tcLookup name
512     traceTc "lk2" (ppr name <+> ppr thing)
513     case thing of 
514         ATyVar _ ty             -> return (typeKind ty)
515         AThing kind             -> return kind
516         AGlobal (ATyCon tc)     -> return (tyConKind tc)
517         _                       -> wrongThingErr "type" thing name
518
519 kcClass :: Name -> TcM TcKind
520 kcClass cls = do        -- Must be a class
521     thing <- tcLookup cls
522     case thing of
523         AThing kind                         -> return kind
524         AGlobal (ATyCon tc)
525           | Just cls <- tyConClass_maybe tc -> return (tyConKind (classTyCon cls))
526         _                                   -> wrongThingErr "class" thing cls
527 \end{code}
528
529
530 %************************************************************************
531 %*                                                                      *
532                 Desugaring
533 %*                                                                      *
534 %************************************************************************
535
536 The type desugarer
537
538         * Transforms from HsType to Type
539         * Zonks any kinds
540
541 It cannot fail, and does no validity checking, except for 
542 structural matters, such as
543         (a) spurious ! annotations.
544         (b) a class used as a type
545
546 \begin{code}
547 dsHsType :: LHsType Name -> TcM Type
548 -- All HsTyVarBndrs in the intput type are kind-annotated
549 dsHsType ty = ds_type (unLoc ty)
550
551 ds_type :: HsType Name -> TcM Type
552 ds_type ty@(HsTyVar _)
553   = ds_app ty []
554
555 ds_type (HsParTy ty)            -- Remove the parentheses markers
556   = dsHsType ty
557
558 ds_type ty@(HsBangTy {})    -- No bangs should be here
559   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
560
561 ds_type ty@(HsRecTy {})     -- No bangs should be here
562   = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
563
564 ds_type (HsKindSig ty _)
565   = dsHsType ty -- Kind checking done already
566
567 ds_type (HsListTy ty) = do
568     tau_ty <- dsHsType ty
569     checkWiredInTyCon listTyCon
570     return (mkListTy tau_ty)
571
572 ds_type (HsPArrTy ty) = do
573     tau_ty <- dsHsType ty
574     checkWiredInTyCon parrTyCon
575     return (mkPArrTy tau_ty)
576
577 ds_type (HsTupleTy hs_con tys) = do
578     con <- case hs_con of
579         HsUnboxedTuple -> return UnboxedTuple
580         HsBoxyTuple kind -> do
581           kind' <- zonkTcKindToKind kind
582           case () of
583             _ | kind' `eqKind` constraintKind -> return ConstraintTuple
584             _ | kind' `eqKind` liftedTypeKind -> return BoxedTuple
585             _ | otherwise
586               -> failWithTc (ptext (sLit "Unexpected tuple component kind:") <+> ppr kind')
587     let tycon = tupleTyCon con (length tys)
588     tau_tys <- dsHsTypes tys
589     checkWiredInTyCon tycon
590     return (mkTyConApp tycon tau_tys)
591
592 ds_type (HsFunTy ty1 ty2) = do
593     tau_ty1 <- dsHsType ty1
594     tau_ty2 <- dsHsType ty2
595     return (mkFunTy tau_ty1 tau_ty2)
596
597 ds_type (HsOpTy ty1 (L span op) ty2) = do
598     tau_ty1 <- dsHsType ty1
599     tau_ty2 <- dsHsType ty2
600     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
601
602 ds_type ty@(HsAppTy _ _)
603   = ds_app ty []
604
605 ds_type (HsIParamTy n ty) = do
606     tau_ty <- dsHsType ty
607     return (mkIPPred n tau_ty)
608
609 ds_type (HsEqTy ty1 ty2) = do
610     tau_ty1 <- dsHsType ty1
611     tau_ty2 <- dsHsType ty2
612     return (mkEqPred (tau_ty1, tau_ty2))
613
614 ds_type (HsForAllTy _ tv_names ctxt ty)
615   = tcTyVarBndrs tv_names               $ \ tyvars -> do
616     theta <- mapM dsHsType (unLoc ctxt)
617     tau <- dsHsType ty
618     return (mkSigmaTy tyvars theta tau)
619
620 ds_type (HsDocTy ty _)  -- Remove the doc comment
621   = dsHsType ty
622
623 ds_type (HsSpliceTy _ _ kind) 
624   = do { kind' <- zonkTcKindToKind kind
625        ; newFlexiTyVarTy kind' }
626
627 ds_type (HsQuasiQuoteTy {}) = panic "ds_type"   -- Eliminated by renamer
628 ds_type (HsCoreTy ty)       = return ty
629
630 dsHsTypes :: [LHsType Name] -> TcM [Type]
631 dsHsTypes arg_tys = mapM dsHsType arg_tys
632 \end{code}
633
634 Help functions for type applications
635 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
636
637 \begin{code}
638 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
639 ds_app (HsAppTy ty1 ty2) tys
640   = ds_app (unLoc ty1) (ty2:tys)
641
642 ds_app ty tys = do
643     arg_tys <- dsHsTypes tys
644     case ty of
645         HsTyVar fun -> ds_var_app fun arg_tys
646         _           -> do fun_ty <- ds_type ty
647                           return (mkAppTys fun_ty arg_tys)
648
649 ds_var_app :: Name -> [Type] -> TcM Type
650 ds_var_app name arg_tys = do
651     thing <- tcLookup name
652     case thing of
653         ATyVar _ ty         -> return (mkAppTys ty arg_tys)
654         AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
655         _                   -> wrongThingErr "type" thing name
656 \end{code}
657
658 \begin{code}
659 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
660         -- Wrap a context around only if we want to show that contexts.  
661         -- Omit invisble ones and ones user's won't grok
662 addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing
663
664 typeCtxt :: HsType Name -> SDoc
665 typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
666 \end{code}
667
668 %************************************************************************
669 %*                                                                      *
670                 Type-variable binders
671 %*                                                                      *
672 %************************************************************************
673
674
675 \begin{code}
676 kcHsTyVars :: [LHsTyVarBndr Name] 
677            -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
678                                                 -- They scope over the thing inside
679            -> TcM r
680 kcHsTyVars tvs thing_inside
681   = do { kinded_tvs <- mapM (wrapLocM kcHsTyVar) tvs
682        ; tcExtendKindEnvTvs kinded_tvs thing_inside }
683
684 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
685         -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it      
686 kcHsTyVar (UserTyVar name _)  = UserTyVar name <$> newKindVar
687 kcHsTyVar tv@(KindedTyVar {}) = return tv
688
689 ------------------
690 tcTyVarBndrs :: [LHsTyVarBndr Name]     -- Kind-annotated binders, which need kind-zonking
691              -> ([TyVar] -> TcM r)
692              -> TcM r
693 -- Used when type-checking types/classes/type-decls
694 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
695 tcTyVarBndrs bndrs thing_inside = do
696     tyvars <- mapM (zonk . unLoc) bndrs
697     tcExtendTyVarEnv tyvars (thing_inside tyvars)
698   where
699     zonk (UserTyVar name kind) = do { kind' <- zonkTcKindToKind kind
700                                     ; return (mkTyVar name kind') }
701     zonk (KindedTyVar name kind) = return (mkTyVar name kind)
702
703 -----------------------------------
704 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
705 -- GADT decls can have a (perhaps partial) kind signature
706 --      e.g.  data T :: * -> * -> * where ...
707 -- This function makes up suitable (kinded) type variables for 
708 -- the argument kinds, and checks that the result kind is indeed *.
709 -- We use it also to make up argument type variables for for data instances.
710 tcDataKindSig Nothing = return []
711 tcDataKindSig (Just kind)
712   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
713         ; span <- getSrcSpanM
714         ; us   <- newUniqueSupply 
715         ; let uniqs = uniqsFromSupply us
716         ; return [ mk_tv span uniq str kind 
717                  | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
718   where
719     (arg_kinds, res_kind) = splitKindFunTys kind
720     mk_tv loc uniq str kind = mkTyVar name kind
721         where
722            name = mkInternalName uniq occ loc
723            occ  = mkOccName tvName str
724           
725     dnames = map ('$' :) names  -- Note [Avoid name clashes for associated data types]
726
727     names :: [String]
728     names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 
729
730 badKindSig :: Kind -> SDoc
731 badKindSig kind 
732  = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
733         2 (ppr kind)
734 \end{code}
735
736 Note [Avoid name clashes for associated data types]
737 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
738 Consider    class C a b where
739                data D b :: * -> *
740 When typechecking the decl for D, we'll invent an extra type variable for D,
741 to fill out its kind.  We *don't* want this type variable to be 'a', because
742 in an .hi file we'd get
743             class C a b where
744                data D b a 
745 which makes it look as if there are *two* type indices.  But there aren't!
746 So we use $a instead, which cannot clash with a user-written type variable.
747 Remember that type variable binders in interface files are just FastStrings,
748 not proper Names.
749
750 (The tidying phase can't help here because we don't tidy TyCons.  Another
751 alternative would be to record the number of indexing parameters in the 
752 interface file.)
753
754
755 %************************************************************************
756 %*                                                                      *
757                 Scoped type variables
758 %*                                                                      *
759 %************************************************************************
760
761
762 tcAddScopedTyVars is used for scoped type variables added by pattern
763 type signatures
764         e.g.  \ ((x::a), (y::a)) -> x+y
765 They never have explicit kinds (because this is source-code only)
766 They are mutable (because they can get bound to a more specific type).
767
768 Usually we kind-infer and expand type splices, and then
769 tupecheck/desugar the type.  That doesn't work well for scoped type
770 variables, because they scope left-right in patterns.  (e.g. in the
771 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
772
773 The current not-very-good plan is to
774   * find all the types in the patterns
775   * find their free tyvars
776   * do kind inference
777   * bring the kinded type vars into scope
778   * BUT throw away the kind-checked type
779         (we'll kind-check it again when we type-check the pattern)
780
781 This is bad because throwing away the kind checked type throws away
782 its splices.  But too bad for now.  [July 03]
783
784 Historical note:
785     We no longer specify that these type variables must be univerally 
786     quantified (lots of email on the subject).  If you want to put that 
787     back in, you need to
788         a) Do a checkSigTyVars after thing_inside
789         b) More insidiously, don't pass in expected_ty, else
790            we unify with it too early and checkSigTyVars barfs
791            Instead you have to pass in a fresh ty var, and unify
792            it with expected_ty afterwards
793
794 \begin{code}
795 tcHsPatSigType :: UserTypeCtxt
796                -> LHsType Name          -- The type signature
797                -> TcM ([TyVar],         -- Newly in-scope type variables
798                         Type)           -- The signature
799 -- Used for type-checking type signatures in
800 -- (a) patterns           e.g  f (x::Int) = e
801 -- (b) result signatures  e.g. g x :: Int = e
802 -- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
803
804 tcHsPatSigType ctxt hs_ty 
805   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
806     do  {       -- Find the type variables that are mentioned in the type
807                 -- but not already in scope.  These are the ones that
808                 -- should be bound by the pattern signature
809           in_scope <- getInLocalScope
810         ; let span = getLoc hs_ty
811               sig_tvs = userHsTyVarBndrs $ map (L span) $ 
812                         filterOut in_scope $
813                         nameSetToList (extractHsTyVars hs_ty)
814
815         ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
816         ; checkValidType ctxt sig_ty 
817         ; return (tyvars, sig_ty)
818       }
819
820 tcPatSig :: UserTypeCtxt
821          -> LHsType Name
822          -> TcSigmaType
823          -> TcM (TcType,           -- The type to use for "inside" the signature
824                  [(Name, TcType)], -- The new bit of type environment, binding
825                                    -- the scoped type variables
826                  HsWrapper)        -- Coercion due to unification with actual ty
827                                    -- Of shape:  res_ty ~ sig_ty
828 tcPatSig ctxt sig res_ty
829   = do  { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
830         -- sig_tvs are the type variables free in 'sig', 
831         -- and not already in scope. These are the ones
832         -- that should be brought into scope
833
834         ; if null sig_tvs then do {
835                 -- The type signature binds no type variables, 
836                 -- and hence is rigid, so use it to zap the res_ty
837                   wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
838                 ; return (sig_ty, [], wrap)
839         } else do {
840                 -- Type signature binds at least one scoped type variable
841         
842                 -- A pattern binding cannot bind scoped type variables
843                 -- The renamer fails with a name-out-of-scope error 
844                 -- if a pattern binding tries to bind a type variable,
845                 -- So we just have an ASSERT here
846         ; let in_pat_bind = case ctxt of
847                                 BindPatSigCtxt -> True
848                                 _              -> False
849         ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
850
851                 -- Check that all newly-in-scope tyvars are in fact
852                 -- constrained by the pattern.  This catches tiresome
853                 -- cases like   
854                 --      type T a = Int
855                 --      f :: Int -> Int
856                 --      f (x :: T a) = ...
857                 -- Here 'a' doesn't get a binding.  Sigh
858         ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
859         ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
860
861         -- Now do a subsumption check of the pattern signature against res_ty
862         ; sig_tvs' <- tcInstSigTyVars sig_tvs
863         ; let sig_ty' = substTyWith sig_tvs sig_tv_tys' sig_ty
864               sig_tv_tys' = mkTyVarTys sig_tvs'
865         ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty'
866
867         -- Check that each is bound to a distinct type variable,
868         -- and one that is not already in scope
869         ; binds_in_scope <- getScopedTyVarBinds
870         ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys'
871         ; check binds_in_scope tv_binds
872         
873         -- Phew!
874         ; return (sig_ty', tv_binds, wrap)
875         } }
876   where
877     check _ [] = return ()
878     check in_scope ((n,ty):rest) = do { check_one in_scope n ty
879                                       ; check ((n,ty):in_scope) rest }
880
881     check_one in_scope n ty
882         = checkTc (null dups) (dupInScope n (head dups) ty)
883                 -- Must not bind to the same type variable
884                 -- as some other in-scope type variable
885         where
886           dups = [n' | (n',ty') <- in_scope, eqType ty' ty]
887 \end{code}
888
889
890 %************************************************************************
891 %*                                                                      *
892         Checking kinds
893 %*                                                                      *
894 %************************************************************************
895
896 We would like to get a decent error message from
897   (a) Under-applied type constructors
898              f :: (Maybe, Maybe)
899   (b) Over-applied type constructors
900              f :: Int x -> Int x
901
902 \begin{code}
903 -- The ExpKind datatype means "expected kind" and contains 
904 -- some info about just why that kind is expected, to improve
905 -- the error message on a mis-match
906 data ExpKind = EK TcKind EkCtxt
907 data EkCtxt  = EkUnk            -- Unknown context
908              | EkEqPred         -- Second argument of an equality predicate
909              | EkKindSig        -- Kind signature
910              | EkArg SDoc Int   -- Function, arg posn, expected kind
911              | EkIParam         -- Implicit parameter type
912              | EkFamInst        -- Family instance
913
914
915 ekLifted, ekOpen, ekConstraint :: ExpKind
916 ekLifted     = EK liftedTypeKind EkUnk
917 ekOpen       = EK openTypeKind   EkUnk
918 ekConstraint = EK constraintKind EkUnk
919
920 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
921 -- A fancy wrapper for 'unifyKind', which tries
922 -- to give decent error messages.
923 --      (checkExpectedKind ty act_kind exp_kind)
924 -- checks that the actual kind act_kind is compatible
925 --      with the expected kind exp_kind
926 -- The first argument, ty, is used only in the error message generation
927 checkExpectedKind ty act_kind (EK exp_kind ek_ctxt) = do
928     (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
929     case mb_r of
930         Just _  -> return ()  -- Unification succeeded
931         Nothing -> do
932
933         -- So there's definitely an error
934         -- Now to find out what sort
935            exp_kind <- zonkTcKind exp_kind
936            act_kind <- zonkTcKind act_kind
937
938            env0 <- tcInitTidyEnv
939            let (exp_as, _) = splitKindFunTys exp_kind
940                (act_as, _) = splitKindFunTys act_kind
941                n_exp_as = length exp_as
942                n_act_as = length act_as
943
944                (env1, tidy_exp_kind) = tidyKind env0 exp_kind
945                (env2, tidy_act_kind) = tidyKind env1 act_kind
946
947                err | n_exp_as < n_act_as     -- E.g. [Maybe]
948                    = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
949
950                      -- Now n_exp_as >= n_act_as. In the next two cases,
951                      -- n_exp_as == 0, and hence so is n_act_as
952                    | isConstraintKind tidy_act_kind
953                    = text "Predicate" <+> quotes (ppr ty) <+> text "used as a type"
954                    
955                    | isConstraintKind tidy_exp_kind
956                    = text "Type of kind " <+> ppr tidy_act_kind <+> text "used as a constraint"
957                    
958                    | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
959                    = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
960                        <+> ptext (sLit "is unlifted")
961
962                    | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
963                    = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
964                        <+> ptext (sLit "is lifted")
965
966                    | otherwise               -- E.g. Monad [Int]
967                    = ptext (sLit "Kind mis-match")
968
969                more_info = sep [ expected_herald ek_ctxt <+> ptext (sLit "kind") 
970                                     <+> quotes (pprKind tidy_exp_kind) <> comma,
971                                  ptext (sLit "but") <+> quotes (ppr ty) <+>
972                                      ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
973
974                expected_herald EkUnk     = ptext (sLit "Expected")
975                expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
976                expected_herald EkEqPred  = ptext (sLit "The left argument of the equality predicate had")
977                expected_herald EkIParam  = ptext (sLit "The type argument of the implicit parameter had")
978                expected_herald EkFamInst = ptext (sLit "The family instance required")
979                expected_herald (EkArg fun arg_no)
980                  = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
981                    <+> fun <+> ptext (sLit ("should have"))
982
983            failWithTcM (env2, err $$ more_info)
984 \end{code}
985
986 %************************************************************************
987 %*                                                                      *
988                 Scoped type variables
989 %*                                                                      *
990 %************************************************************************
991
992 \begin{code}
993 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
994 pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon, 
995                                  nest 2 (pp_sig ctxt) ]
996   where
997     pp_sig (FunSigCtxt n)  = pp_n_colon n
998     pp_sig (ConArgCtxt n)  = pp_n_colon n
999     pp_sig (ForSigCtxt n)  = pp_n_colon n
1000     pp_sig _               = ppr (unLoc hs_ty)
1001
1002     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
1003
1004 badPatSigTvs :: TcType -> [TyVar] -> SDoc
1005 badPatSigTvs sig_ty bad_tvs
1006   = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, 
1007                  quotes (pprWithCommas ppr bad_tvs), 
1008                  ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
1009                  ptext (sLit "but are actually discarded by a type synonym") ]
1010          , ptext (sLit "To fix this, expand the type synonym") 
1011          , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
1012
1013 dupInScope :: Name -> Name -> Type -> SDoc
1014 dupInScope n n' _
1015   = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
1016        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
1017                 ptext (sLit "Distinct scoped type variables must be distinct")])
1018 \end{code}
1019