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