11288dc6d8500b614208e0309cd3023131b69f1b
[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
429 -- remove the doc nodes here, no need to worry about the location since
430 -- its the same for a doc node and it's child type node
431 kc_hs_type (HsDocTy ty _)
432   = kc_hs_type (unLoc ty) 
433
434 ---------------------------
435 kcApps :: Outputable a
436        => a 
437        -> TcKind                        -- Function kind
438        -> [LHsType Name]                -- Arg types
439        -> TcM ([LHsType Name], TcKind)  -- Kind-checked args
440 kcApps the_fun fun_kind args
441   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
442        ; args' <- kc_check_lhs_types args_w_kinds
443        ; return (args', res_kind) }
444
445 kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
446             -> HsType Name     -- The type being checked (for err messages only)
447             -> ExpKind         -- Expected kind
448             -> TcM [LHsType Name]
449 kcCheckApps the_fun fun_kind args ty exp_kind
450   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
451        ; checkExpectedKind ty res_kind exp_kind
452              -- Check the result kind *before* checking argument kinds
453              -- This improves error message; Trac #2994
454        ; kc_check_lhs_types args_w_kinds }
455
456 splitHsAppTys :: LHsType Name -> LHsType Name -> (LHsType Name, [LHsType Name])
457 splitHsAppTys fun_ty arg_ty = split fun_ty [arg_ty]
458   where
459     split (L _ (HsAppTy f a)) as = split f (a:as)
460     split f                   as = (f,as)
461
462 mkHsAppTys :: LHsType Name -> [LHsType Name] -> HsType Name
463 mkHsAppTys fun_ty [] = pprPanic "mkHsAppTys" (ppr fun_ty)
464 mkHsAppTys fun_ty (arg_ty:arg_tys)
465   = foldl mk_app (HsAppTy fun_ty arg_ty) arg_tys
466   where
467     mk_app fun arg = HsAppTy (noLoc fun) arg    -- Add noLocs for inner nodes of
468                                                 -- the application; they are
469                                                 -- never used 
470
471 ---------------------------
472 splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
473 splitFunKind _       _      fk [] = return ([], fk)
474 splitFunKind the_fun arg_no fk (arg:args)
475   = do { mb_fk <- unifyFunKind fk
476        ; case mb_fk of
477             Nothing       -> failWithTc too_many_args 
478             Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
479                                 ; return ((arg, EK ak (EkArg the_fun arg_no)):aks, rk) } }
480   where
481     too_many_args = quotes the_fun <+>
482                     ptext (sLit "is applied to too many type arguments")
483
484 ---------------------------
485 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
486 kcHsContext ctxt = wrapLocM (mapM kcHsLPred) ctxt
487
488 kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
489 kcHsLPred = wrapLocM kcHsPred
490
491 kcHsPred :: HsPred Name -> TcM (HsPred Name)
492 kcHsPred pred = do      -- Checks that the result is of kind liftedType
493     (pred', kind) <- kc_pred pred
494     checkExpectedKind pred kind ekLifted
495     return pred'
496     
497 ---------------------------
498 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)     
499         -- Does *not* check for a saturated
500         -- application (reason: used from TcDeriv)
501 kc_pred (HsIParam name ty)
502   = do { (ty', kind) <- kc_lhs_type ty
503        ; return (HsIParam name ty', kind)
504        }
505 kc_pred (HsClassP cls tys)
506   = do { kind <- kcClass cls
507        ; (tys', res_kind) <- kcApps cls kind tys
508        ; return (HsClassP cls tys', res_kind)
509        }
510 kc_pred (HsEqualP ty1 ty2)
511   = do { (ty1', kind1) <- kc_lhs_type ty1
512 --       ; checkExpectedKind ty1 kind1 liftedTypeKind
513        ; (ty2', kind2) <- kc_lhs_type ty2
514 --       ; checkExpectedKind ty2 kind2 liftedTypeKind
515        ; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
516        ; return (HsEqualP ty1' ty2', liftedTypeKind)
517        }
518
519 ---------------------------
520 kcTyVar :: Name -> TcM TcKind
521 kcTyVar name = do       -- Could be a tyvar or a tycon
522     traceTc (text "lk1" <+> ppr name)
523     thing <- tcLookup name
524     traceTc (text "lk2" <+> ppr name <+> ppr thing)
525     case thing of 
526         ATyVar _ ty             -> return (typeKind ty)
527         AThing kind             -> return kind
528         AGlobal (ATyCon tc)     -> return (tyConKind tc)
529         _                       -> wrongThingErr "type" thing name
530
531 kcClass :: Name -> TcM TcKind
532 kcClass cls = do        -- Must be a class
533     thing <- tcLookup cls
534     case thing of
535         AThing kind             -> return kind
536         AGlobal (AClass cls)    -> return (tyConKind (classTyCon cls))
537         _                       -> wrongThingErr "class" thing cls
538 \end{code}
539
540
541 %************************************************************************
542 %*                                                                      *
543                 Desugaring
544 %*                                                                      *
545 %************************************************************************
546
547 The type desugarer
548
549         * Transforms from HsType to Type
550         * Zonks any kinds
551
552 It cannot fail, and does no validity checking, except for 
553 structural matters, such as
554         (a) spurious ! annotations.
555         (b) a class used as a type
556
557 \begin{code}
558 dsHsType :: LHsType Name -> TcM Type
559 -- All HsTyVarBndrs in the intput type are kind-annotated
560 dsHsType ty = ds_type (unLoc ty)
561
562 ds_type :: HsType Name -> TcM Type
563 ds_type ty@(HsTyVar _)
564   = ds_app ty []
565
566 ds_type (HsParTy ty)            -- Remove the parentheses markers
567   = dsHsType ty
568
569 ds_type ty@(HsBangTy {})    -- No bangs should be here
570   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
571
572 ds_type ty@(HsRecTy {})     -- No bangs should be here
573   = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
574
575 ds_type (HsKindSig ty _)
576   = dsHsType ty -- Kind checking done already
577
578 ds_type (HsListTy ty) = do
579     tau_ty <- dsHsType ty
580     checkWiredInTyCon listTyCon
581     return (mkListTy tau_ty)
582
583 ds_type (HsPArrTy ty) = do
584     tau_ty <- dsHsType ty
585     checkWiredInTyCon parrTyCon
586     return (mkPArrTy tau_ty)
587
588 ds_type (HsTupleTy boxity tys) = do
589     tau_tys <- dsHsTypes tys
590     checkWiredInTyCon tycon
591     return (mkTyConApp tycon tau_tys)
592   where
593     tycon = tupleTyCon boxity (length tys)
594
595 ds_type (HsFunTy ty1 ty2) = do
596     tau_ty1 <- dsHsType ty1
597     tau_ty2 <- dsHsType ty2
598     return (mkFunTy tau_ty1 tau_ty2)
599
600 ds_type (HsOpTy ty1 (L span op) ty2) = do
601     tau_ty1 <- dsHsType ty1
602     tau_ty2 <- dsHsType ty2
603     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
604
605 ds_type (HsNumTy n)
606   = ASSERT(n==1) do
607     tc <- tcLookupTyCon genUnitTyConName
608     return (mkTyConApp tc [])
609
610 ds_type ty@(HsAppTy _ _)
611   = ds_app ty []
612
613 ds_type (HsPredTy pred) = do
614     pred' <- dsHsPred pred
615     return (mkPredTy pred')
616
617 ds_type (HsForAllTy _ tv_names ctxt ty)
618   = tcTyVarBndrs tv_names               $ \ tyvars -> do
619     theta <- mapM dsHsLPred (unLoc ctxt)
620     tau <- dsHsType ty
621     return (mkSigmaTy tyvars theta tau)
622
623 ds_type (HsDocTy ty _)  -- Remove the doc comment
624   = dsHsType ty
625
626 ds_type (HsSpliceTyOut kind) 
627   = do { kind' <- zonkTcKindToKind kind
628        ; newFlexiTyVarTy kind' }
629
630 ds_type (HsSpliceTy {}) = panic "ds_type"
631
632 dsHsTypes :: [LHsType Name] -> TcM [Type]
633 dsHsTypes arg_tys = mapM dsHsType arg_tys
634 \end{code}
635
636 Help functions for type applications
637 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
638
639 \begin{code}
640 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
641 ds_app (HsAppTy ty1 ty2) tys
642   = ds_app (unLoc ty1) (ty2:tys)
643
644 ds_app ty tys = do
645     arg_tys <- dsHsTypes tys
646     case ty of
647         HsTyVar fun -> ds_var_app fun arg_tys
648         _           -> do fun_ty <- ds_type ty
649                           return (mkAppTys fun_ty arg_tys)
650
651 ds_var_app :: Name -> [Type] -> TcM Type
652 ds_var_app name arg_tys = do
653     thing <- tcLookup name
654     case thing of
655         ATyVar _ ty         -> return (mkAppTys ty arg_tys)
656         AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
657         _                   -> wrongThingErr "type" thing name
658 \end{code}
659
660
661 Contexts
662 ~~~~~~~~
663
664 \begin{code}
665 dsHsLPred :: LHsPred Name -> TcM PredType
666 dsHsLPred pred = dsHsPred (unLoc pred)
667
668 dsHsPred :: HsPred Name -> TcM PredType
669 dsHsPred (HsClassP class_name tys)
670   = do { arg_tys <- dsHsTypes tys
671        ; clas <- tcLookupClass class_name
672        ; return (ClassP clas arg_tys)
673        }
674 dsHsPred (HsEqualP ty1 ty2)
675   = do { arg_ty1 <- dsHsType ty1
676        ; arg_ty2 <- dsHsType ty2
677        ; return (EqPred arg_ty1 arg_ty2)
678        }
679 dsHsPred (HsIParam name ty)
680   = do { arg_ty <- dsHsType ty
681        ; return (IParam name arg_ty)
682        }
683 \end{code}
684
685 GADT constructor signatures
686
687 \begin{code}
688 tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
689 tcLHsConResTy (L span res_ty)
690   = setSrcSpan span $
691     case get_args res_ty [] of
692            (HsTyVar tc_name, args) 
693               -> do { args' <- mapM dsHsType args
694                     ; thing <- tcLookup tc_name
695                     ; case thing of
696                         AGlobal (ATyCon tc) -> return (tc, args')
697                         _ -> failWithTc (badGadtDecl res_ty) }
698            _ -> failWithTc (badGadtDecl res_ty)
699   where
700         -- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
701         -- because that causes a black hole, and for good reason.  Building
702         -- the type means expanding type synonyms, and we can't do that
703         -- inside the "knot".  So we have to work by steam.
704     get_args (HsAppTy (L _ fun) arg)   args = get_args fun (arg:args)
705     get_args (HsParTy (L _ ty))        args = get_args ty  args
706     get_args (HsOpTy ty1 (L _ tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
707     get_args ty                        args = (ty, args)
708
709 badGadtDecl :: HsType Name -> SDoc
710 badGadtDecl ty
711   = hang (ptext (sLit "Malformed constructor result type:"))
712        2 (ppr ty)
713
714 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
715         -- Wrap a context around only if we want to show that contexts.  
716 addKcTypeCtxt (L _ (HsPredTy _)) thing = thing
717         -- Omit invisble ones and ones user's won't grok (HsPred p).
718 addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing
719
720 typeCtxt :: HsType Name -> SDoc
721 typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
722 \end{code}
723
724 %************************************************************************
725 %*                                                                      *
726                 Type-variable binders
727 %*                                                                      *
728 %************************************************************************
729
730
731 \begin{code}
732 kcHsTyVars :: [LHsTyVarBndr Name] 
733            -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
734                                                 -- They scope over the thing inside
735            -> TcM r
736 kcHsTyVars tvs thing_inside  = do
737     bndrs <- mapM (wrapLocM kcHsTyVar) tvs
738     tcExtendKindEnvTvs bndrs (thing_inside bndrs)
739
740 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
741         -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it      
742 kcHsTyVar (UserTyVar name)        = KindedTyVar name <$> newKindVar
743 kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind)
744
745 ------------------
746 tcTyVarBndrs :: [LHsTyVarBndr Name]     -- Kind-annotated binders, which need kind-zonking
747              -> ([TyVar] -> TcM r)
748              -> TcM r
749 -- Used when type-checking types/classes/type-decls
750 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
751 tcTyVarBndrs bndrs thing_inside = do
752     tyvars <- mapM (zonk . unLoc) bndrs
753     tcExtendTyVarEnv tyvars (thing_inside tyvars)
754   where
755     zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
756                                       ; return (mkTyVar name kind') }
757     zonk (UserTyVar name) = WARN( True, ptext (sLit "Un-kinded tyvar") <+> ppr name )
758                             return (mkTyVar name liftedTypeKind)
759
760 -----------------------------------
761 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
762 -- GADT decls can have a (perhaps partial) kind signature
763 --      e.g.  data T :: * -> * -> * where ...
764 -- This function makes up suitable (kinded) type variables for 
765 -- the argument kinds, and checks that the result kind is indeed *.
766 -- We use it also to make up argument type variables for for data instances.
767 tcDataKindSig Nothing = return []
768 tcDataKindSig (Just kind)
769   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
770         ; span <- getSrcSpanM
771         ; us   <- newUniqueSupply 
772         ; let uniqs = uniqsFromSupply us
773         ; return [ mk_tv span uniq str kind 
774                  | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
775   where
776     (arg_kinds, res_kind) = splitKindFunTys kind
777     mk_tv loc uniq str kind = mkTyVar name kind
778         where
779            name = mkInternalName uniq occ loc
780            occ  = mkOccName tvName str
781           
782     dnames = map ('$' :) names  -- Note [Avoid name clashes for associated data types]
783
784     names :: [String]
785     names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 
786
787 badKindSig :: Kind -> SDoc
788 badKindSig kind 
789  = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
790         2 (ppr kind)
791 \end{code}
792
793 Note [Avoid name clashes for associated data types]
794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
795 Consider    class C a b where
796                data D b :: * -> *
797 When typechecking the decl for D, we'll invent an extra type variable for D,
798 to fill out its kind.  We *don't* want this type variable to be 'a', because
799 in an .hi file we'd get
800             class C a b where
801                data D b a 
802 which makes it look as if there are *two* type indices.  But there aren't!
803 So we use $a instead, which cannot clash with a user-written type variable.
804 Remember that type variable binders in interface files are just FastStrings,
805 not proper Names.
806
807 (The tidying phase can't help here because we don't tidy TyCons.  Another
808 alternative would be to record the number of indexing parameters in the 
809 interface file.)
810
811
812 %************************************************************************
813 %*                                                                      *
814                 Scoped type variables
815 %*                                                                      *
816 %************************************************************************
817
818
819 tcAddScopedTyVars is used for scoped type variables added by pattern
820 type signatures
821         e.g.  \ ((x::a), (y::a)) -> x+y
822 They never have explicit kinds (because this is source-code only)
823 They are mutable (because they can get bound to a more specific type).
824
825 Usually we kind-infer and expand type splices, and then
826 tupecheck/desugar the type.  That doesn't work well for scoped type
827 variables, because they scope left-right in patterns.  (e.g. in the
828 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
829
830 The current not-very-good plan is to
831   * find all the types in the patterns
832   * find their free tyvars
833   * do kind inference
834   * bring the kinded type vars into scope
835   * BUT throw away the kind-checked type
836         (we'll kind-check it again when we type-check the pattern)
837
838 This is bad because throwing away the kind checked type throws away
839 its splices.  But too bad for now.  [July 03]
840
841 Historical note:
842     We no longer specify that these type variables must be univerally 
843     quantified (lots of email on the subject).  If you want to put that 
844     back in, you need to
845         a) Do a checkSigTyVars after thing_inside
846         b) More insidiously, don't pass in expected_ty, else
847            we unify with it too early and checkSigTyVars barfs
848            Instead you have to pass in a fresh ty var, and unify
849            it with expected_ty afterwards
850
851 \begin{code}
852 tcHsPatSigType :: UserTypeCtxt
853                -> LHsType Name          -- The type signature
854                -> TcM ([TyVar],         -- Newly in-scope type variables
855                         Type)           -- The signature
856 -- Used for type-checking type signatures in
857 -- (a) patterns           e.g  f (x::Int) = e
858 -- (b) result signatures  e.g. g x :: Int = e
859 -- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
860
861 tcHsPatSigType ctxt hs_ty 
862   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
863     do  {       -- Find the type variables that are mentioned in the type
864                 -- but not already in scope.  These are the ones that
865                 -- should be bound by the pattern signature
866           in_scope <- getInLocalScope
867         ; let span = getLoc hs_ty
868               sig_tvs = [ L span (UserTyVar n) 
869                         | n <- nameSetToList (extractHsTyVars hs_ty),
870                           not (in_scope n) ]
871
872         ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
873         ; checkValidType ctxt sig_ty 
874         ; return (tyvars, sig_ty)
875       }
876
877 tcPatSig :: UserTypeCtxt
878          -> LHsType Name
879          -> BoxySigmaType
880          -> TcM (TcType,           -- The type to use for "inside" the signature
881                  [(Name, TcType)], -- The new bit of type environment, binding
882                                    -- the scoped type variables
883                  CoercionI)        -- Coercion due to unification with actual ty
884 tcPatSig ctxt sig res_ty
885   = do  { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
886
887         ; if null sig_tvs then do {
888                 -- The type signature binds no type variables, 
889                 -- and hence is rigid, so use it to zap the res_ty
890                   coi <- boxyUnify sig_ty res_ty
891                 ; return (sig_ty, [], coi)
892
893         } else do {
894                 -- Type signature binds at least one scoped type variable
895         
896                 -- A pattern binding cannot bind scoped type variables
897                 -- The renamer fails with a name-out-of-scope error 
898                 -- if a pattern binding tries to bind a type variable,
899                 -- So we just have an ASSERT here
900         ; let in_pat_bind = case ctxt of
901                                 BindPatSigCtxt -> True
902                                 _              -> False
903         ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
904
905                 -- Check that pat_ty is rigid
906         ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
907
908                 -- Check that all newly-in-scope tyvars are in fact
909                 -- constrained by the pattern.  This catches tiresome
910                 -- cases like   
911                 --      type T a = Int
912                 --      f :: Int -> Int
913                 --      f (x :: T a) = ...
914                 -- Here 'a' doesn't get a binding.  Sigh
915         ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
916         ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
917
918                 -- Now match the pattern signature against res_ty
919                 -- For convenience, and uniform-looking error messages
920                 -- we do the matching by allocating meta type variables, 
921                 -- unifying, and reading out the results.
922                 -- This is a strictly local operation.
923         ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
924         ; coi <- boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) 
925                            res_ty
926         ; sig_tv_tys <- mapM readFilledBox box_tvs
927
928                 -- Check that each is bound to a distinct type variable,
929                 -- and one that is not already in scope
930         ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
931         ; binds_in_scope <- getScopedTyVarBinds
932         ; check binds_in_scope tv_binds
933         
934                 -- Phew!
935         ; return (res_ty, tv_binds, coi)
936         } }
937   where
938     check _ [] = return ()
939     check in_scope ((n,ty):rest) = do { check_one in_scope n ty
940                                       ; check ((n,ty):in_scope) rest }
941
942     check_one in_scope n ty
943         = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
944                 -- Must bind to a type variable
945
946              ; checkTc (null dups) (dupInScope n (head dups) ty)
947                 -- Must not bind to the same type variable
948                 -- as some other in-scope type variable
949
950              ; return () }
951         where
952           dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
953 \end{code}
954
955
956 %************************************************************************
957 %*                                                                      *
958         Checking kinds
959 %*                                                                      *
960 %************************************************************************
961
962 We would like to get a decent error message from
963   (a) Under-applied type constructors
964              f :: (Maybe, Maybe)
965   (b) Over-applied type constructors
966              f :: Int x -> Int x
967
968 \begin{code}
969 -- The ExpKind datatype means "expected kind" and contains 
970 -- some info about just why that kind is expected, to improve
971 -- the error message on a mis-match
972 data ExpKind = EK TcKind EkCtxt
973 data EkCtxt  = EkUnk            -- Unknown context
974              | EkEqPred         -- Second argument of an equality predicate
975              | EkKindSig        -- Kind signature
976              | EkArg SDoc Int   -- Function, arg posn, expected kind
977
978
979 ekLifted, ekOpen :: ExpKind
980 ekLifted = EK liftedTypeKind EkUnk
981 ekOpen   = EK openTypeKind   EkUnk
982
983 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
984 -- A fancy wrapper for 'unifyKind', which tries
985 -- to give decent error messages.
986 --      (checkExpectedKind ty act_kind exp_kind)
987 -- checks that the actual kind act_kind is compatible
988 --      with the expected kind exp_kind
989 -- The first argument, ty, is used only in the error message generation
990 checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
991   | act_kind `isSubKind` exp_kind -- Short cut for a very common case
992   = return ()
993   | otherwise = do
994     (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
995     case mb_r of
996         Just _  -> return ()  -- Unification succeeded
997         Nothing -> do
998
999         -- So there's definitely an error
1000         -- Now to find out what sort
1001            exp_kind <- zonkTcKind exp_kind
1002            act_kind <- zonkTcKind act_kind
1003
1004            env0 <- tcInitTidyEnv
1005            let (exp_as, _) = splitKindFunTys exp_kind
1006                (act_as, _) = splitKindFunTys act_kind
1007                n_exp_as = length exp_as
1008                n_act_as = length act_as
1009
1010                (env1, tidy_exp_kind) = tidyKind env0 exp_kind
1011                (env2, tidy_act_kind) = tidyKind env1 act_kind
1012
1013                err | n_exp_as < n_act_as     -- E.g. [Maybe]
1014                    = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
1015
1016                      -- Now n_exp_as >= n_act_as. In the next two cases,
1017                      -- n_exp_as == 0, and hence so is n_act_as
1018                    | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1019                    = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
1020                        <+> ptext (sLit "is unlifted")
1021
1022                    | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1023                    = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
1024                        <+> ptext (sLit "is lifted")
1025
1026                    | otherwise               -- E.g. Monad [Int]
1027                    = ptext (sLit "Kind mis-match")
1028
1029                more_info = sep [ expected_herald ek_ctxt <+> ptext (sLit "kind") 
1030                                     <+> quotes (pprKind tidy_exp_kind) <> comma,
1031                                  ptext (sLit "but") <+> quotes (ppr ty) <+>
1032                                      ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
1033
1034                expected_herald EkUnk     = ptext (sLit "Expected")
1035                expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
1036                expected_herald EkEqPred  = ptext (sLit "The left argument of the equality predicate had")
1037                expected_herald (EkArg fun arg_no)
1038                  = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
1039                    <+> quotes fun <+> ptext (sLit ("should have"))
1040
1041            failWithTcM (env2, err $$ more_info)
1042 \end{code}
1043
1044 %************************************************************************
1045 %*                                                                      *
1046                 Scoped type variables
1047 %*                                                                      *
1048 %************************************************************************
1049
1050 \begin{code}
1051 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
1052 pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon, 
1053                                  nest 2 (pp_sig ctxt) ]
1054   where
1055     pp_sig (FunSigCtxt n)  = pp_n_colon n
1056     pp_sig (ConArgCtxt n)  = pp_n_colon n
1057     pp_sig (ForSigCtxt n)  = pp_n_colon n
1058     pp_sig _               = ppr (unLoc hs_ty)
1059
1060     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
1061
1062 wobblyPatSig :: [Var] -> SDoc
1063 wobblyPatSig sig_tvs
1064   = hang (ptext (sLit "A pattern type signature cannot bind scoped type variables") 
1065                 <+> pprQuotedList sig_tvs)
1066        2 (ptext (sLit "unless the pattern has a rigid type context"))
1067                 
1068 badPatSigTvs :: TcType -> [TyVar] -> SDoc
1069 badPatSigTvs sig_ty bad_tvs
1070   = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, 
1071                  quotes (pprWithCommas ppr bad_tvs), 
1072                  ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
1073                  ptext (sLit "but are actually discarded by a type synonym") ]
1074          , ptext (sLit "To fix this, expand the type synonym") 
1075          , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
1076
1077 scopedNonVar :: Name -> Type -> SDoc
1078 scopedNonVar n ty
1079   = vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr n),
1080                nest 2 (ptext (sLit "is bound to the type") <+> quotes (ppr ty))],
1081           nest 2 (ptext (sLit "You can only bind scoped type variables to type variables"))]
1082
1083 dupInScope :: Name -> Name -> Type -> SDoc
1084 dupInScope n n' _
1085   = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
1086        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
1087                 ptext (sLit "Distinct scoped type variables must be distinct")])
1088
1089 wrongPredErr :: HsPred Name -> TcM (HsType Name, TcKind)
1090 wrongPredErr pred = failWithTc (text "Predicate used as a type:" <+> ppr pred)
1091 \end{code}
1092