VECTORISE pragmas for type classes and instances
[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, tcHsVectInst, 
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
223 -- Used for 'VECTORISE [SCALAR] instance' declarations
224 --
225 tcHsVectInst :: LHsType Name -> TcM (Class, [Type])
226 tcHsVectInst ty
227   | Just (L _ cls_name, tys) <- splitLHsClassTy_maybe ty
228   = do { cls_kind <- kcClass cls_name
229        ; (tys, _res_kind) <- kcApps cls_name cls_kind tys
230        ; arg_tys <- dsHsTypes tys
231        ; cls <- tcLookupClass cls_name
232        ; return (cls, arg_tys)
233        }
234   | otherwise
235   = failWithTc $ ptext (sLit "Malformed instance type")
236 \end{code}
237
238         These functions are used during knot-tying in
239         type and class declarations, when we have to
240         separate kind-checking, desugaring, and validity checking
241
242 \begin{code}
243 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
244         -- Used for type signatures
245 kcHsSigType ty       = addKcTypeCtxt ty $ kcTypeType ty
246 kcHsLiftedSigType ty = addKcTypeCtxt ty $ kcLiftedType ty
247
248 tcHsKindedType :: LHsType Name -> TcM Type
249   -- Don't do kind checking, nor validity checking.
250   -- This is used in type and class decls, where kinding is
251   -- done in advance, and validity checking is done later
252   -- [Validity checking done later because of knot-tying issues.]
253 tcHsKindedType hs_ty = dsHsType hs_ty
254
255 tcHsBangType :: LHsType Name -> TcM Type
256 -- Permit a bang, but discard it
257 tcHsBangType (L _ (HsBangTy _ ty)) = tcHsKindedType ty
258 tcHsBangType ty                    = tcHsKindedType ty
259
260 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
261 -- Used when we are expecting a ClassContext (i.e. no implicit params)
262 -- Does not do validity checking, like tcHsKindedType
263 tcHsKindedContext hs_theta = addLocM (mapM dsHsType) hs_theta
264 \end{code}
265
266
267 %************************************************************************
268 %*                                                                      *
269                 The main kind checker: kcHsType
270 %*                                                                      *
271 %************************************************************************
272         
273         First a couple of simple wrappers for kcHsType
274
275 \begin{code}
276 ---------------------------
277 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
278 -- The type ty must be a *lifted* *type*
279 kcLiftedType ty = kc_check_lhs_type ty ekLifted
280     
281 ---------------------------
282 kcTypeType :: LHsType Name -> TcM (LHsType Name)
283 -- The type ty must be a *type*, but it can be lifted or 
284 -- unlifted or an unboxed tuple.
285 kcTypeType ty = kc_check_lhs_type ty ekOpen
286
287 kcArgs :: SDoc -> [LHsType Name] -> Kind -> TcM [LHsType Name]
288 kcArgs what tys kind 
289   = sequence [ kc_check_lhs_type ty (EK kind (EkArg what n)) 
290              | (ty,n) <- tys `zip` [1..] ]
291
292 ---------------------------
293 kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)
294 kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind
295
296
297 kc_check_lhs_type :: LHsType Name -> ExpKind -> TcM (LHsType Name)
298 -- Check that the type has the specified kind
299 -- Be sure to use checkExpectedKind, rather than simply unifying 
300 -- with OpenTypeKind, because it gives better error messages
301 kc_check_lhs_type (L span ty) exp_kind 
302   = setSrcSpan span $
303     do { ty' <- kc_check_hs_type ty exp_kind
304        ; return (L span ty') }
305
306 kc_check_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [LHsType Name]
307 kc_check_lhs_types tys_w_kinds
308   = mapM kc_arg tys_w_kinds
309   where
310     kc_arg (arg, arg_kind) = kc_check_lhs_type arg arg_kind
311
312
313 ---------------------------
314 kc_check_hs_type :: HsType Name -> ExpKind -> TcM (HsType Name)
315
316 -- First some special cases for better error messages 
317 -- when we know the expected kind
318 kc_check_hs_type (HsParTy ty) exp_kind
319   = do { ty' <- kc_check_lhs_type ty exp_kind; return (HsParTy ty') }
320
321 kc_check_hs_type ty@(HsAppTy ty1 ty2) exp_kind
322   = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
323        ; (fun_ty', fun_kind) <- kc_lhs_type fun_ty
324        ; arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
325        ; return (mkHsAppTys fun_ty' arg_tys') }
326
327 -- This is the general case: infer the kind and compare
328 kc_check_hs_type ty exp_kind
329   = do  { (ty', act_kind) <- kc_hs_type ty
330                 -- Add the context round the inner check only
331                 -- because checkExpectedKind already mentions
332                 -- 'ty' by name in any error message
333
334         ; checkExpectedKind (strip ty) act_kind exp_kind
335         ; return ty' }
336   where
337         -- We infer the kind of the type, and then complain if it's
338         -- not right.  But we don't want to complain about
339         --      (ty) or !(ty) or forall a. ty
340         -- when the real difficulty is with the 'ty' part.
341     strip (HsParTy (L _ ty))          = strip ty
342     strip (HsBangTy _ (L _ ty))       = strip ty
343     strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
344     strip ty                          = ty
345 \end{code}
346
347         Here comes the main function
348
349 \begin{code}
350 kcLHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
351 -- Called from outside: set the context
352 kcLHsType ty = addKcTypeCtxt ty (kc_lhs_type ty)
353
354 kc_lhs_type :: LHsType Name -> TcM (LHsType Name, TcKind)
355 kc_lhs_type (L span ty)
356   = setSrcSpan span $
357     do { (ty', kind) <- kc_hs_type ty
358        ; return (L span ty', kind) }
359
360 -- kc_hs_type *returns* the kind of the type, rather than taking an expected
361 -- kind as argument as tcExpr does.  
362 -- Reasons: 
363 --      (a) the kind of (->) is
364 --              forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
365 --          so we'd need to generate huge numbers of bx variables.
366 --      (b) kinds are so simple that the error messages are fine
367 --
368 -- The translated type has explicitly-kinded type-variable binders
369
370 kc_hs_type :: HsType Name -> TcM (HsType Name, TcKind)
371 kc_hs_type (HsParTy ty) = do
372    (ty', kind) <- kc_lhs_type ty
373    return (HsParTy ty', kind)
374
375 kc_hs_type (HsTyVar name)
376   -- Special case for the unit tycon so it benefits from kind overloading
377   | name == tyConName unitTyCon
378   = kc_hs_type (HsTupleTy (HsBoxyTuple placeHolderKind) [])
379   | otherwise = do
380     kind <- kcTyVar name
381     return (HsTyVar name, kind)
382
383 kc_hs_type (HsListTy ty) = do
384     ty' <- kcLiftedType ty
385     return (HsListTy ty', liftedTypeKind)
386
387 kc_hs_type (HsPArrTy ty) = do
388     ty' <- kcLiftedType ty
389     return (HsPArrTy ty', liftedTypeKind)
390
391 kc_hs_type (HsKindSig ty k) = do
392     ty' <- kc_check_lhs_type ty (EK k EkKindSig)
393     return (HsKindSig ty' k, k)
394
395 kc_hs_type (HsTupleTy (HsBoxyTuple _) tys)
396   = do { fact_tup_ok <- xoptM Opt_ConstraintKinds
397        ; k <- if fact_tup_ok
398               then newKindVar
399               else return liftedTypeKind
400        ; tys' <- kcArgs (ptext (sLit "a tuple")) tys k
401        ; return (HsTupleTy (HsBoxyTuple k) tys', k) }
402              -- In some contexts users really "mean" to write
403              -- tuples with Constraint components, rather than * components.
404              --
405              -- This special case of kind-checking does this rewriting 
406              -- when we can detect that we need it.
407
408 kc_hs_type (HsTupleTy HsUnboxedTuple tys)
409   = do { tys' <- kcArgs (ptext (sLit "an unboxed tuple")) tys argTypeKind
410        ; return (HsTupleTy HsUnboxedTuple tys', ubxTupleKind) }
411
412 kc_hs_type (HsFunTy ty1 ty2) = do
413     ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)
414     ty2' <- kcTypeType ty2
415     return (HsFunTy ty1' ty2', liftedTypeKind)
416
417 kc_hs_type (HsOpTy ty1 op ty2) = do
418     op_kind <- addLocM kcTyVar op
419     ([ty1',ty2'], res_kind) <- kcApps op op_kind [ty1,ty2]
420     return (HsOpTy ty1' op ty2', res_kind)
421
422 kc_hs_type (HsAppTy ty1 ty2) = do
423     let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
424     (fun_ty', fun_kind) <- kc_lhs_type fun_ty
425     (arg_tys', res_kind) <- kcApps fun_ty fun_kind arg_tys
426     return (mkHsAppTys fun_ty' arg_tys', res_kind)
427
428 kc_hs_type (HsIParamTy n ty) = do
429     ty' <- kc_check_lhs_type ty (EK liftedTypeKind EkIParam)
430     return (HsIParamTy n ty', constraintKind)
431
432 kc_hs_type (HsEqTy ty1 ty2) = do
433     (ty1', kind1) <- kc_lhs_type ty1
434     (ty2', kind2) <- kc_lhs_type ty2
435     checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
436     return (HsEqTy ty1' ty2', constraintKind)
437
438 kc_hs_type (HsCoreTy ty)
439   = return (HsCoreTy ty, typeKind ty)
440
441 kc_hs_type (HsForAllTy exp tv_names context ty)
442   = kcHsTyVars tv_names         $ \ tv_names' ->
443     do  { ctxt' <- kcHsContext context
444         ; ty'   <- kcLiftedType ty
445              -- The body of a forall is usually a type, but in principle
446              -- there's no reason to prohibit *unlifted* types.
447              -- In fact, GHC can itself construct a function with an
448              -- unboxed tuple inside a for-all (via CPR analyis; see 
449              -- typecheck/should_compile/tc170)
450              --
451              -- Still, that's only for internal interfaces, which aren't
452              -- kind-checked, so we only allow liftedTypeKind here
453
454         ; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
455
456 kc_hs_type (HsBangTy b ty)
457   = do { (ty', kind) <- kc_lhs_type ty
458        ; return (HsBangTy b ty', kind) }
459
460 kc_hs_type ty@(HsRecTy _)
461   = failWithTc (ptext (sLit "Unexpected record type") <+> ppr ty)
462       -- Record types (which only show up temporarily in constructor signatures) 
463       -- should have been removed by now
464
465 #ifdef GHCI     /* Only if bootstrapped */
466 kc_hs_type (HsSpliceTy sp fvs _) = kcSpliceType sp fvs
467 #else
468 kc_hs_type ty@(HsSpliceTy {}) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
469 #endif
470
471 kc_hs_type (HsQuasiQuoteTy {}) = panic "kc_hs_type"     -- Eliminated by renamer
472
473 -- remove the doc nodes here, no need to worry about the location since
474 -- its the same for a doc node and it's child type node
475 kc_hs_type (HsDocTy ty _)
476   = kc_hs_type (unLoc ty) 
477
478 ---------------------------
479 kcApps :: Outputable a
480        => a 
481        -> TcKind                        -- Function kind
482        -> [LHsType Name]                -- Arg types
483        -> TcM ([LHsType Name], TcKind)  -- Kind-checked args
484 kcApps the_fun fun_kind args
485   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
486        ; args' <- kc_check_lhs_types args_w_kinds
487        ; return (args', res_kind) }
488
489 kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
490             -> HsType Name     -- The type being checked (for err messages only)
491             -> ExpKind         -- Expected kind
492             -> TcM [LHsType Name]
493 kcCheckApps the_fun fun_kind args ty exp_kind
494   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
495        ; checkExpectedKind ty res_kind exp_kind
496              -- Check the result kind *before* checking argument kinds
497              -- This improves error message; Trac #2994
498        ; kc_check_lhs_types args_w_kinds }
499
500
501 ---------------------------
502 splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
503 splitFunKind _       _      fk [] = return ([], fk)
504 splitFunKind the_fun arg_no fk (arg:args)
505   = do { mb_fk <- matchExpectedFunKind fk
506        ; case mb_fk of
507             Nothing       -> failWithTc too_many_args 
508             Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
509                                 ; return ((arg, EK ak (EkArg (quotes the_fun) arg_no)):aks, rk) } }
510   where
511     too_many_args = quotes the_fun <+>
512                     ptext (sLit "is applied to too many type arguments")
513
514 ---------------------------
515 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
516 kcHsContext ctxt = wrapLocM (mapM kcHsLPredType) ctxt
517
518 kcHsLPredType :: LHsType Name -> TcM (LHsType Name)
519 kcHsLPredType pred = kc_check_lhs_type pred ekConstraint
520
521 ---------------------------
522 kcTyVar :: Name -> TcM TcKind
523 kcTyVar name = do       -- Could be a tyvar or a tycon
524     traceTc "lk1" (ppr name)
525     thing <- tcLookup name
526     traceTc "lk2" (ppr name <+> ppr thing)
527     case thing of 
528         ATyVar _ ty             -> return (typeKind ty)
529         AThing kind             -> return kind
530         AGlobal (ATyCon tc)     -> return (tyConKind tc)
531         _                       -> wrongThingErr "type" thing name
532
533 kcClass :: Name -> TcM TcKind
534 kcClass cls = do        -- Must be a class
535     thing <- tcLookup cls
536     case thing of
537         AThing kind                         -> return kind
538         AGlobal (ATyCon tc)
539           | Just cls <- tyConClass_maybe tc -> return (tyConKind (classTyCon cls))
540         _                                   -> wrongThingErr "class" thing cls
541 \end{code}
542
543
544 %************************************************************************
545 %*                                                                      *
546                 Desugaring
547 %*                                                                      *
548 %************************************************************************
549
550 The type desugarer
551
552         * Transforms from HsType to Type
553         * Zonks any kinds
554
555 It cannot fail, and does no validity checking, except for 
556 structural matters, such as
557         (a) spurious ! annotations.
558         (b) a class used as a type
559
560 \begin{code}
561 dsHsType :: LHsType Name -> TcM Type
562 -- All HsTyVarBndrs in the intput type are kind-annotated
563 dsHsType ty = ds_type (unLoc ty)
564
565 ds_type :: HsType Name -> TcM Type
566 ds_type ty@(HsTyVar _)
567   = ds_app ty []
568
569 ds_type (HsParTy ty)            -- Remove the parentheses markers
570   = dsHsType ty
571
572 ds_type ty@(HsBangTy {})    -- No bangs should be here
573   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
574
575 ds_type ty@(HsRecTy {})     -- No bangs should be here
576   = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
577
578 ds_type (HsKindSig ty _)
579   = dsHsType ty -- Kind checking done already
580
581 ds_type (HsListTy ty) = do
582     tau_ty <- dsHsType ty
583     checkWiredInTyCon listTyCon
584     return (mkListTy tau_ty)
585
586 ds_type (HsPArrTy ty) = do
587     tau_ty <- dsHsType ty
588     checkWiredInTyCon parrTyCon
589     return (mkPArrTy tau_ty)
590
591 ds_type (HsTupleTy hs_con tys) = do
592     con <- case hs_con of
593         HsUnboxedTuple -> return UnboxedTuple
594         HsBoxyTuple kind -> do
595           kind' <- zonkTcKindToKind kind
596           case () of
597             _ | kind' `eqKind` constraintKind -> return ConstraintTuple
598             _ | kind' `eqKind` liftedTypeKind -> return BoxedTuple
599             _ | otherwise
600               -> failWithTc (ptext (sLit "Unexpected tuple component kind:") <+> ppr kind')
601     let tycon = tupleTyCon con (length tys)
602     tau_tys <- dsHsTypes tys
603     checkWiredInTyCon tycon
604     return (mkTyConApp tycon tau_tys)
605
606 ds_type (HsFunTy ty1 ty2) = do
607     tau_ty1 <- dsHsType ty1
608     tau_ty2 <- dsHsType ty2
609     return (mkFunTy tau_ty1 tau_ty2)
610
611 ds_type (HsOpTy ty1 (L span op) ty2) = do
612     tau_ty1 <- dsHsType ty1
613     tau_ty2 <- dsHsType ty2
614     setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
615
616 ds_type ty@(HsAppTy _ _)
617   = ds_app ty []
618
619 ds_type (HsIParamTy n ty) = do
620     tau_ty <- dsHsType ty
621     return (mkIPPred n tau_ty)
622
623 ds_type (HsEqTy ty1 ty2) = do
624     tau_ty1 <- dsHsType ty1
625     tau_ty2 <- dsHsType ty2
626     return (mkEqPred (tau_ty1, tau_ty2))
627
628 ds_type (HsForAllTy _ tv_names ctxt ty)
629   = tcTyVarBndrs tv_names               $ \ tyvars -> do
630     theta <- mapM dsHsType (unLoc ctxt)
631     tau <- dsHsType ty
632     return (mkSigmaTy tyvars theta tau)
633
634 ds_type (HsDocTy ty _)  -- Remove the doc comment
635   = dsHsType ty
636
637 ds_type (HsSpliceTy _ _ kind) 
638   = do { kind' <- zonkTcKindToKind kind
639        ; newFlexiTyVarTy kind' }
640
641 ds_type (HsQuasiQuoteTy {}) = panic "ds_type"   -- Eliminated by renamer
642 ds_type (HsCoreTy ty)       = return ty
643
644 dsHsTypes :: [LHsType Name] -> TcM [Type]
645 dsHsTypes arg_tys = mapM dsHsType arg_tys
646 \end{code}
647
648 Help functions for type applications
649 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
650
651 \begin{code}
652 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
653 ds_app (HsAppTy ty1 ty2) tys
654   = ds_app (unLoc ty1) (ty2:tys)
655
656 ds_app ty tys = do
657     arg_tys <- dsHsTypes tys
658     case ty of
659         HsTyVar fun -> ds_var_app fun arg_tys
660         _           -> do fun_ty <- ds_type ty
661                           return (mkAppTys fun_ty arg_tys)
662
663 ds_var_app :: Name -> [Type] -> TcM Type
664 ds_var_app name arg_tys = do
665     thing <- tcLookup name
666     case thing of
667         ATyVar _ ty         -> return (mkAppTys ty arg_tys)
668         AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
669         _                   -> wrongThingErr "type" thing name
670 \end{code}
671
672 \begin{code}
673 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
674         -- Wrap a context around only if we want to show that contexts.  
675         -- Omit invisble ones and ones user's won't grok
676 addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing
677
678 typeCtxt :: HsType Name -> SDoc
679 typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
680 \end{code}
681
682 %************************************************************************
683 %*                                                                      *
684                 Type-variable binders
685 %*                                                                      *
686 %************************************************************************
687
688
689 \begin{code}
690 kcHsTyVars :: [LHsTyVarBndr Name] 
691            -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
692                                                 -- They scope over the thing inside
693            -> TcM r
694 kcHsTyVars tvs thing_inside
695   = do { kinded_tvs <- mapM (wrapLocM kcHsTyVar) tvs
696        ; tcExtendKindEnvTvs kinded_tvs thing_inside }
697
698 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
699         -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it      
700 kcHsTyVar (UserTyVar name _)  = UserTyVar name <$> newKindVar
701 kcHsTyVar tv@(KindedTyVar {}) = return tv
702
703 ------------------
704 tcTyVarBndrs :: [LHsTyVarBndr Name]     -- Kind-annotated binders, which need kind-zonking
705              -> ([TyVar] -> TcM r)
706              -> TcM r
707 -- Used when type-checking types/classes/type-decls
708 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
709 tcTyVarBndrs bndrs thing_inside = do
710     tyvars <- mapM (zonk . unLoc) bndrs
711     tcExtendTyVarEnv tyvars (thing_inside tyvars)
712   where
713     zonk (UserTyVar name kind) = do { kind' <- zonkTcKindToKind kind
714                                     ; return (mkTyVar name kind') }
715     zonk (KindedTyVar name kind) = return (mkTyVar name kind)
716
717 -----------------------------------
718 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
719 -- GADT decls can have a (perhaps partial) kind signature
720 --      e.g.  data T :: * -> * -> * where ...
721 -- This function makes up suitable (kinded) type variables for 
722 -- the argument kinds, and checks that the result kind is indeed *.
723 -- We use it also to make up argument type variables for for data instances.
724 tcDataKindSig Nothing = return []
725 tcDataKindSig (Just kind)
726   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
727         ; span <- getSrcSpanM
728         ; us   <- newUniqueSupply 
729         ; let uniqs = uniqsFromSupply us
730         ; return [ mk_tv span uniq str kind 
731                  | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
732   where
733     (arg_kinds, res_kind) = splitKindFunTys kind
734     mk_tv loc uniq str kind = mkTyVar name kind
735         where
736            name = mkInternalName uniq occ loc
737            occ  = mkOccName tvName str
738           
739     dnames = map ('$' :) names  -- Note [Avoid name clashes for associated data types]
740
741     names :: [String]
742     names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 
743
744 badKindSig :: Kind -> SDoc
745 badKindSig kind 
746  = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
747         2 (ppr kind)
748 \end{code}
749
750 Note [Avoid name clashes for associated data types]
751 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
752 Consider    class C a b where
753                data D b :: * -> *
754 When typechecking the decl for D, we'll invent an extra type variable for D,
755 to fill out its kind.  We *don't* want this type variable to be 'a', because
756 in an .hi file we'd get
757             class C a b where
758                data D b a 
759 which makes it look as if there are *two* type indices.  But there aren't!
760 So we use $a instead, which cannot clash with a user-written type variable.
761 Remember that type variable binders in interface files are just FastStrings,
762 not proper Names.
763
764 (The tidying phase can't help here because we don't tidy TyCons.  Another
765 alternative would be to record the number of indexing parameters in the 
766 interface file.)
767
768
769 %************************************************************************
770 %*                                                                      *
771                 Scoped type variables
772 %*                                                                      *
773 %************************************************************************
774
775
776 tcAddScopedTyVars is used for scoped type variables added by pattern
777 type signatures
778         e.g.  \ ((x::a), (y::a)) -> x+y
779 They never have explicit kinds (because this is source-code only)
780 They are mutable (because they can get bound to a more specific type).
781
782 Usually we kind-infer and expand type splices, and then
783 tupecheck/desugar the type.  That doesn't work well for scoped type
784 variables, because they scope left-right in patterns.  (e.g. in the
785 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
786
787 The current not-very-good plan is to
788   * find all the types in the patterns
789   * find their free tyvars
790   * do kind inference
791   * bring the kinded type vars into scope
792   * BUT throw away the kind-checked type
793         (we'll kind-check it again when we type-check the pattern)
794
795 This is bad because throwing away the kind checked type throws away
796 its splices.  But too bad for now.  [July 03]
797
798 Historical note:
799     We no longer specify that these type variables must be univerally 
800     quantified (lots of email on the subject).  If you want to put that 
801     back in, you need to
802         a) Do a checkSigTyVars after thing_inside
803         b) More insidiously, don't pass in expected_ty, else
804            we unify with it too early and checkSigTyVars barfs
805            Instead you have to pass in a fresh ty var, and unify
806            it with expected_ty afterwards
807
808 \begin{code}
809 tcHsPatSigType :: UserTypeCtxt
810                -> LHsType Name          -- The type signature
811                -> TcM ([TyVar],         -- Newly in-scope type variables
812                         Type)           -- The signature
813 -- Used for type-checking type signatures in
814 -- (a) patterns           e.g  f (x::Int) = e
815 -- (b) result signatures  e.g. g x :: Int = e
816 -- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
817
818 tcHsPatSigType ctxt hs_ty 
819   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
820     do  {       -- Find the type variables that are mentioned in the type
821                 -- but not already in scope.  These are the ones that
822                 -- should be bound by the pattern signature
823           in_scope <- getInLocalScope
824         ; let span = getLoc hs_ty
825               sig_tvs = userHsTyVarBndrs $ map (L span) $ 
826                         filterOut in_scope $
827                         nameSetToList (extractHsTyVars hs_ty)
828
829         ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
830         ; checkValidType ctxt sig_ty 
831         ; return (tyvars, sig_ty)
832       }
833
834 tcPatSig :: UserTypeCtxt
835          -> LHsType Name
836          -> TcSigmaType
837          -> TcM (TcType,           -- The type to use for "inside" the signature
838                  [(Name, TcType)], -- The new bit of type environment, binding
839                                    -- the scoped type variables
840                  HsWrapper)        -- Coercion due to unification with actual ty
841                                    -- Of shape:  res_ty ~ sig_ty
842 tcPatSig ctxt sig res_ty
843   = do  { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
844         -- sig_tvs are the type variables free in 'sig', 
845         -- and not already in scope. These are the ones
846         -- that should be brought into scope
847
848         ; if null sig_tvs then do {
849                 -- The type signature binds no type variables, 
850                 -- and hence is rigid, so use it to zap the res_ty
851                   wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
852                 ; return (sig_ty, [], wrap)
853         } else do {
854                 -- Type signature binds at least one scoped type variable
855         
856                 -- A pattern binding cannot bind scoped type variables
857                 -- The renamer fails with a name-out-of-scope error 
858                 -- if a pattern binding tries to bind a type variable,
859                 -- So we just have an ASSERT here
860         ; let in_pat_bind = case ctxt of
861                                 BindPatSigCtxt -> True
862                                 _              -> False
863         ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
864
865                 -- Check that all newly-in-scope tyvars are in fact
866                 -- constrained by the pattern.  This catches tiresome
867                 -- cases like   
868                 --      type T a = Int
869                 --      f :: Int -> Int
870                 --      f (x :: T a) = ...
871                 -- Here 'a' doesn't get a binding.  Sigh
872         ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
873         ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
874
875         -- Now do a subsumption check of the pattern signature against res_ty
876         ; sig_tvs' <- tcInstSigTyVars sig_tvs
877         ; let sig_ty' = substTyWith sig_tvs sig_tv_tys' sig_ty
878               sig_tv_tys' = mkTyVarTys sig_tvs'
879         ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty'
880
881         -- Check that each is bound to a distinct type variable,
882         -- and one that is not already in scope
883         ; binds_in_scope <- getScopedTyVarBinds
884         ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys'
885         ; check binds_in_scope tv_binds
886         
887         -- Phew!
888         ; return (sig_ty', tv_binds, wrap)
889         } }
890   where
891     check _ [] = return ()
892     check in_scope ((n,ty):rest) = do { check_one in_scope n ty
893                                       ; check ((n,ty):in_scope) rest }
894
895     check_one in_scope n ty
896         = checkTc (null dups) (dupInScope n (head dups) ty)
897                 -- Must not bind to the same type variable
898                 -- as some other in-scope type variable
899         where
900           dups = [n' | (n',ty') <- in_scope, eqType ty' ty]
901 \end{code}
902
903
904 %************************************************************************
905 %*                                                                      *
906         Checking kinds
907 %*                                                                      *
908 %************************************************************************
909
910 We would like to get a decent error message from
911   (a) Under-applied type constructors
912              f :: (Maybe, Maybe)
913   (b) Over-applied type constructors
914              f :: Int x -> Int x
915
916 \begin{code}
917 -- The ExpKind datatype means "expected kind" and contains 
918 -- some info about just why that kind is expected, to improve
919 -- the error message on a mis-match
920 data ExpKind = EK TcKind EkCtxt
921 data EkCtxt  = EkUnk            -- Unknown context
922              | EkEqPred         -- Second argument of an equality predicate
923              | EkKindSig        -- Kind signature
924              | EkArg SDoc Int   -- Function, arg posn, expected kind
925              | EkIParam         -- Implicit parameter type
926              | EkFamInst        -- Family instance
927
928
929 ekLifted, ekOpen, ekConstraint :: ExpKind
930 ekLifted     = EK liftedTypeKind EkUnk
931 ekOpen       = EK openTypeKind   EkUnk
932 ekConstraint = EK constraintKind EkUnk
933
934 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
935 -- A fancy wrapper for 'unifyKind', which tries
936 -- to give decent error messages.
937 --      (checkExpectedKind ty act_kind exp_kind)
938 -- checks that the actual kind act_kind is compatible
939 --      with the expected kind exp_kind
940 -- The first argument, ty, is used only in the error message generation
941 checkExpectedKind ty act_kind (EK exp_kind ek_ctxt) = do
942     (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
943     case mb_r of
944         Just _  -> return ()  -- Unification succeeded
945         Nothing -> do
946
947         -- So there's definitely an error
948         -- Now to find out what sort
949            exp_kind <- zonkTcKind exp_kind
950            act_kind <- zonkTcKind act_kind
951
952            env0 <- tcInitTidyEnv
953            let (exp_as, _) = splitKindFunTys exp_kind
954                (act_as, _) = splitKindFunTys act_kind
955                n_exp_as = length exp_as
956                n_act_as = length act_as
957
958                (env1, tidy_exp_kind) = tidyKind env0 exp_kind
959                (env2, tidy_act_kind) = tidyKind env1 act_kind
960
961                err | n_exp_as < n_act_as     -- E.g. [Maybe]
962                    = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
963
964                      -- Now n_exp_as >= n_act_as. In the next two cases,
965                      -- n_exp_as == 0, and hence so is n_act_as
966                    | isConstraintKind tidy_act_kind
967                    = text "Predicate" <+> quotes (ppr ty) <+> text "used as a type"
968                    
969                    | isConstraintKind tidy_exp_kind
970                    = text "Type of kind " <+> ppr tidy_act_kind <+> text "used as a constraint"
971                    
972                    | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
973                    = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
974                        <+> ptext (sLit "is unlifted")
975
976                    | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
977                    = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
978                        <+> ptext (sLit "is lifted")
979
980                    | otherwise               -- E.g. Monad [Int]
981                    = ptext (sLit "Kind mis-match")
982
983                more_info = sep [ expected_herald ek_ctxt <+> ptext (sLit "kind") 
984                                     <+> quotes (pprKind tidy_exp_kind) <> comma,
985                                  ptext (sLit "but") <+> quotes (ppr ty) <+>
986                                      ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
987
988                expected_herald EkUnk     = ptext (sLit "Expected")
989                expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
990                expected_herald EkEqPred  = ptext (sLit "The left argument of the equality predicate had")
991                expected_herald EkIParam  = ptext (sLit "The type argument of the implicit parameter had")
992                expected_herald EkFamInst = ptext (sLit "The family instance required")
993                expected_herald (EkArg fun arg_no)
994                  = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
995                    <+> fun <+> ptext (sLit ("should have"))
996
997            failWithTcM (env2, err $$ more_info)
998 \end{code}
999
1000 %************************************************************************
1001 %*                                                                      *
1002                 Scoped type variables
1003 %*                                                                      *
1004 %************************************************************************
1005
1006 \begin{code}
1007 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
1008 pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon, 
1009                                  nest 2 (pp_sig ctxt) ]
1010   where
1011     pp_sig (FunSigCtxt n)  = pp_n_colon n
1012     pp_sig (ConArgCtxt n)  = pp_n_colon n
1013     pp_sig (ForSigCtxt n)  = pp_n_colon n
1014     pp_sig _               = ppr (unLoc hs_ty)
1015
1016     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
1017
1018 badPatSigTvs :: TcType -> [TyVar] -> SDoc
1019 badPatSigTvs sig_ty bad_tvs
1020   = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, 
1021                  quotes (pprWithCommas ppr bad_tvs), 
1022                  ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
1023                  ptext (sLit "but are actually discarded by a type synonym") ]
1024          , ptext (sLit "To fix this, expand the type synonym") 
1025          , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
1026
1027 dupInScope :: Name -> Name -> Type -> SDoc
1028 dupInScope n n' _
1029   = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
1030        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
1031                 ptext (sLit "Distinct scoped type variables must be distinct")])
1032 \end{code}
1033