f26bfbbf9ae6370bbf0a9c6f78b76bd24f57a047
[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 {-# OPTIONS -fno-warn-tabs #-}
9 -- The above warning supression flag is a temporary kludge.
10 -- While working on this module you are encouraged to remove it and
11 -- detab the module (please do the detabbing in a separate patch). See
12 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
13 -- for details
14
15 module TcHsType (
16         tcHsSigType, tcHsSigTypeNC, tcHsDeriv, tcHsVectInst, 
17         tcHsInstHead, tcHsQuantifiedType,
18         UserTypeCtxt(..), 
19
20                 -- Kind checking
21         kcHsTyVars, kcHsSigType, kcHsLiftedSigType, 
22         kcLHsType, kcCheckLHsType, kcHsContext, kcApps,
23         kindGeneralizeKind, kindGeneralizeKinds,
24
25                 -- Sort checking
26         scDsLHsKind, scDsLHsMaybeKind,
27
28                 -- Typechecking kinded types
29         tcHsType, tcCheckHsType,
30         tcHsKindedContext, tcHsKindedType, tcHsBangType,
31         tcTyVarBndrs, tcTyVarBndrsKindGen, dsHsType,
32         tcDataKindSig, tcTyClTyVars,
33
34         ExpKind(..), ekConstraint, expArgKind, checkExpectedKind,
35
36                 -- Pattern type signatures
37         tcHsPatSigType, tcPatSig
38    ) where
39
40 #include "HsVersions.h"
41
42 #ifdef GHCI     /* Only if bootstrapped */
43 import {-# SOURCE #-}   TcSplice( kcSpliceType )
44 #endif
45
46 import HsSyn
47 import RnHsSyn
48 import TcRnMonad
49 import RnEnv   ( dataKindsErr )
50 import TcHsSyn ( mkZonkTcTyVar )
51 import TcEvidence( HsWrapper )
52 import TcEnv
53 import TcMType
54 import TcUnify
55 import TcIface
56 import TcType
57 import {- Kind parts of -} Type
58 import Kind
59 import Var
60 import VarSet
61 import TyCon
62 import DataCon
63 import TysPrim ( liftedTypeKindTyConName, constraintKindTyConName )
64 import Class
65 import RdrName ( rdrNameSpace, nameRdrName )
66 import Name
67 import NameSet
68 import TysWiredIn
69 import BasicTypes
70 import SrcLoc
71 import DynFlags ( ExtensionFlag( Opt_DataKinds ) )
72 import Util
73 import UniqSupply
74 import Outputable
75 import FastString
76 import Control.Monad ( unless )
77 \end{code}
78
79
80         ----------------------------
81                 General notes
82         ----------------------------
83
84 Generally speaking we now type-check types in three phases
85
86   1.  kcHsType: kind check the HsType
87         *includes* performing any TH type splices;
88         so it returns a translated, and kind-annotated, type
89
90   2.  dsHsType: convert from HsType to Type:
91         perform zonking
92         expand type synonyms [mkGenTyApps]
93         hoist the foralls [tcHsType]
94
95   3.  checkValidType: check the validity of the resulting type
96
97 Often these steps are done one after the other (tcHsSigType).
98 But in mutually recursive groups of type and class decls we do
99         1 kind-check the whole group
100         2 build TyCons/Classes in a knot-tied way
101         3 check the validity of types in the now-unknotted TyCons/Classes
102
103 For example, when we find
104         (forall a m. m a -> m a)
105 we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
106 a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
107 an environment that binds a and m suitably.
108
109 The kind checker passed to tcHsTyVars needs to look at enough to
110 establish the kind of the tyvar:
111   * For a group of type and class decls, it's just the group, not
112         the rest of the program
113   * For a tyvar bound in a pattern type signature, its the types
114         mentioned in the other type signatures in that bunch of patterns
115   * For a tyvar bound in a RULE, it's the type signatures on other
116         universally quantified variables in the rule
117
118 Note that this may occasionally give surprising results.  For example:
119
120         data T a b = MkT (a b)
121
122 Here we deduce                  a::*->*,       b::*
123 But equally valid would be      a::(*->*)-> *, b::*->*
124
125
126 Validity checking
127 ~~~~~~~~~~~~~~~~~
128 Some of the validity check could in principle be done by the kind checker, 
129 but not all:
130
131 - During desugaring, we normalise by expanding type synonyms.  Only
132   after this step can we check things like type-synonym saturation
133   e.g.  type T k = k Int
134         type S a = a
135   Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
136   and then S is saturated.  This is a GHC extension.
137
138 - Similarly, also a GHC extension, we look through synonyms before complaining
139   about the form of a class or instance declaration
140
141 - Ambiguity checks involve functional dependencies, and it's easier to wait
142   until knots have been resolved before poking into them
143
144 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
145 finished building the loop.  So to keep things simple, we postpone most validity
146 checking until step (3).
147
148 Knot tying
149 ~~~~~~~~~~
150 During step (1) we might fault in a TyCon defined in another module, and it might
151 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
152 knot around type declarations with ARecThing, so that the fault-in code can get
153 the TyCon being defined.
154
155
156 %************************************************************************
157 %*                                                                      *
158 \subsection{Checking types}
159 %*                                                                      *
160 %************************************************************************
161
162 \begin{code}
163 tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
164   -- Do kind checking, and hoist for-alls to the top
165   -- NB: it's important that the foralls that come from the top-level
166   --     HsForAllTy in hs_ty occur *first* in the returned type.
167   --     See Note [Scoped] with TcSigInfo
168 tcHsSigType ctxt hs_ty 
169   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
170     tcHsSigTypeNC ctxt hs_ty
171
172 tcHsSigTypeNC ctxt hs_ty
173   = do  { kinded_ty <- case expectedKindInCtxt ctxt of
174                          Nothing -> fmap fst (kc_lhs_type_fresh hs_ty)
175                          Just k  -> kc_lhs_type hs_ty (EK k (ptext (sLit "Expected")))
176           -- The kind is checked by checkValidType, and isn't necessarily
177           -- of kind * in a Template Haskell quote eg [t| Maybe |]
178         ; ty <- tcHsKindedType kinded_ty
179         ; checkValidType ctxt ty
180         ; return ty }
181
182 -- Like tcHsType, but takes an expected kind
183 tcCheckHsType :: LHsType Name -> Kind -> TcM Type
184 tcCheckHsType hs_ty exp_kind
185   = do { kinded_ty <- kcCheckLHsType hs_ty (EK exp_kind (ptext (sLit "Expected")))
186        ; ty <- tcHsKindedType kinded_ty
187        ; return ty }
188
189 tcHsType :: LHsType Name -> TcM Type
190 -- kind check and desugar
191 -- no validity checking because of knot-tying
192 tcHsType hs_ty
193   = do { (kinded_ty, _) <- kc_lhs_type_fresh hs_ty
194        ; ty <- tcHsKindedType kinded_ty
195        ; return ty }
196
197 tcHsInstHead :: UserTypeCtxt -> LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
198 -- Typecheck an instance head.  We can't use 
199 -- tcHsSigType, because it's not a valid user type.
200 tcHsInstHead ctxt lhs_ty@(L loc hs_ty)
201   = setSrcSpan loc   $  -- No need for an "In the type..." context
202                         -- because that comes from the caller
203     do { kinded_ty <- kc_hs_type hs_ty ekConstraint
204        ; ty <- ds_type kinded_ty
205        ; let (tvs, theta, tau) = tcSplitSigmaTy ty
206        ; case getClassPredTys_maybe tau of
207            Nothing          -> failWithTc (ptext (sLit "Malformed instance type"))
208            Just (clas,tys)  -> do { checkValidInstance ctxt lhs_ty tvs theta clas tys
209                                   ; return (tvs, theta, clas, tys) } }
210
211 tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
212 -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
213 -- except that we want to keep the tvs separate
214 tcHsQuantifiedType tv_names hs_ty
215   = kcHsTyVars tv_names $ \ tv_names' ->
216     do  { kc_ty <- kcHsSigType hs_ty
217         ; tcTyVarBndrs tv_names' $ \ tvs ->
218     do  { ty <- dsHsType kc_ty
219         ; return (tvs, ty) } }
220
221 -- Used for the deriving(...) items
222 tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
223 tcHsDeriv = tc_hs_deriv []
224
225 tc_hs_deriv :: [LHsTyVarBndr Name] -> HsType Name
226             -> TcM ([TyVar], Class, [Type])
227 tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
228   =     -- Funny newtype deriving form
229         --      forall a. C [a]
230         -- where C has arity 2.  Hence can't use regular functions
231     tc_hs_deriv (tv_names1 ++ tv_names2) ty
232
233 tc_hs_deriv tv_names ty
234   | Just (cls_name, hs_tys) <- splitHsClassTy_maybe ty
235   = kcHsTyVars tv_names                 $ \ tv_names' ->
236     do  { cls_kind <- kcClass cls_name
237         ; (tys, _res_kind) <- kcApps cls_name cls_kind hs_tys
238         ; tcTyVarBndrsKindGen tv_names'        $ \ tyvars ->
239     do  { arg_tys <- dsHsTypes tys
240         ; cls <- tcLookupClass cls_name
241         ; return (tyvars, cls, arg_tys) }}
242
243   | otherwise
244   = failWithTc (ptext (sLit "Illegal deriving item") <+> ppr ty)
245
246 -- Used for 'VECTORISE [SCALAR] instance' declarations
247 --
248 tcHsVectInst :: LHsType Name -> TcM (Class, [Type])
249 tcHsVectInst ty
250   | Just (L _ cls_name, tys) <- splitLHsClassTy_maybe ty
251   = do { cls_kind <- kcClass cls_name
252        ; (tys, _res_kind) <- kcApps cls_name cls_kind tys
253        ; arg_tys <- dsHsTypes tys
254        ; cls <- tcLookupClass cls_name
255        ; return (cls, arg_tys)
256        }
257   | otherwise
258   = failWithTc $ ptext (sLit "Malformed instance type")
259 \end{code}
260
261         These functions are used during knot-tying in
262         type and class declarations, when we have to
263         separate kind-checking, desugaring, and validity checking
264
265 \begin{code}
266 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
267         -- Used for type signatures
268 kcHsSigType ty       = addKcTypeCtxt ty $ kcArgType ty
269 kcHsLiftedSigType ty = addKcTypeCtxt ty $ kcLiftedType ty
270
271 tcHsKindedType :: LHsType Name -> TcM Type
272   -- Don't do kind checking, nor validity checking.
273   -- This is used in type and class decls, where kinding is
274   -- done in advance, and validity checking is done later
275   -- [Validity checking done later because of knot-tying issues.]
276 tcHsKindedType hs_ty = dsHsType hs_ty
277
278 tcHsBangType :: LHsType Name -> TcM Type
279 -- Permit a bang, but discard it
280 -- Input type has already been kind-checked
281 tcHsBangType (L _ (HsBangTy _ ty)) = tcHsKindedType ty
282 tcHsBangType ty                    = tcHsKindedType ty
283
284 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
285 -- Used when we are expecting a ClassContext (i.e. no implicit params)
286 -- Does not do validity checking, like tcHsKindedType
287 tcHsKindedContext hs_theta = addLocM (mapM dsHsType) hs_theta
288 \end{code}
289
290
291 %************************************************************************
292 %*                                                                      *
293                 The main kind checker: kcHsType
294 %*                                                                      *
295 %************************************************************************
296         
297         First a couple of simple wrappers for kcHsType
298
299 \begin{code}
300 ---------------------------
301 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
302 -- The type ty must be a *lifted* *type*
303 kcLiftedType ty = kc_lhs_type ty ekLifted
304     
305 kcArgs :: SDoc -> [LHsType Name] -> Kind -> TcM [LHsType Name]
306 kcArgs what tys kind 
307   = sequence [ kc_lhs_type ty (expArgKind what kind n)
308              | (ty,n) <- tys `zip` [1..] ]
309
310 ---------------------------
311 kcArgType :: LHsType Name -> TcM (LHsType Name)
312 -- The type ty must be an *arg* *type* (lifted or unlifted)
313 kcArgType ty = kc_lhs_type ty ekArg
314
315 ---------------------------
316 kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)
317 kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_lhs_type ty kind
318 \end{code}
319
320 Like tcExpr, kc_hs_type takes an expected kind which it unifies with
321 the kind it figures out. When we don't know what kind to expect, we use
322 kc_lhs_type_fresh, to first create a new meta kind variable and use that as
323 the expected kind.
324
325 \begin{code}
326 kcLHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
327 -- Called from outside: set the context
328 kcLHsType ty = addKcTypeCtxt ty (kc_lhs_type_fresh ty)
329
330 kc_lhs_type_fresh :: LHsType Name -> TcM (LHsType Name, TcKind)
331 kc_lhs_type_fresh ty =  do
332   kv <- newMetaKindVar
333   r <- kc_lhs_type ty (EK kv (ptext (sLit "Expected")))
334   return (r, kv)
335
336 kc_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [LHsType Name]
337 kc_lhs_types tys_w_kinds = mapM (uncurry kc_lhs_type) tys_w_kinds
338
339 kc_lhs_type :: LHsType Name -> ExpKind -> TcM (LHsType Name)
340 kc_lhs_type (L span ty) exp_kind
341   = setSrcSpan span $
342     do { traceTc "kc_lhs_type" (ppr ty <+> ppr exp_kind)
343        ; ty' <- kc_hs_type ty exp_kind
344        ; return (L span ty') }
345
346 kc_hs_type :: HsType Name -> ExpKind -> TcM (HsType Name)
347 kc_hs_type (HsParTy ty) exp_kind = do
348    ty' <- kc_lhs_type ty exp_kind
349    return (HsParTy ty')
350
351 kc_hs_type (HsTyVar name) exp_kind = do
352    (ty, k) <- kcTyVar name
353    checkExpectedKind ty k exp_kind
354    return ty
355
356 kc_hs_type (HsListTy ty) exp_kind = do
357     ty' <- kcLiftedType ty
358     checkExpectedKind ty liftedTypeKind exp_kind
359     return (HsListTy ty')
360
361 kc_hs_type (HsPArrTy ty) exp_kind = do
362     ty' <- kcLiftedType ty
363     checkExpectedKind ty liftedTypeKind exp_kind
364     return (HsPArrTy ty')
365
366 kc_hs_type (HsKindSig ty sig_k) exp_kind = do
367     sig_k' <- scDsLHsKind sig_k
368     ty' <- kc_lhs_type ty
369              (EK sig_k' (ptext (sLit "An enclosing kind signature specified")))
370     checkExpectedKind ty sig_k' exp_kind
371     return (HsKindSig ty' sig_k)
372
373 -- See Note [Distinguishing tuple kinds] in HsTypes
374 kc_hs_type ty@(HsTupleTy HsBoxedOrConstraintTuple tys) exp_kind@(EK exp_k _ctxt)
375   | isConstraintOrLiftedKind exp_k -- (NB: not zonking, to avoid left-right bias)
376   = do { tys' <- kcArgs (ptext (sLit "a tuple")) tys exp_k
377        ; return $ if isConstraintKind exp_k
378                     then HsTupleTy HsConstraintTuple tys'
379                     else HsTupleTy HsBoxedTuple      tys' }
380   | otherwise
381   -- It is not clear from the context if it's * or Constraint, 
382   -- so we infer the kind from the arguments
383   = do { k <- newMetaKindVar
384        ; tys' <- kcArgs (ptext (sLit "a tuple")) tys k 
385        ; k' <- zonkTcKind k
386        ; if isConstraintKind k'
387          then do { checkExpectedKind ty k' exp_kind
388                  ; return (HsTupleTy HsConstraintTuple tys') }
389          -- If it's not clear from the arguments that it's Constraint, then
390          -- it must be *. Check the arguments again to give good error messages
391          -- in eg. `(Maybe, Maybe)`
392          else do { tys'' <- kcArgs (ptext (sLit "a tuple")) tys liftedTypeKind
393                  ; checkExpectedKind ty liftedTypeKind exp_kind
394                  ; return (HsTupleTy HsBoxedTuple tys'') } }
395 {-
396 Note that we will still fail to infer the correct kind in this case:
397
398   type T a = ((a,a), D a)
399   type family D :: Constraint -> Constraint
400
401 While kind checking T, we do not yet know the kind of D, so we will default the
402 kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
403 -}
404
405 kc_hs_type ty@(HsTupleTy tup_sort tys) exp_kind
406   = do { tys' <- kcArgs cxt_doc tys arg_kind
407        ; checkExpectedKind ty out_kind exp_kind
408        ; return (HsTupleTy tup_sort tys') }
409   where
410     arg_kind = case tup_sort of
411                  HsBoxedTuple      -> liftedTypeKind
412                  HsUnboxedTuple    -> argTypeKind
413                  HsConstraintTuple -> constraintKind
414                  _                 -> panic "kc_hs_type arg_kind"
415     out_kind = case tup_sort of
416                  HsUnboxedTuple    -> ubxTupleKind
417                  _                 -> arg_kind
418     cxt_doc = case tup_sort of
419                  HsBoxedTuple      -> ptext (sLit "a tuple")
420                  HsUnboxedTuple    -> ptext (sLit "an unboxed tuple")
421                  HsConstraintTuple -> ptext (sLit "a constraint tuple")
422                  _                 -> panic "kc_hs_type tup_sort"
423
424 kc_hs_type ty@(HsFunTy ty1 ty2) exp_kind@(EK _ ctxt) = do
425     ty1' <- kc_lhs_type ty1 (EK argTypeKind  ctxt)
426     ty2' <- kc_lhs_type ty2 (EK openTypeKind ctxt)
427     checkExpectedKind ty liftedTypeKind exp_kind
428     return (HsFunTy ty1' ty2')
429
430 kc_hs_type ty@(HsOpTy ty1 (_, l_op@(L loc op)) ty2) exp_kind = do
431     (wop, op_kind) <- kcTyVar op
432     [ty1',ty2'] <- kcCheckApps l_op op_kind [ty1,ty2] ty exp_kind
433     let op' = case wop of
434                 HsTyVar name -> (WpKiApps [], L loc name)
435                 HsWrapTy wrap (HsTyVar name) -> (wrap, L loc name)
436                 _ -> panic "kc_hs_type HsOpTy"
437     return (HsOpTy ty1' op' ty2')
438
439 kc_hs_type ty@(HsAppTy ty1 ty2) exp_kind = do
440     let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
441     (fun_ty', fun_kind) <- kc_lhs_type_fresh fun_ty
442     arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
443     return (mkHsAppTys fun_ty' arg_tys')
444
445 kc_hs_type ipTy@(HsIParamTy n ty) exp_kind = do
446     ty' <- kc_lhs_type ty 
447              (EK liftedTypeKind 
448                (ptext (sLit "The type argument of the implicit parameter had")))
449     checkExpectedKind ipTy constraintKind exp_kind
450     return (HsIParamTy n ty')
451
452 kc_hs_type ty@(HsEqTy ty1 ty2) exp_kind = do
453     (ty1', kind1) <- kc_lhs_type_fresh ty1
454     (ty2', kind2) <- kc_lhs_type_fresh ty2
455     checkExpectedKind ty2 kind2
456       (EK kind1 (ptext (sLit "The left argument of the equality predicate had")))
457     checkExpectedKind ty constraintKind exp_kind
458     return (HsEqTy ty1' ty2')
459
460 kc_hs_type (HsCoreTy ty) exp_kind = do
461     checkExpectedKind ty (typeKind ty) exp_kind
462     return (HsCoreTy ty)
463
464 kc_hs_type (HsForAllTy exp tv_names context ty) exp_kind
465   = kcHsTyVars tv_names         $ \ tv_names' ->
466     do  { ctxt' <- kcHsContext context
467         ; ty'   <- kc_lhs_type ty exp_kind
468              -- The body of a forall is usually a type, but in principle
469              -- there's no reason to prohibit *unlifted* types.
470              -- In fact, GHC can itself construct a function with an
471              -- unboxed tuple inside a for-all (via CPR analyis; see 
472              -- typecheck/should_compile/tc170).
473              --
474              -- Moreover in instance heads we get forall-types with
475              -- kind Constraint.  
476              --
477              -- Really we should check that it's a type of value kind
478              -- {*, Constraint, #}, but I'm not doing that yet
479              -- Example that should be rejected:  
480              --          f :: (forall (a:*->*). a) Int
481         ; return (HsForAllTy exp tv_names' ctxt' ty') }
482
483 kc_hs_type (HsBangTy b ty) exp_kind
484   = do { ty' <- kc_lhs_type ty exp_kind
485        ; return (HsBangTy b ty') }
486
487 kc_hs_type ty@(HsRecTy _) _exp_kind
488   = failWithTc (ptext (sLit "Unexpected record type") <+> ppr ty)
489       -- Record types (which only show up temporarily in constructor signatures) 
490       -- should have been removed by now
491
492 #ifdef GHCI     /* Only if bootstrapped */
493 kc_hs_type (HsSpliceTy sp fvs _) exp_kind = do
494     (ty, k) <- kcSpliceType sp fvs
495     checkExpectedKind ty k exp_kind
496     return ty
497 #else
498 kc_hs_type ty@(HsSpliceTy {}) _exp_kind =
499     failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
500 #endif
501
502 kc_hs_type (HsQuasiQuoteTy {}) _exp_kind =
503     panic "kc_hs_type"  -- Eliminated by renamer
504
505 -- Remove the doc nodes here, no need to worry about the location since
506 -- it's the same for a doc node and its child type node
507 kc_hs_type (HsDocTy ty _) exp_kind
508   = kc_hs_type (unLoc ty) exp_kind
509
510 kc_hs_type ty@(HsExplicitListTy _k tys) exp_kind
511   = do { ty_k_s <- mapM kc_lhs_type_fresh tys
512        ; kind <- unifyKinds (ptext (sLit "In a promoted list")) ty_k_s
513        ; checkExpectedKind ty (mkPromotedListTy kind) exp_kind
514        ; return (HsExplicitListTy kind (map fst ty_k_s)) }
515
516 kc_hs_type ty@(HsExplicitTupleTy _ tys) exp_kind = do
517   ty_k_s <- mapM kc_lhs_type_fresh tys
518   let tycon   = promotedTupleTyCon BoxedTuple (length tys)
519       tupleKi = mkTyConApp tycon (map snd ty_k_s)
520   checkExpectedKind ty tupleKi exp_kind
521   return (HsExplicitTupleTy (map snd ty_k_s) (map fst ty_k_s))
522
523 kc_hs_type (HsWrapTy {}) _exp_kind =
524     panic "kc_hs_type HsWrapTy"  -- We kind checked something twice
525
526 ---------------------------
527 kcApps :: Outputable a
528        => a 
529        -> TcKind                        -- Function kind
530        -> [LHsType Name]                -- Arg types
531        -> TcM ([LHsType Name], TcKind)  -- Kind-checked args
532 kcApps the_fun fun_kind args
533   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
534        ; args' <- kc_lhs_types args_w_kinds
535        ; return (args', res_kind) }
536
537 kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
538             -> HsType Name     -- The type being checked (for err messages only)
539             -> ExpKind         -- Expected kind
540             -> TcM ([LHsType Name])
541 kcCheckApps the_fun fun_kind args ty exp_kind
542   = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
543        ; args_w_kinds' <- kc_lhs_types args_w_kinds
544        ; checkExpectedKind ty res_kind exp_kind
545        ; return args_w_kinds' }
546
547
548 ---------------------------
549 splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
550 splitFunKind _       _      fk [] = return ([], fk)
551 splitFunKind the_fun arg_no fk (arg:args)
552   = do { mb_fk <- matchExpectedFunKind fk
553        ; case mb_fk of
554             Nothing       -> failWithTc too_many_args 
555             Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
556                                 ; return ((arg
557                                           ,expArgKind (quotes the_fun) ak arg_no)
558                                          :aks ,rk) } }
559   where
560     too_many_args = quotes the_fun <+>
561                     ptext (sLit "is applied to too many type arguments")
562
563 ---------------------------
564 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
565 kcHsContext ctxt = wrapLocM (mapM kcHsLPredType) ctxt
566
567 kcHsLPredType :: LHsType Name -> TcM (LHsType Name)
568 kcHsLPredType pred = kc_lhs_type pred ekConstraint
569
570 ---------------------------
571 kcTyVar :: Name -> TcM (HsType Name, TcKind)
572 -- See Note [Type checking recursive type and class declarations]
573 -- in TcTyClsDecls
574 kcTyVar name         -- Could be a tyvar, a tycon, or a datacon
575   = do { traceTc "lk1" (ppr name)
576        ; thing <- tcLookup name
577        ; traceTc "lk2" (ppr name <+> ppr thing)
578        ; case thing of
579            ATyVar _ tv           -> wrap_mono (tyVarKind tv)
580            AThing kind           -> wrap_poly kind
581            AGlobal (ATyCon tc)   -> wrap_poly (tyConKind tc)
582            AGlobal (ADataCon dc) -> kcDataCon dc >>= wrap_poly
583            _                     -> wrongThingErr "type" thing name }
584   where
585     wrap_mono kind = do { traceTc "lk3" (ppr name <+> dcolon <+> ppr kind)
586                         ; return (HsTyVar name, kind) }
587     wrap_poly kind
588       | null kvs = wrap_mono kind
589       | otherwise
590       = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind)
591            ; kvs' <- mapM (const newMetaKindVar) kvs
592            ; let ki = substKiWith kvs kvs' ki_body
593            ; return (HsWrapTy (WpKiApps kvs') (HsTyVar name), ki) }
594       where (kvs, ki_body) = splitForAllTys kind
595
596 -- IA0_TODO: this function should disapear, and use the dcPromoted field of DataCon
597 kcDataCon :: DataCon -> TcM TcKind
598 kcDataCon dc = do
599   let ty = dataConUserType dc
600   unless (isPromotableType ty) $ promoteErr dc ty
601   let ki = promoteType ty
602   traceTc "prm" (ppr ty <+> ptext (sLit "~~>") <+> ppr ki)
603   return ki
604   where
605     promoteErr dc ty = failWithTc (quotes (ppr dc) <+> ptext (sLit "of type")
606       <+> quotes (ppr ty) <+> ptext (sLit "is not promotable"))
607
608 kcClass :: Name -> TcM TcKind
609 kcClass cls = do        -- Must be a class
610     thing <- tcLookup cls
611     case thing of
612         AThing kind                         -> return kind
613         AGlobal (ATyCon tc)
614           | Just cls <- tyConClass_maybe tc -> return (tyConKind (classTyCon cls))
615         _                                   -> wrongThingErr "class" thing cls
616 \end{code}
617
618
619 %************************************************************************
620 %*                                                                      *
621                 Desugaring
622 %*                                                                      *
623 %************************************************************************
624
625 Note [Desugaring types]
626 ~~~~~~~~~~~~~~~~~~~~~~~
627 The type desugarer is phase 2 of dealing with HsTypes.  Specifically:
628
629   * It transforms from HsType to Type
630
631   * It zonks any kinds.  The returned type should have no mutable kind
632     or type variables (hence returning Type not TcType):
633       - any unconstrained kind variables are defaulted to AnyK just 
634         as in TcHsSyn. 
635       - there are no mutable type variables because we are 
636         kind-checking a type
637     Reason: the returned type may be put in a TyCon or DataCon where
638     it will never subsequently be zonked.
639
640 You might worry about nested scopes:
641         ..a:kappa in scope..
642             let f :: forall b. T '[a,b] -> Int
643 In this case, f's type could have a mutable kind variable kappa in it;
644 and we might then default it to AnyK when dealing with f's type
645 signature.  But we don't expect this to happen because we can't get a
646 lexically scoped type variable with a mutable kind variable in it.  A
647 delicate point, this.  If it becomes an issue we might need to
648 distinguish top-level from nested uses.
649
650 Moreover
651   * it cannot fail, 
652   * it does no unifications
653   * it does no validity checking, except for structural matters, such as
654         (a) spurious ! annotations.
655         (b) a class used as a type
656
657 \begin{code}
658
659 zonkTcKindToKind :: TcKind -> TcM Kind
660 -- When zonking a TcKind to a kind we instantiate kind variables to AnyK
661 zonkTcKindToKind = zonkType (mkZonkTcTyVar (\ _ -> return anyKind) mkTyVarTy)
662
663 dsHsType :: LHsType Name -> TcM Type
664 -- All HsTyVarBndrs in the intput type are kind-annotated
665 -- See Note [Desugaring types]
666 dsHsType ty = ds_type (unLoc ty)
667
668 ds_type :: HsType Name -> TcM Type
669 -- See Note [Desugaring types]
670 ds_type ty@(HsTyVar _)
671   = ds_app ty []
672
673 ds_type (HsParTy ty)            -- Remove the parentheses markers
674   = dsHsType ty
675
676 ds_type ty@(HsBangTy {})    -- No bangs should be here
677   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
678
679 ds_type ty@(HsRecTy {})     -- No bangs should be here
680   = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
681
682 ds_type (HsKindSig ty _)
683   = dsHsType ty -- Kind checking done already
684
685 ds_type (HsListTy ty) = do
686     tau_ty <- dsHsType ty
687     checkWiredInTyCon listTyCon
688     return (mkListTy tau_ty)
689
690 ds_type (HsPArrTy ty) = do
691     tau_ty <- dsHsType ty
692     checkWiredInTyCon parrTyCon
693     return (mkPArrTy tau_ty)
694
695 ds_type (HsTupleTy hs_con tys) = do
696     con <- case hs_con of
697         HsUnboxedTuple    -> return UnboxedTuple
698         HsBoxedTuple      -> return BoxedTuple
699         HsConstraintTuple -> return ConstraintTuple
700         _ -> panic "ds_type HsTupleTy"
701         -- failWithTc (ptext (sLit "Unexpected tuple component kind:") <+> ppr kind')
702     let tycon = tupleTyCon con (length tys)
703     tau_tys <- dsHsTypes tys
704     checkWiredInTyCon tycon
705     return (mkTyConApp tycon tau_tys)
706
707 ds_type (HsFunTy ty1 ty2) = do
708     tau_ty1 <- dsHsType ty1
709     tau_ty2 <- dsHsType ty2
710     return (mkFunTy tau_ty1 tau_ty2)
711
712 ds_type (HsOpTy ty1 (wrap, (L span op)) ty2) =
713     setSrcSpan span (ds_app (HsWrapTy wrap (HsTyVar op)) [ty1,ty2])
714
715 ds_type ty@(HsAppTy _ _)
716   = ds_app ty []
717
718 ds_type (HsIParamTy n ty) = do
719     tau_ty <- dsHsType ty
720     return (mkIPPred n tau_ty)
721
722 ds_type (HsEqTy ty1 ty2) = do
723     tau_ty1 <- dsHsType ty1
724     tau_ty2 <- dsHsType ty2
725     return (mkEqPred (tau_ty1, tau_ty2))
726
727 ds_type (HsForAllTy _ tv_names ctxt ty)
728   = tcTyVarBndrsKindGen tv_names $ \ tyvars -> do
729     theta <- mapM dsHsType (unLoc ctxt)
730     tau <- dsHsType ty
731     return (mkSigmaTy tyvars theta tau)
732
733 ds_type (HsDocTy ty _)  -- Remove the doc comment
734   = dsHsType ty
735
736 ds_type (HsSpliceTy _ _ kind) 
737   = do { kind' <- zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind) mkTyVarTy) 
738                            kind
739                      -- See Note [Kind of a type splice]
740        ; newFlexiTyVarTy kind' }
741
742 ds_type (HsQuasiQuoteTy {}) = panic "ds_type"   -- Eliminated by renamer
743 ds_type (HsCoreTy ty)       = return ty
744
745 ds_type (HsExplicitListTy kind tys) = do
746   kind' <- zonkTcKindToKind kind
747   ds_tys <- mapM dsHsType tys
748   return $
749    foldr (\a b -> mkTyConApp (buildPromotedDataCon consDataCon) [kind', a, b])
750          (mkTyConApp (buildPromotedDataCon nilDataCon) [kind']) ds_tys
751
752 ds_type (HsExplicitTupleTy kis tys) = do
753   MASSERT( length kis == length tys )
754   kis' <- mapM zonkTcKindToKind kis
755   tys' <- mapM dsHsType tys
756   return $ mkTyConApp (buildPromotedDataCon (tupleCon BoxedTuple (length kis'))) (kis' ++ tys')
757
758 ds_type (HsWrapTy (WpKiApps kappas) ty) = do
759   tau <- ds_type ty
760   kappas' <- mapM zonkTcKindToKind kappas
761   return (mkAppTys tau kappas')
762
763 dsHsTypes :: [LHsType Name] -> TcM [Type]
764 dsHsTypes arg_tys = mapM dsHsType arg_tys
765 \end{code}
766
767 Note [Kind of a type splice]
768 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
769 Consider these terms, each with TH type splice inside:
770      [| e1 :: Maybe $(..blah..) |]
771      [| e2 :: $(..blah..) |]
772 When kind-checking the type signature, we'll kind-check the splice
773 $(..blah..); we want to give it a kind that can fit in any context,
774 as if $(..blah..) :: forall k. k.  
775
776 In the e1 example, the context of the splice fixes kappa to *.  But
777 in the e2 example, we'll desugar the type, zonking the kind unification
778 variables as we go.  When we encournter the unconstrained kappa, we
779 want to default it to '*', not to AnyK.
780
781
782 Help functions for type applications
783 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
784
785 \begin{code}
786 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
787 ds_app (HsAppTy ty1 ty2) tys
788   = ds_app (unLoc ty1) (ty2:tys)
789
790 ds_app ty tys = do
791     arg_tys <- dsHsTypes tys
792     case ty of
793         HsTyVar fun -> ds_var_app fun arg_tys
794         _           -> do fun_ty <- ds_type ty
795                           return (mkAppTys fun_ty arg_tys)
796
797 ds_var_app :: Name -> [Type] -> TcM Type
798 -- See Note [Type checking recursive type and class declarations]
799 -- in TcTyClsDecls
800 ds_var_app name arg_tys 
801   | isTvNameSpace (rdrNameSpace (nameRdrName name))
802   = do { thing <- tcLookup name
803        ; case thing of
804            ATyVar _ tv -> return (mkAppTys (mkTyVarTy tv) arg_tys)
805            _           -> wrongThingErr "type" thing name }
806
807   | otherwise
808   = do { thing <- tcLookupGlobal name
809        ; case thing of
810            ATyCon tc   -> return (mkTyConApp tc arg_tys)
811            ADataCon dc -> return (mkTyConApp (buildPromotedDataCon dc) arg_tys) 
812            _           -> wrongThingErr "type" (AGlobal thing) name }
813
814 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
815         -- Wrap a context around only if we want to show that contexts.  
816         -- Omit invisble ones and ones user's won't grok
817 addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing
818
819 typeCtxt :: HsType Name -> SDoc
820 typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
821 \end{code}
822
823 %************************************************************************
824 %*                                                                      *
825                 Type-variable binders
826 %*                                                                      *
827 %************************************************************************
828
829 Note [Kind-checking kind-polymorphic types]
830 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
831 Consider:
832   f :: forall (f::k -> *) a. f a -> Int
833
834 Here, the [LHsTyVarBndr Name] of the forall type will be [f,a], where
835   a is a  UserTyVar   -> type variable without kind annotation
836   f is a  KindedTyVar -> type variable with kind annotation
837
838 If were were to allow binding sites for kind variables, thus
839   f :: forall @k (f :: k -> *) a. f a -> Int
840 then we'd also need
841   k is a   UserKiVar   -> kind variable (they don't need annotation,
842                           since we only have BOX for a super kind)
843
844 \begin{code}
845 kcHsTyVars :: [LHsTyVarBndr Name] 
846            -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
847                                                 -- They scope over the thing inside
848            -> TcM r
849 kcHsTyVars tvs thing_inside
850   = do { kinded_tvs <- mapM (wrapLocM kcHsTyVar) tvs
851        ; tcExtendKindEnvTvs kinded_tvs thing_inside }
852
853 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
854 -- Return a *kind-annotated* binder, whose PostTcKind is
855 -- initialised with a kind variable.
856 -- Typically the Kind inside the KindedTyVar will be a tyvar with a mutable kind 
857 -- in it. We aren't yet sure whether the binder is a *type* variable or a *kind*
858 -- variable. See Note [Kind-checking kind-polymorphic types]
859 --
860 -- If the variable is already in scope return it, instead of introducing a new
861 -- one. This can occur in 
862 --   instance C (a,b) where
863 --     type F (a,b) c = ...
864 -- Here a,b will be in scope when processing the associated type instance for F.
865 kcHsTyVar tyvar = do in_scope <- getInLocalScope
866                      if in_scope (hsTyVarName tyvar)
867                       then do inscope_tyvar <- tcLookupTyVar (hsTyVarName tyvar)
868                               return (UserTyVar (tyVarName inscope_tyvar)
869                                 (tyVarKind inscope_tyvar)) 
870                        else kcHsTyVar' tyvar
871     where
872         kcHsTyVar' (UserTyVar name _)        = UserTyVar name <$> newMetaKindVar
873         kcHsTyVar' (KindedTyVar name kind _) = do
874           kind' <- scDsLHsKind kind
875           return (KindedTyVar name kind kind')
876
877 ------------------
878 tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
879              -> ([TyVar] -> TcM r)
880              -> TcM r
881 -- Used when type-checking types/classes/type-decls
882 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
883 -- Fix #5426: avoid abstraction over kinds containing # or (#)
884 tcTyVarBndrs bndrs thing_inside = do
885     tyvars <- mapM (zonk . hsTyVarNameKind . unLoc) bndrs
886     tcExtendTyVarEnv tyvars (thing_inside tyvars)
887   where
888     zonk (name, kind)
889       = do { kind' <- zonkTcKind kind
890            ; return (mkTyVar name kind') }
891
892 tcTyVarBndrsKindGen :: [LHsTyVarBndr Name] -> ([TyVar] -> TcM r) -> TcM r
893 -- tcTyVarBndrsKindGen [(f :: ?k -> *), (a :: ?k)] thing_inside
894 -- calls thing_inside with [(k :: BOX), (f :: k -> *), (a :: k)]
895 tcTyVarBndrsKindGen bndrs thing_inside
896   = do { let kinds = map (hsTyVarKind . unLoc) bndrs
897        ; (kvs, zonked_kinds) <- kindGeneralizeKinds kinds
898        ; let tyvars = zipWith mkTyVar (map hsLTyVarName bndrs) zonked_kinds
899              ktvs = kvs ++ tyvars     -- See Note [Kinds of quantified type variables]
900        ; traceTc "tcTyVarBndrsKindGen" (ppr (bndrs, kvs, tyvars))
901        ; tcExtendTyVarEnv ktvs (thing_inside ktvs) }
902 \end{code}
903
904 Note [Kinds of quantified type variables]
905 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
906 tcTyVarBndrsKindGen quantifies over a specified list of type variables,
907 *and* over the kind variables mentioned in the kinds of those tyvars.
908
909 Note that we must zonk those kinds (obviously) but less obviously, we
910 must return type variables whose kinds are zonked too. Example
911     (a :: k7)  where  k7 := k9 -> k9
912 We must return
913     [k9, a:k9->k9]
914 and NOT 
915     [k9, a:k7]
916 Reason: we're going to turn this into a for-all type, 
917    forall k9. forall (a:k7). blah
918 which the type checker will then instantiate, and instantiate does not
919 look through unification variables!  
920
921 Hence using zonked_kinds when forming 'tyvars'.
922
923 \begin{code}
924 tcTyClTyVars :: Name -> [LHsTyVarBndr Name]     -- LHS of the type or class decl
925              -> ([TyVar] -> Kind -> TcM a) -> TcM a
926 -- (tcTyClTyVars T [a,b] thing_inside) 
927 --   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
928 --   calls thing_inside with arguments
929 --      [k1,k2,a,b] (k2 -> *)  
930 --
931 -- No need to freshen the k's because they are just skolem 
932 -- constants here, and we are at top level anyway.
933 tcTyClTyVars tycon tyvars thing_inside
934   = do { thing <- tcLookup tycon
935        ; let { kind =
936                  case thing of
937                    AThing kind -> kind
938                    _ -> panic "tcTyClTyVars"
939                      -- We only call tcTyClTyVars during typechecking in
940                      -- TcTyClDecls, where the local env is extended with
941                      -- the generalized_env (mapping Names to AThings).
942              ; (kvs, body) = splitForAllTys kind
943              ; (kinds, res) = splitKindFunTysN (length names) body
944              ; names = hsLTyVarNames tyvars
945              ; tvs = zipWith mkTyVar names kinds
946              ; all_vs = kvs ++ tvs }
947        ; tcExtendTyVarEnv all_vs (thing_inside all_vs res) }
948
949 -- Used when generalizing binders and type family patterns
950 -- It takes a kind from the type checker (like `k0 -> *`), and returns the 
951 -- final, kind-generalized kind (`forall k::BOX. k -> *`)
952 kindGeneralizeKinds :: [TcKind] -> TcM ([KindVar], [Kind])
953 -- INVARIANT: the returned kinds are zonked, and
954 --            mention the returned kind variables
955 kindGeneralizeKinds kinds 
956   = do { -- Quantify over kind variables free in
957          -- the kinds, and *not* in the environment
958        ; traceTc "kindGeneralizeKinds 1" (ppr kinds)
959        ; zonked_kinds <- mapM zonkTcKind kinds
960        ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
961        ; tidy_env <- tcInitTidyEnv
962        ; let kvs_to_quantify = varSetElems (tyVarsOfTypes zonked_kinds
963                                             `minusVarSet` gbl_tvs)
964
965              (_, tidy_kvs_to_quantify) = tidyTyVarBndrs tidy_env kvs_to_quantify
966                            -- We do not get a later chance to tidy!
967
968        ; kvs <- ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify)
969                 zonkQuantifiedTyVars tidy_kvs_to_quantify
970
971          -- Zonk the kinds again, to pick up either the kind 
972          -- variables we quantify over, or *, depending on whether
973          -- zonkQuantifiedTyVars decided to generalise (which in
974          -- turn depends on PolyKinds)
975        ; final_kinds <- mapM zonkTcKind zonked_kinds
976
977        ; traceTc "kindGeneralizeKinds 2" (vcat [ ppr gbl_tvs, ppr kinds, ppr kvs_to_quantify
978                                         , ppr kvs, ppr final_kinds ])
979        ; return (kvs, final_kinds) }
980
981 kindGeneralizeKind :: TcKind -> TcM ( [KindVar]  -- these were flexi kind vars
982                                     , Kind )     -- this is the old kind where flexis got zonked
983 kindGeneralizeKind kind = do
984   (kvs, [kind']) <- kindGeneralizeKinds [kind]
985   return (kvs, kind')
986
987 -----------------------------------
988 tcDataKindSig :: Kind -> TcM [TyVar]
989 -- GADT decls can have a (perhaps partial) kind signature
990 --      e.g.  data T :: * -> * -> * where ...
991 -- This function makes up suitable (kinded) type variables for 
992 -- the argument kinds, and checks that the result kind is indeed *.
993 -- We use it also to make up argument type variables for for data instances.
994 tcDataKindSig kind
995   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
996         ; span <- getSrcSpanM
997         ; us   <- newUniqueSupply 
998         ; let uniqs = uniqsFromSupply us
999         ; return [ mk_tv span uniq str kind 
1000                  | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
1001   where
1002     (arg_kinds, res_kind) = splitKindFunTys kind
1003     mk_tv loc uniq str kind = mkTyVar name kind
1004         where
1005            name = mkInternalName uniq occ loc
1006            occ  = mkOccName tvName str
1007           
1008     dnames = map ('$' :) names  -- Note [Avoid name clashes for associated data types]
1009
1010     names :: [String]
1011     names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 
1012
1013 badKindSig :: Kind -> SDoc
1014 badKindSig kind 
1015  = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
1016         2 (ppr kind)
1017 \end{code}
1018
1019 Note [Avoid name clashes for associated data types]
1020 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1021 Consider    class C a b where
1022                data D b :: * -> *
1023 When typechecking the decl for D, we'll invent an extra type variable for D,
1024 to fill out its kind.  We *don't* want this type variable to be 'a', because
1025 in an .hi file we'd get
1026             class C a b where
1027                data D b a 
1028 which makes it look as if there are *two* type indices.  But there aren't!
1029 So we use $a instead, which cannot clash with a user-written type variable.
1030 Remember that type variable binders in interface files are just FastStrings,
1031 not proper Names.
1032
1033 (The tidying phase can't help here because we don't tidy TyCons.  Another
1034 alternative would be to record the number of indexing parameters in the 
1035 interface file.)
1036
1037
1038 %************************************************************************
1039 %*                                                                      *
1040                 Scoped type variables
1041 %*                                                                      *
1042 %************************************************************************
1043
1044
1045 tcAddScopedTyVars is used for scoped type variables added by pattern
1046 type signatures
1047         e.g.  \ ((x::a), (y::a)) -> x+y
1048 They never have explicit kinds (because this is source-code only)
1049 They are mutable (because they can get bound to a more specific type).
1050
1051 Usually we kind-infer and expand type splices, and then
1052 tupecheck/desugar the type.  That doesn't work well for scoped type
1053 variables, because they scope left-right in patterns.  (e.g. in the
1054 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
1055
1056 The current not-very-good plan is to
1057   * find all the types in the patterns
1058   * find their free tyvars
1059   * do kind inference
1060   * bring the kinded type vars into scope
1061   * BUT throw away the kind-checked type
1062         (we'll kind-check it again when we type-check the pattern)
1063
1064 This is bad because throwing away the kind checked type throws away
1065 its splices.  But too bad for now.  [July 03]
1066
1067 Historical note:
1068     We no longer specify that these type variables must be univerally 
1069     quantified (lots of email on the subject).  If you want to put that 
1070     back in, you need to
1071         a) Do a checkSigTyVars after thing_inside
1072         b) More insidiously, don't pass in expected_ty, else
1073            we unify with it too early and checkSigTyVars barfs
1074            Instead you have to pass in a fresh ty var, and unify
1075            it with expected_ty afterwards
1076
1077 \begin{code}
1078 tcHsPatSigType :: UserTypeCtxt
1079                -> LHsType Name          -- The type signature
1080                -> TcM ([TyVar],         -- Newly in-scope type variables
1081                         Type)           -- The signature
1082 -- Used for type-checking type signatures in
1083 -- (a) patterns           e.g  f (x::Int) = e
1084 -- (b) result signatures  e.g. g x :: Int = e
1085 -- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
1086
1087 tcHsPatSigType ctxt hs_ty 
1088   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
1089     do  {       -- Find the type variables that are mentioned in the type
1090                 -- but not already in scope.  These are the ones that
1091                 -- should be bound by the pattern signature
1092           in_scope <- getInLocalScope
1093         ; let span = getLoc hs_ty
1094               sig_tvs = userHsTyVarBndrs $ map (L span) $ 
1095                         filterOut in_scope $
1096                         nameSetToList (extractHsTyVars hs_ty)
1097
1098         ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
1099         ; checkValidType ctxt sig_ty 
1100         ; return (tyvars, sig_ty)
1101       }
1102
1103 tcPatSig :: UserTypeCtxt
1104          -> LHsType Name
1105          -> TcSigmaType
1106          -> TcM (TcType,            -- The type to use for "inside" the signature
1107                  [(Name, TcTyVar)], -- The new bit of type environment, binding
1108                                     -- the scoped type variables
1109                  HsWrapper)         -- Coercion due to unification with actual ty
1110                                     -- Of shape:  res_ty ~ sig_ty
1111 tcPatSig ctxt sig res_ty
1112   = do  { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
1113         -- sig_tvs are the type variables free in 'sig', 
1114         -- and not already in scope. These are the ones
1115         -- that should be brought into scope
1116
1117         ; if null sig_tvs then do {
1118                 -- Just do the subsumption check and return
1119                   wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
1120                 ; return (sig_ty, [], wrap)
1121         } else do {
1122                 -- Type signature binds at least one scoped type variable
1123         
1124                 -- A pattern binding cannot bind scoped type variables
1125                 -- The renamer fails with a name-out-of-scope error 
1126                 -- if a pattern binding tries to bind a type variable,
1127                 -- So we just have an ASSERT here
1128         ; let in_pat_bind = case ctxt of
1129                                 BindPatSigCtxt -> True
1130                                 _              -> False
1131         ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
1132
1133                 -- Check that all newly-in-scope tyvars are in fact
1134                 -- constrained by the pattern.  This catches tiresome
1135                 -- cases like   
1136                 --      type T a = Int
1137                 --      f :: Int -> Int
1138                 --      f (x :: T a) = ...
1139                 -- Here 'a' doesn't get a binding.  Sigh
1140         ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
1141         ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
1142
1143         -- Now do a subsumption check of the pattern signature against res_ty
1144         ; sig_tvs' <- tcInstSigTyVars sig_tvs
1145         ; let sig_ty' = substTyWith sig_tvs (mkTyVarTys sig_tvs') sig_ty
1146         ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty'
1147
1148         -- Check that each is bound to a distinct type variable,
1149         -- and one that is not already in scope
1150         ; binds_in_scope <- getScopedTyVarBinds
1151         ; let tv_binds :: [(Name,TcTyVar)]
1152               tv_binds = map tyVarName sig_tvs `zip` sig_tvs'
1153         ; check binds_in_scope tv_binds
1154         
1155         -- Phew!
1156         ; return (sig_ty', tv_binds, wrap)
1157         } }
1158   where
1159     check :: [(Name,TcTyVar)] -> [(Name, TcTyVar)] -> TcM ()
1160     check _        []            = return ()
1161     check in_scope ((n,tv):rest) = do { check_one in_scope n tv
1162                                       ; check ((n,tv):in_scope) rest }
1163
1164     check_one :: [(Name,TcTyVar)] -> Name -> TcTyVar -> TcM ()
1165     check_one in_scope n tv
1166         = checkTc (null dups) (dupInScope n (head dups) tv)
1167                 -- Must not bind to the same type variable
1168                 -- as some other in-scope type variable
1169         where
1170           dups = [n' | (n',tv') <- in_scope, tv' == tv]
1171 \end{code}
1172
1173
1174 %************************************************************************
1175 %*                                                                      *
1176         Checking kinds
1177 %*                                                                      *
1178 %************************************************************************
1179
1180 We would like to get a decent error message from
1181   (a) Under-applied type constructors
1182              f :: (Maybe, Maybe)
1183   (b) Over-applied type constructors
1184              f :: Int x -> Int x
1185
1186 \begin{code}
1187 -- The ExpKind datatype means "expected kind" and contains 
1188 -- some info about just why that kind is expected, to improve
1189 -- the error message on a mis-match
1190 data ExpKind = EK TcKind SDoc
1191
1192 instance Outputable ExpKind where
1193   ppr (EK k _) = ptext (sLit "Expected kind:") <+> ppr k
1194
1195 ekLifted, ekArg, ekConstraint :: ExpKind
1196 ekLifted     = EK liftedTypeKind (ptext (sLit "Expected"))
1197 ekArg        = EK argTypeKind    (ptext (sLit "Expected"))
1198 ekConstraint = EK constraintKind (ptext (sLit "Expected"))
1199
1200 -- Build an ExpKind for arguments
1201 expArgKind :: SDoc -> TcKind -> Int -> ExpKind
1202 expArgKind exp kind arg_no = EK kind (ptext (sLit "The") <+> speakNth arg_no 
1203                                   <+> ptext (sLit "argument of") <+> exp
1204                                   <+> ptext (sLit "should have"))
1205
1206 unifyKinds :: SDoc -> [(LHsType Name, TcKind)] -> TcM TcKind
1207 unifyKinds fun act_kinds = do
1208   kind <- newMetaKindVar
1209   let checkArgs (arg_no, (ty, act_kind)) = 
1210         checkExpectedKind ty act_kind (expArgKind (quotes fun) kind arg_no)
1211   mapM_ checkArgs (zip [1..] act_kinds)
1212   return kind
1213
1214 checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
1215 -- A fancy wrapper for 'unifyKind', which tries
1216 -- to give decent error messages.
1217 --      (checkExpectedKind ty act_kind exp_kind)
1218 -- checks that the actual kind act_kind is compatible
1219 --      with the expected kind exp_kind
1220 -- The first argument, ty, is used only in the error message generation
1221 checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt) = do
1222     traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr ek)
1223     (_errs, mb_r) <- tryTc (unifyKind act_kind exp_kind)
1224     case mb_r of
1225         Just _  -> return ()  -- Unification succeeded
1226         Nothing -> do
1227
1228         -- So there's definitely an error
1229         -- Now to find out what sort
1230            exp_kind <- zonkTcKind exp_kind
1231            act_kind <- zonkTcKind act_kind
1232
1233            env0 <- tcInitTidyEnv
1234            let (exp_as, _) = splitKindFunTys exp_kind
1235                (act_as, _) = splitKindFunTys act_kind
1236                n_exp_as  = length exp_as
1237                n_act_as  = length act_as
1238                n_diff_as = n_act_as - n_exp_as
1239
1240                (env1, tidy_exp_kind) = tidyOpenKind env0 exp_kind
1241                (env2, tidy_act_kind) = tidyOpenKind env1 act_kind
1242
1243                err | n_exp_as < n_act_as     -- E.g. [Maybe]
1244                    = ptext (sLit "Expecting") <+>
1245                      speakN n_diff_as <+> ptext (sLit "more argument") <>
1246                      (if n_diff_as > 1 then char 's' else empty) <+>
1247                      ptext (sLit "to") <+> quotes (ppr ty)
1248
1249                      -- Now n_exp_as >= n_act_as. In the next two cases,
1250                      -- n_exp_as == 0, and hence so is n_act_as
1251                    | isConstraintKind tidy_act_kind
1252                    = text "Predicate" <+> quotes (ppr ty) <+> text "used as a type"
1253                    
1254                    | isConstraintKind tidy_exp_kind
1255                    = text "Type of kind" <+> ppr tidy_act_kind <+> text "used as a constraint"
1256                    
1257                    | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1258                    = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
1259                        <+> ptext (sLit "is unlifted")
1260
1261                    | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1262                    = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
1263                        <+> ptext (sLit "is lifted")
1264
1265                    | otherwise               -- E.g. Monad [Int]
1266                    = ptext (sLit "Kind mis-match") $$ more_info
1267
1268                more_info = sep [ ek_ctxt <+> ptext (sLit "kind") 
1269                                     <+> quotes (pprKind tidy_exp_kind) <> comma,
1270                                  ptext (sLit "but") <+> quotes (ppr ty) <+>
1271                                      ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
1272
1273            failWithTcM (env2, err)
1274 \end{code}
1275
1276 %************************************************************************
1277 %*                                                                      *
1278         Sort checking kinds
1279 %*                                                                      *
1280 %************************************************************************
1281
1282 scDsLHsKind converts a user-written kind to an internal, sort-checked kind.
1283 It does sort checking and desugaring at the same time, in one single pass.
1284 It fails when the kinds are not well-formed (eg. data A :: * Int), or if there
1285 are non-promotable or non-fully applied kinds.
1286
1287 \begin{code}
1288 scDsLHsKind :: LHsKind Name -> TcM Kind
1289 scDsLHsKind k = addErrCtxt (ptext (sLit "In the kind") <+> quotes (ppr k)) $
1290                   sc_ds_lhs_kind k
1291
1292 scDsLHsMaybeKind :: Maybe (LHsKind Name) -> TcM (Maybe Kind)
1293 scDsLHsMaybeKind Nothing  = return Nothing
1294 scDsLHsMaybeKind (Just k) = do k' <- scDsLHsKind k
1295                                return (Just k')
1296
1297 sc_ds_lhs_kind :: LHsKind Name -> TcM Kind
1298 sc_ds_lhs_kind (L span ki) = setSrcSpan span (sc_ds_hs_kind ki)
1299
1300 -- The main worker
1301 sc_ds_hs_kind :: HsKind Name -> TcM Kind
1302 sc_ds_hs_kind k@(HsTyVar _)   = sc_ds_app k []
1303 sc_ds_hs_kind k@(HsAppTy _ _) = sc_ds_app k []
1304
1305 sc_ds_hs_kind (HsParTy ki) = sc_ds_lhs_kind ki
1306
1307 sc_ds_hs_kind (HsFunTy ki1 ki2) =
1308   do kappa_ki1 <- sc_ds_lhs_kind ki1
1309      kappa_ki2 <- sc_ds_lhs_kind ki2
1310      return (mkArrowKind kappa_ki1 kappa_ki2)
1311
1312 sc_ds_hs_kind (HsListTy ki) =
1313   do kappa <- sc_ds_lhs_kind ki
1314      checkWiredInTyCon listTyCon
1315      return $ mkPromotedListTy kappa
1316
1317 sc_ds_hs_kind (HsTupleTy _ kis) =
1318   do kappas <- mapM sc_ds_lhs_kind kis
1319      checkWiredInTyCon tycon
1320      return $ mkTyConApp tycon kappas
1321   where 
1322      tycon = promotedTupleTyCon BoxedTuple (length kis)
1323
1324 -- Argument not kind-shaped
1325 sc_ds_hs_kind k = panic ("sc_ds_hs_kind: " ++ showPpr k)
1326
1327 -- Special case for kind application
1328 sc_ds_app :: HsKind Name -> [LHsKind Name] -> TcM Kind
1329 sc_ds_app (HsAppTy ki1 ki2) kis = sc_ds_app (unLoc ki1) (ki2:kis)
1330 sc_ds_app (HsTyVar tc)      kis =
1331   do arg_kis <- mapM sc_ds_lhs_kind kis
1332      sc_ds_var_app tc arg_kis
1333 sc_ds_app ki                _   = failWithTc (quotes (ppr ki) <+> 
1334                                     ptext (sLit "is not a kind constructor"))
1335
1336 -- IA0_TODO: With explicit kind polymorphism I might need to add ATyVar
1337 sc_ds_var_app :: Name -> [Kind] -> TcM Kind
1338 -- Special case for * and Constraint kinds
1339 -- They are kinds already, so we don't need to promote them
1340 sc_ds_var_app name arg_kis
1341   |  name == liftedTypeKindTyConName
1342   || name == constraintKindTyConName
1343   = do { unless (null arg_kis)
1344            (failWithTc (text "Kind" <+> ppr name <+> text "cannot be applied"))
1345        ; thing <- tcLookup name
1346        ; case thing of
1347            AGlobal (ATyCon tc) -> return (mkTyConApp tc [])
1348            _                   -> panic "sc_ds_var_app 1" }
1349
1350 -- General case
1351 sc_ds_var_app name arg_kis = do
1352   (_errs, mb_thing) <- tryTc (tcLookup name)
1353   case mb_thing of
1354     Just (AGlobal (ATyCon tc))
1355       | isAlgTyCon tc || isTupleTyCon tc -> do
1356       data_kinds <- xoptM Opt_DataKinds
1357       unless data_kinds $ addErr (dataKindsErr name)
1358       case isPromotableTyCon tc of
1359         Just n | n == length arg_kis ->
1360           return (mkTyConApp (buildPromotedTyCon tc) arg_kis)
1361         Just _  -> err tc "is not fully applied"
1362         Nothing -> err tc "is not promotable"
1363
1364     -- It is in scope, but not what we expected
1365     Just thing -> wrongThingErr "promoted type" thing name
1366
1367     -- It is not in scope, but it passed the renamer: staging error
1368     Nothing    -> ASSERT2 ( isTyConName name, ppr name )
1369                   failWithTc (ptext (sLit "Promoted kind") <+> 
1370                               quotes (ppr name) <+>
1371                               ptext (sLit "used in a mutually recursive group"))
1372   where 
1373    err tc msg = failWithTc (quotes (ppr tc) <+> ptext (sLit "of kind")
1374                         <+> quotes (ppr (tyConKind tc)) <+> ptext (sLit msg))
1375
1376 \end{code}
1377
1378 %************************************************************************
1379 %*                                                                      *
1380                 Scoped type variables
1381 %*                                                                      *
1382 %************************************************************************
1383
1384 \begin{code}
1385 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
1386 pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon, 
1387                                  nest 2 (pp_sig ctxt) ]
1388   where
1389     pp_sig (FunSigCtxt n)  = pp_n_colon n
1390     pp_sig (ConArgCtxt n)  = pp_n_colon n
1391     pp_sig (ForSigCtxt n)  = pp_n_colon n
1392     pp_sig _               = ppr (unLoc hs_ty)
1393
1394     pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
1395
1396 badPatSigTvs :: TcType -> [TyVar] -> SDoc
1397 badPatSigTvs sig_ty bad_tvs
1398   = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, 
1399                  quotes (pprWithCommas ppr bad_tvs), 
1400                  ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
1401                  ptext (sLit "but are actually discarded by a type synonym") ]
1402          , ptext (sLit "To fix this, expand the type synonym") 
1403          , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
1404
1405 dupInScope :: Name -> Name -> TcTyVar -> SDoc
1406 dupInScope n n' _
1407   = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
1408        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
1409                 ptext (sLit "Distinct scoped type variables must be distinct")])
1410 \end{code}
1411