TcHsType.hs 67.6 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

5
\section[TcMonoType]{Typechecking user-specified @MonoTypes@}
Austin Seipp's avatar
Austin Seipp committed
6
-}
7

8
{-# LANGUAGE CPP #-}
Ian Lynagh's avatar
Ian Lynagh committed
9

10
module TcHsType (
11
        tcHsSigType, tcHsDeriv, tcHsVectInst,
12 13
        tcHsInstHead,
        UserTypeCtxt(..),
14

15
                -- Type checking type and class decls
16 17
        kcLookupKind, kcTyClTyVars, tcTyClTyVars,
        tcHsConArgType, tcDataKindSig,
18
        tcClassSigType,
dreixel's avatar
dreixel committed
19

20
                -- Kind-checking types
21
                -- No kind generalisation, no checkValidType
22
        kcHsTyVarBndrs, tcHsTyVarBndrs,
23
        tcHsLiftedType, tcHsOpenType,
24
        tcLHsType, tcCheckLHsType, tcCheckLHsTypeAndGen,
25
        tcHsContext, tcInferApps, tcHsArgTys,
batterseapower's avatar
batterseapower committed
26

27
        kindGeneralize, checkKind,
28

29 30
                -- Sort-checking kinds
        tcLHsKind,
31

32 33
                -- Pattern type signatures
        tcHsPatSigType, tcPatSig
34 35 36 37
   ) where

#include "HsVersions.h"

38
import HsSyn
39
import TcRnMonad
40
import TcEvidence( HsWrapper )
41 42
import TcEnv
import TcMType
43
import TcValidity
44 45 46
import TcUnify
import TcIface
import TcType
47
import Type
48
import TypeRep( Type(..) )  -- For the mkNakedXXX stuff
dreixel's avatar
dreixel committed
49
import Kind
50
import RdrName( lookupLocalRdrOcc )
51
import Var
52
import VarSet
53
import TyCon
cactus's avatar
cactus committed
54
import ConLike
55
import DataCon
dreixel's avatar
dreixel committed
56
import TysPrim ( liftedTypeKindTyConName, constraintKindTyConName )
57 58
import Class
import Name
59
import NameEnv
60 61 62
import TysWiredIn
import BasicTypes
import SrcLoc
63
import DynFlags ( ExtensionFlag( Opt_DataKinds ), getDynFlags )
64 65
import Constants ( mAX_CTUPLE_SIZE )
import ErrUtils( MsgDoc )
66
import Unique
67
import UniqSupply
68
import Outputable
69
import FastString
70 71
import Util

72
import Data.Maybe( isNothing )
73
import Control.Monad ( unless, when, zipWithM )
74
import PrelNames( ipClassName, funTyConKey, allNameStrings )
75

Austin Seipp's avatar
Austin Seipp committed
76
{-
77 78 79
        ----------------------------
                General notes
        ----------------------------
80 81 82 83

Generally speaking we now type-check types in three phases

  1.  kcHsType: kind check the HsType
84 85
        *includes* performing any TH type splices;
        so it returns a translated, and kind-annotated, type
86 87

  2.  dsHsType: convert from HsType to Type:
88 89 90
        perform zonking
        expand type synonyms [mkGenTyApps]
        hoist the foralls [tcHsType]
91 92 93 94 95

  3.  checkValidType: check the validity of the resulting type

Often these steps are done one after the other (tcHsSigType).
But in mutually recursive groups of type and class decls we do
96 97 98
        1 kind-check the whole group
        2 build TyCons/Classes in a knot-tied way
        3 check the validity of types in the now-unknotted TyCons/Classes
99 100

For example, when we find
101
        (forall a m. m a -> m a)
102 103 104 105 106 107 108
we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
an environment that binds a and m suitably.

The kind checker passed to tcHsTyVars needs to look at enough to
establish the kind of the tyvar:
  * For a group of type and class decls, it's just the group, not
109
        the rest of the program
110
  * For a tyvar bound in a pattern type signature, its the types
111
        mentioned in the other type signatures in that bunch of patterns
112
  * For a tyvar bound in a RULE, it's the type signatures on other
113
        universally quantified variables in the rule
114 115 116

Note that this may occasionally give surprising results.  For example:

117
        data T a b = MkT (a b)
118

119 120
Here we deduce                  a::*->*,       b::*
But equally valid would be      a::(*->*)-> *, b::*->*
121 122 123 124


Validity checking
~~~~~~~~~~~~~~~~~
125
Some of the validity check could in principle be done by the kind checker,
126 127 128 129
but not all:

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
130 131
  e.g.  type T k = k Int
        type S a = a
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
  Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
  and then S is saturated.  This is a GHC extension.

- Similarly, also a GHC extension, we look through synonyms before complaining
  about the form of a class or instance declaration

- Ambiguity checks involve functional dependencies, and it's easier to wait
  until knots have been resolved before poking into them

Also, in a mutually recursive group of types, we can't look at the TyCon until we've
finished building the loop.  So to keep things simple, we postpone most validity
checking until step (3).

Knot tying
~~~~~~~~~~
During step (1) we might fault in a TyCon defined in another module, and it might
(via a loop) refer back to a TyCon defined in this module. So when we tie a big
knot around type declarations with ARecThing, so that the fault-in code can get
the TyCon being defined.


Austin Seipp's avatar
Austin Seipp committed
153 154
************************************************************************
*                                                                      *
155
              Check types AND do validity checking
Austin Seipp's avatar
Austin Seipp committed
156 157 158
*                                                                      *
************************************************************************
-}
159

160
tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
161
  -- NB: it's important that the foralls that come from the top-level
162
  --     HsForAllTy in hs_ty occur *first* in the returned type.
163
  --     See Note [Scoped] with TcSigInfo
164 165 166
tcHsSigType ctxt (L loc hs_ty)
  = setSrcSpan loc $
    addErrCtxt (pprSigCtxt ctxt empty (ppr hs_ty)) $
167 168 169
    do  { kind <- case expectedKindInCtxt ctxt of
                    Nothing -> newMetaKindVar
                    Just k  -> return k
170 171
          -- The kind is checked by checkValidType, and isn't necessarily
          -- of kind * in a Template Haskell quote eg [t| Maybe |]
172

173
          -- Generalise here: see Note [Kind generalisation]
174
        ; ty <- tcCheckHsTypeAndGen hs_ty kind
dreixel's avatar
dreixel committed
175

176
          -- Zonk to expose kind information to checkValidType
177
        ; ty <- zonkSigType ty
178 179
        ; checkValidType ctxt ty
        ; return ty }
dreixel's avatar
dreixel committed
180

181
-----------------
dreixel's avatar
dreixel committed
182
tcHsInstHead :: UserTypeCtxt -> LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
183
-- Like tcHsSigType, but for an instance head.
184
tcHsInstHead user_ctxt lhs_ty@(L loc hs_ty)
185
  = setSrcSpan loc $    -- The "In the type..." context comes from the caller
186
    do { inst_ty <- tc_inst_head hs_ty
187
       ; kvs     <- zonkTcTypeAndFV inst_ty
188
       ; kvs     <- kindGeneralize kvs
189
       ; inst_ty <- zonkSigType (mkForAllTys kvs inst_ty)
190 191 192
       ; checkValidInstance user_ctxt lhs_ty inst_ty }

tc_inst_head :: HsType Name -> TcM TcType
thomasw's avatar
thomasw committed
193
tc_inst_head (HsForAllTy _ _ hs_tvs hs_ctxt hs_ty)
194
  = tcHsTyVarBndrs hs_tvs $ \ tvs ->
195 196 197 198 199 200
    do { ctxt <- tcHsContext hs_ctxt
       ; ty   <- tc_lhs_type hs_ty ekConstraint    -- Body for forall has kind Constraint
       ; return (mkSigmaTy tvs ctxt ty) }

tc_inst_head hs_ty
  = tc_hs_type hs_ty ekConstraint
batterseapower's avatar
batterseapower committed
201

202
-----------------
203
tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type], Kind)
204
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
205 206 207 208 209 210 211 212 213 214 215
-- Returns the C, [ty1, ty2, and the kind of C's *next* argument
-- E.g.    class C (a::*) (b::k->k)
--         data T a b = ... deriving( C Int )
--    returns ([k], C, [k, Int],  k->k)
-- Also checks that (C ty1 ty2 arg) :: Constraint
-- if arg has a suitable kind
tcHsDeriv hs_ty
  = do { arg_kind <- newMetaKindVar
       ; ty <- tcCheckHsTypeAndGen hs_ty (mkArrowKind arg_kind constraintKind)
       ; ty       <- zonkSigType ty
       ; arg_kind <- zonkSigType arg_kind
216 217
       ; let (tvs, pred) = splitForAllTys ty
       ; case getClassPredTys_maybe pred of
218
           Just (cls, tys) -> return (tvs, cls, tys, arg_kind)
219
           Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) }
220 221 222 223 224 225

-- Used for 'VECTORISE [SCALAR] instance' declarations
--
tcHsVectInst :: LHsType Name -> TcM (Class, [Type])
tcHsVectInst ty
  | Just (L _ cls_name, tys) <- splitLHsClassTy_maybe ty
226 227 228
  = do { (cls, cls_kind) <- tcClass cls_name
       ; (arg_tys, _res_kind) <- tcInferApps cls_name cls_kind tys
       ; return (cls, arg_tys) }
229 230
  | otherwise
  = failWithTc $ ptext (sLit "Malformed instance type")
231

Austin Seipp's avatar
Austin Seipp committed
232
{-
233 234 235
        These functions are used during knot-tying in
        type and class declarations, when we have to
        separate kind-checking, desugaring, and validity checking
236 237


Austin Seipp's avatar
Austin Seipp committed
238 239
************************************************************************
*                                                                      *
240
            The main kind checker: no validity checks here
Austin Seipp's avatar
Austin Seipp committed
241 242
*                                                                      *
************************************************************************
243 244

        First a couple of simple wrappers for kcHsType
Austin Seipp's avatar
Austin Seipp committed
245
-}
246

247
tcClassSigType :: LHsType Name -> TcM Type
248 249
tcClassSigType lhs_ty
  = do { ty <- tcCheckLHsTypeAndGen lhs_ty liftedTypeKind
250
       ; zonkSigType ty }
251 252 253 254 255 256 257

tcHsConArgType :: NewOrData ->  LHsType Name -> TcM Type
-- Permit a bang, but discard it
tcHsConArgType NewType  bty = tcHsLiftedType (getBangType bty)
  -- Newtypes can't have bangs, but we don't check that
  -- until checkValidDataCon, so do not want to crash here

258
tcHsConArgType DataType bty = tcHsOpenType (getBangType bty)
259 260 261 262
  -- Can't allow an unlifted type for newtypes, because we're effectively
  -- going to remove the constructor while coercing it to a lifted type.
  -- And newtypes can't be bang'd

263
---------------------------
264 265 266 267 268 269 270 271 272 273 274
tcHsArgTys :: SDoc -> [LHsType Name] -> [Kind] -> TcM [TcType]
tcHsArgTys what tys kinds
  = sequence [ addTypeCtxt ty $
               tc_lhs_type ty (expArgKind what kind n)
             | (ty,kind,n) <- zip3 tys kinds [1..] ]

tc_hs_arg_tys :: SDoc -> [LHsType Name] -> [Kind] -> TcM [TcType]
-- Just like tcHsArgTys but without the addTypeCtxt
tc_hs_arg_tys what tys kinds
  = sequence [ tc_lhs_type ty (expArgKind what kind n)
             | (ty,kind,n) <- zip3 tys kinds [1..] ]
275

dreixel's avatar
dreixel committed
276
---------------------------
277
tcHsOpenType, tcHsLiftedType :: LHsType Name -> TcM TcType
278 279
-- Used for type signatures
-- Do not do validity checking
280
tcHsOpenType ty   = addTypeCtxt ty $ tc_lhs_type ty ekOpen
281 282 283 284 285
tcHsLiftedType ty = addTypeCtxt ty $ tc_lhs_type ty ekLifted

-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType Name -> Kind -> TcM Type
tcCheckLHsType hs_ty exp_kind
286
  = addTypeCtxt hs_ty $
287
    tc_lhs_type hs_ty (EK exp_kind expectedKindMsg)
288 289 290 291

tcLHsType :: LHsType Name -> TcM (TcType, TcKind)
-- Called from outside: set the context
tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type ty)
dreixel's avatar
dreixel committed
292

293
---------------------------
294
tcCheckLHsTypeAndGen :: LHsType Name -> Kind -> TcM Type
295 296
-- Typecheck a type signature, and kind-generalise it
-- The result is not necessarily zonked, and has not been checked for validity
297 298 299 300 301 302 303 304 305
tcCheckLHsTypeAndGen lhs_ty kind
  = do { ty  <- tcCheckLHsType lhs_ty kind
       ; kvs <- zonkTcTypeAndFV ty
       ; kvs <- kindGeneralize kvs
       ; return (mkForAllTys kvs ty) }

tcCheckHsTypeAndGen :: HsType Name -> Kind -> TcM Type
-- Input type is HsType, not LHsType; the caller adds the context
-- Otherwise same as tcCheckLHsTypeAndGen
306
tcCheckHsTypeAndGen hs_ty kind
307
  = do { ty  <- tc_hs_type hs_ty (EK kind expectedKindMsg)
308
       ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty)
309
       ; kvs <- zonkTcTypeAndFV ty
310
       ; kvs <- kindGeneralize kvs
311
       ; return (mkForAllTys kvs ty) }
312

Austin Seipp's avatar
Austin Seipp committed
313
{-
314
Like tcExpr, tc_hs_type takes an expected kind which it unifies with
dreixel's avatar
dreixel committed
315
the kind it figures out. When we don't know what kind to expect, we use
316
tc_lhs_type_fresh, to first create a new meta kind variable and use that as
dreixel's avatar
dreixel committed
317
the expected kind.
Austin Seipp's avatar
Austin Seipp committed
318
-}
319

320 321 322
tc_infer_lhs_type :: LHsType Name -> TcM (TcType, TcKind)
tc_infer_lhs_type ty =
  do { kv <- newMetaKindVar
323
     ; r <- tc_lhs_type ty (EK kv expectedKindMsg)
324 325 326 327
     ; return (r, kv) }

tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType
tc_lhs_type (L span ty) exp_kind
328
  = setSrcSpan span $
329 330 331 332 333 334
    do { traceTc "tc_lhs_type:" (ppr ty $$ ppr exp_kind)
       ; tc_hs_type ty exp_kind }

tc_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [TcType]
tc_lhs_types tys_w_kinds = mapM (uncurry tc_lhs_type) tys_w_kinds

335 336
------------------------------------------
tc_fun_type :: HsType Name -> LHsType Name -> LHsType Name -> ExpKind -> TcM TcType
337
-- We need to recognise (->) so that we can construct a FunTy,
338 339 340 341 342 343 344 345 346
-- *and* we need to do by looking at the Name, not the TyCon
-- (see Note [Zonking inside the knot]).  For example,
-- consider  f :: (->) Int Int  (Trac #7312)
tc_fun_type ty ty1 ty2 exp_kind@(EK _ ctxt)
  = do { ty1' <- tc_lhs_type ty1 (EK openTypeKind ctxt)
       ; ty2' <- tc_lhs_type ty2 (EK openTypeKind ctxt)
       ; checkExpectedKind ty liftedTypeKind exp_kind
       ; return (mkFunTy ty1' ty2') }

347 348 349 350
------------------------------------------
tc_hs_type :: HsType Name -> ExpKind -> TcM TcType
tc_hs_type (HsParTy ty)        exp_kind = tc_lhs_type ty exp_kind
tc_hs_type (HsDocTy ty _)      exp_kind = tc_lhs_type ty exp_kind
351 352 353 354 355
tc_hs_type ty@(HsBangTy {})    _
    -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
    -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
    -- bangs are invalid, so fail. (#7210)
    = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
356
tc_hs_type (HsRecTy _)         _ = panic "tc_hs_type: record" -- Unwrapped by con decls
357
      -- Record types (which only show up temporarily in constructor
358 359 360 361 362 363 364 365
      -- signatures) should have been removed by now

---------- Functions and applications
tc_hs_type hs_ty@(HsTyVar name) exp_kind
  = do { (ty, k) <- tcTyVar name
       ; checkExpectedKind hs_ty k exp_kind
       ; return ty }

366 367
tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind
  = tc_fun_type ty ty1 ty2 exp_kind
368 369

tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind
370 371 372
  | op `hasKey` funTyConKey
  = tc_fun_type hs_ty ty1 ty2 exp_kind
  | otherwise
373 374 375 376 377 378
  = do { (op', op_kind) <- tcTyVar op
       ; tys' <- tcCheckApps hs_ty l_op op_kind [ty1,ty2] exp_kind
       ; return (mkNakedAppTys op' tys') }
         -- mkNakedAppTys: see Note [Zonking inside the knot]

tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind
379 380 381 382 383
--  | L _ (HsTyVar fun) <- fun_ty
--  , fun `hasKey` funTyConKey
--  , [fty1,fty2] <- arg_tys
--  = tc_fun_type hs_ty fty1 fty2 exp_kind
--  | otherwise
384
  = do { (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty
385 386 387
       ; arg_tys' <- tcCheckApps hs_ty fun_ty fun_kind arg_tys exp_kind
       ; return (mkNakedAppTys fun_ty' arg_tys') }
         -- mkNakedAppTys: see Note [Zonking inside the knot]
388
         -- This looks fragile; how do we *know* that fun_ty isn't
Simon Peyton Jones's avatar
Simon Peyton Jones committed
389 390
         -- a TyConApp, say (which is never supposed to appear in the
         -- function position of an AppTy)?
391 392
  where
    (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
393 394

--------- Foralls
thomasw's avatar
thomasw committed
395
tc_hs_type hs_ty@(HsForAllTy _ _ hs_tvs context ty) exp_kind@(EK exp_k _)
396 397 398 399 400
  | isConstraintKind exp_k
  = failWithTc (hang (ptext (sLit "Illegal constraint:")) 2 (ppr hs_ty))

  | otherwise
  = tcHsTyVarBndrs hs_tvs $ \ tvs' ->
401 402
    -- Do not kind-generalise here!  See Note [Kind generalisation]
    do { ctxt' <- tcHsContext context
403 404
       ; ty' <- if null (unLoc context) then  -- Plain forall, no context
                   tc_lhs_type ty exp_kind    -- Why exp_kind?  See Note [Body kind of forall]
405
                else
406
                   -- If there is a context, then this forall is really a
407
                   -- _function_, so the kind of the result really is *
408 409 410
                   -- The body kind (result of the function can be * or #, hence ekOpen
                   do { checkExpectedKind hs_ty liftedTypeKind exp_kind
                      ; tc_lhs_type ty ekOpen }
411 412 413
       ; return (mkSigmaTy tvs' ctxt' ty') }

--------- Lists, arrays, and tuples
414
tc_hs_type hs_ty@(HsListTy elt_ty) exp_kind
415 416 417 418 419 420 421 422 423 424
  = do { tau_ty <- tc_lhs_type elt_ty ekLifted
       ; checkExpectedKind hs_ty liftedTypeKind exp_kind
       ; checkWiredInTyCon listTyCon
       ; return (mkListTy tau_ty) }

tc_hs_type hs_ty@(HsPArrTy elt_ty) exp_kind
  = do { tau_ty <- tc_lhs_type elt_ty ekLifted
       ; checkExpectedKind hs_ty liftedTypeKind exp_kind
       ; checkWiredInTyCon parrTyCon
       ; return (mkPArrTy tau_ty) }
425

dreixel's avatar
dreixel committed
426
-- See Note [Distinguishing tuple kinds] in HsTypes
427
-- See Note [Inferring tuple kinds]
428
tc_hs_type hs_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind@(EK exp_k _ctxt)
429
     -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
430
  | Just tup_sort <- tupKindSort_maybe exp_k
431 432
  = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
    tc_tuple hs_ty tup_sort hs_tys exp_kind
dreixel's avatar
dreixel committed
433
  | otherwise
Austin Seipp's avatar
Austin Seipp committed
434
  = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
435
       ; (tys, kinds) <- mapAndUnzipM tc_infer_lhs_type hs_tys
436
       ; kinds <- mapM zonkTcKind kinds
437 438 439 440 441 442
           -- Infer each arg type separately, because errors can be
           -- confusing if we give them a shared kind.  Eg Trac #7410
           -- (Either Int, Int), we do not want to get an error saying
           -- "the second argument of a tuple should have kind *->*"

       ; let (arg_kind, tup_sort)
443 444 445
               = case [ (k,s) | k <- kinds
                              , Just s <- [tupKindSort_maybe k] ] of
                    ((k,s) : _) -> (k,s)
446
                    [] -> (liftedTypeKind, BoxedTuple)
447 448
         -- In the [] case, it's not clear what the kind is, so guess *

449 450
       ; sequence_ [ setSrcSpan loc $
                     checkExpectedKind ty kind
451
                        (expArgKind (ptext (sLit "a tuple")) arg_kind n)
452
                   | (ty@(L loc _),kind,n) <- zip3 hs_tys kinds [1..] ]
453

454 455
       ; finish_tuple hs_ty tup_sort tys exp_kind }

dreixel's avatar
dreixel committed
456

457
tc_hs_type hs_ty@(HsTupleTy hs_tup_sort tys) exp_kind
458
  = tc_tuple hs_ty tup_sort tys exp_kind
459 460 461 462 463 464 465
  where
    tup_sort = case hs_tup_sort of  -- Fourth case dealt with above
                  HsUnboxedTuple    -> UnboxedTuple
                  HsBoxedTuple      -> BoxedTuple
                  HsConstraintTuple -> ConstraintTuple
                  _                 -> panic "tc_hs_type HsTupleTy"

dreixel's avatar
dreixel committed
466

467 468 469 470 471 472 473 474
--------- Promoted lists and tuples
tc_hs_type hs_ty@(HsExplicitListTy _k tys) exp_kind
  = do { tks <- mapM tc_infer_lhs_type tys
       ; let taus = map fst tks
       ; kind <- unifyKinds (ptext (sLit "In a promoted list")) tks
       ; checkExpectedKind hs_ty (mkPromotedListTy kind) exp_kind
       ; return (foldr (mk_cons kind) (mk_nil kind) taus) }
  where
475 476
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
477 478 479 480

tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
  = do { tks <- mapM tc_infer_lhs_type tys
       ; let n          = length tys
481 482
             kind_con   = promotedTupleTyCon   Boxed n
             ty_con     = promotedTupleDataCon Boxed n
483 484 485 486 487 488 489
             (taus, ks) = unzip tks
             tup_k      = mkTyConApp kind_con ks
       ; checkExpectedKind hs_ty tup_k exp_kind
       ; return (mkTyConApp ty_con (ks ++ taus)) }

--------- Constraint types
tc_hs_type ipTy@(HsIParamTy n ty) exp_kind
490
  = do { ty' <- tc_lhs_type ty ekLifted
491
       ; checkExpectedKind ipTy constraintKind exp_kind
492 493 494 495
       ; ipClass <- tcLookupClass ipClassName
       ; let n' = mkStrLitTy $ hsIPNameFS n
       ; return (mkClassPred ipClass [n',ty'])
       }
496

497
tc_hs_type ty@(HsEqTy ty1 ty2) exp_kind
498 499 500
  = do { (ty1', kind1) <- tc_infer_lhs_type ty1
       ; (ty2', kind2) <- tc_infer_lhs_type ty2
       ; checkExpectedKind ty2 kind2
501
              (EK kind1 msg_fn)
502 503
       ; checkExpectedKind ty constraintKind exp_kind
       ; return (mkNakedTyConApp eqTyCon [kind1, ty1', ty2']) }
504 505 506
  where
    msg_fn pkind = ptext (sLit "The left argument of the equality had kind")
                   <+> quotes (pprKind pkind)
507 508

--------- Misc
509
tc_hs_type (HsKindSig ty sig_k) exp_kind
510 511
  = do { sig_k' <- tcLHsKind sig_k
       ; checkExpectedKind ty sig_k' exp_kind
512 513
       ; tc_lhs_type ty (EK sig_k' msg_fn) }
  where
514
    msg_fn pkind = ptext (sLit "The signature specified kind")
515
                   <+> quotes (pprKind pkind)
516 517 518 519

tc_hs_type (HsCoreTy ty) exp_kind
  = do { checkExpectedKind ty (typeKind ty) exp_kind
       ; return ty }
dreixel's avatar
dreixel committed
520 521


522 523
-- This should never happen; type splices are expanded by the renamer
tc_hs_type ty@(HsSpliceTy {}) _exp_kind
524 525
  = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)

526
tc_hs_type (HsWrapTy {}) _exp_kind
527
  = panic "tc_hs_type HsWrapTy"  -- We kind checked something twice
dreixel's avatar
dreixel committed
528

Alan Zimmerman's avatar
Alan Zimmerman committed
529
tc_hs_type hs_ty@(HsTyLit (HsNumTy _ n)) exp_kind
530 531 532 533
  = do { checkExpectedKind hs_ty typeNatKind exp_kind
       ; checkWiredInTyCon typeNatKindCon
       ; return (mkNumLitTy n) }

Alan Zimmerman's avatar
Alan Zimmerman committed
534
tc_hs_type hs_ty@(HsTyLit (HsStrTy _ s)) exp_kind
535 536
  = do { checkExpectedKind hs_ty typeSymbolKind exp_kind
       ; checkWiredInTyCon typeSymbolKindCon
537
       ; return (mkStrLitTy s) }
538

thomasw's avatar
thomasw committed
539 540 541
tc_hs_type hs_ty@(HsWildCardTy wc) exp_kind
  = do { let name = wildCardName wc
       ; (ty, k) <- tcTyVar name
thomasw's avatar
thomasw committed
542 543 544
       ; checkExpectedKind hs_ty k exp_kind
       ; return ty }

545
---------------------------
546
tupKindSort_maybe :: TcKind -> Maybe TupleSort
547
tupKindSort_maybe k
548 549
  | isConstraintKind k = Just ConstraintTuple
  | isLiftedTypeKind k = Just BoxedTuple
550 551
  | otherwise          = Nothing

552
tc_tuple :: HsType Name -> TupleSort -> [LHsType Name] -> ExpKind -> TcM TcType
553 554 555
tc_tuple hs_ty tup_sort tys exp_kind
  = do { tau_tys <- tc_hs_arg_tys cxt_doc tys (repeat arg_kind)
       ; finish_tuple hs_ty tup_sort tau_tys exp_kind }
dreixel's avatar
dreixel committed
556 557
  where
    arg_kind = case tup_sort of
558 559 560
                 BoxedTuple      -> liftedTypeKind
                 UnboxedTuple    -> openTypeKind
                 ConstraintTuple -> constraintKind
dreixel's avatar
dreixel committed
561
    cxt_doc = case tup_sort of
562 563 564
                 BoxedTuple      -> ptext (sLit "a tuple")
                 UnboxedTuple    -> ptext (sLit "an unboxed tuple")
                 ConstraintTuple -> ptext (sLit "a constraint tuple")
dreixel's avatar
dreixel committed
565

566
finish_tuple :: HsType Name -> TupleSort -> [TcType] -> ExpKind -> TcM TcType
567
finish_tuple hs_ty tup_sort tau_tys exp_kind
568 569
  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr exp_kind $$ ppr exp_kind)
       ; checkExpectedKind hs_ty res_kind exp_kind
570
       ; tycon <- case tup_sort of
571 572 573 574 575 576 577 578
           ConstraintTuple
             | arity > mAX_CTUPLE_SIZE
                         -> failWith (bigConstraintTuple arity)
             | otherwise -> tcLookupTyCon (cTupleTyConName arity)
           BoxedTuple    -> do { let tc = tupleTyCon Boxed arity
                               ; checkWiredInTyCon tc
                               ; return tc }
           UnboxedTuple  -> return (tupleTyCon Unboxed arity)
579 580
       ; return (mkTyConApp tycon tau_tys) }
  where
581
    arity = length tau_tys
582
    res_kind = case tup_sort of
583 584 585
                 UnboxedTuple    -> unliftedTypeKind
                 BoxedTuple      -> liftedTypeKind
                 ConstraintTuple -> constraintKind
586

587 588 589 590 591 592
bigConstraintTuple :: Arity -> MsgDoc
bigConstraintTuple arity
  = hang (ptext (sLit "Constraint tuple arity too large:") <+> int arity
          <+> parens (ptext (sLit "max arity =") <+> int mAX_CTUPLE_SIZE))
       2 (ptext (sLit "Instead, use a nested tuple"))

593
---------------------------
594
tcInferApps :: Outputable a
595 596 597 598
       => a
       -> TcKind                        -- Function kind
       -> [LHsType Name]                -- Arg types
       -> TcM ([TcType], TcKind)        -- Kind-checked args
599 600 601
tcInferApps the_fun fun_kind args
  = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) fun_kind args
       ; args' <- tc_lhs_types args_w_kinds
602 603
       ; return (args', res_kind) }

604
tcCheckApps :: Outputable a
605 606 607
            => HsType Name     -- The type being checked (for err messages only)
            -> a               -- The function
            -> TcKind -> [LHsType Name]   -- Fun kind and arg types
608 609
            -> ExpKind                    -- Expected kind
            -> TcM [TcType]
610 611 612 613
tcCheckApps hs_ty the_fun fun_kind args exp_kind
  = do { (arg_tys, res_kind) <- tcInferApps the_fun fun_kind args
       ; checkExpectedKind hs_ty res_kind exp_kind
       ; return arg_tys }
614

615
---------------------------
616 617 618
splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
splitFunKind the_fun fun_kind args
  = go 1 fun_kind args
619
  where
620 621 622 623
    go _      fk [] = return ([], fk)
    go arg_no fk (arg:args)
       = do { mb_fk <- matchExpectedFunKind fk
            ; case mb_fk of
624
                 Nothing       -> failWithTc too_many_args
625 626 627
                 Just (ak,fk') -> do { (aks, rk) <- go (arg_no+1) fk' args
                                     ; let exp_kind = expArgKind (quotes the_fun) ak arg_no
                                     ; return ((arg, exp_kind) : aks, rk) } }
628

629
    too_many_args = quotes the_fun <+>
630
                    ptext (sLit "is applied to too many type arguments")
631

632

633
---------------------------
634 635
tcHsContext :: LHsContext Name -> TcM [PredType]
tcHsContext ctxt = mapM tcHsLPredType (unLoc ctxt)
636

637 638
tcHsLPredType :: LHsType Name -> TcM PredType
tcHsLPredType pred = tc_lhs_type pred ekConstraint
639 640

---------------------------
641
tcTyVar :: Name -> TcM (TcType, TcKind)
dreixel's avatar
dreixel committed
642 643
-- See Note [Type checking recursive type and class declarations]
-- in TcTyClsDecls
644
tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
dreixel's avatar
dreixel committed
645 646 647
  = do { traceTc "lk1" (ppr name)
       ; thing <- tcLookup name
       ; case thing of
648
           ATyVar _ tv
649 650 651 652 653
              | isKindVar tv
              -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr tv)
                             <+> ptext (sLit "used as a type"))
              | otherwise
              -> return (mkTyVarTy tv, tyVarKind tv)
654 655 656 657 658 659 660

           AThing kind -> do { tc <- get_loopy_tc name
                             ; inst_tycon (mkNakedTyConApp tc) kind }
                             -- mkNakedTyConApp: see Note [Zonking inside the knot]

           AGlobal (ATyCon tc) -> inst_tycon (mkTyConApp tc) (tyConKind tc)

cactus's avatar
cactus committed
661
           AGlobal (AConLike (RealDataCon dc))
662
             | Just tc <- promoteDataCon_maybe dc
663 664 665
             -> do { data_kinds <- xoptM Opt_DataKinds
                   ; unless data_kinds $ promotionErr name NoDataKinds
                   ; inst_tycon (mkTyConApp tc) (tyConKind tc) }
666
             | otherwise -> failWithTc (ptext (sLit "Data constructor") <+> quotes (ppr dc)
667
                                        <+> ptext (sLit "comes from an un-promotable type")
668
                                        <+> quotes (ppr (dataConTyCon dc)))
669

670
           APromotionErr err -> promotionErr name err
671 672

           _  -> wrongThingErr "type" thing name }
dreixel's avatar
dreixel committed
673
  where
674 675 676 677 678 679 680 681 682 683
    get_loopy_tc name
      = do { env <- getGblEnv
           ; case lookupNameEnv (tcg_type_env env) name of
                Just (ATyCon tc) -> return tc
                _                -> return (aThingErr "tcTyVar" name) }

    inst_tycon :: ([Type] -> Type) -> Kind -> TcM (Type, Kind)
    -- Instantiate the polymorphic kind
    -- Lazy in the TyCon
    inst_tycon mk_tc_app kind
684
      | null kvs
685
      = return (mk_tc_app [], ki_body)
dreixel's avatar
dreixel committed
686 687
      | otherwise
      = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind)
688 689
           ; ks <- mapM (const newMetaKindVar) kvs
           ; return (mk_tc_app ks, substKiWith kvs ks ki_body) }
690
      where
691 692 693
        (kvs, ki_body) = splitForAllTys kind

tcClass :: Name -> TcM (Class, TcKind)
694
tcClass cls     -- Must be a class
695 696 697 698
  = do { thing <- tcLookup cls
       ; case thing of
           AThing kind -> return (aThingErr "tcClass" cls, kind)
           AGlobal (ATyCon tc)
699
             | Just cls <- tyConClass_maybe tc
700 701 702 703 704 705 706 707 708
             -> return (cls, tyConKind tc)
           _ -> wrongThingErr "class" thing cls }


aThingErr :: String -> Name -> b
-- The type checker for types is sometimes called simply to
-- do *kind* checking; and in that case it ignores the type
-- returned. Which is a good thing since it may not be available yet!
aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
709

Austin Seipp's avatar
Austin Seipp committed
710
{-
711 712 713 714 715
Note [Zonking inside the knot]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are checking the argument types of a data constructor.  We
must zonk the types before making the DataCon, because once built we
can't change it.  So we must traverse the type.
716

717
BUT the parent TyCon is knot-tied, so we can't look at it yet.
718 719

So we must be careful not to use "smart constructors" for types that
720
look at the TyCon or Class involved.
721

722 723 724
  * Hence the use of mkNakedXXX functions. These do *not* enforce
    the invariants (for example that we use (FunTy s t) rather
    than (TyConApp (->) [s,t])).
725 726 727 728 729 730 731 732 733 734 735 736

  * Ditto in zonkTcType (which may be applied more than once, eg to
    squeeze out kind meta-variables), we are careful not to look at
    the TyCon.

  * We arrange to call zonkSigType *once* right at the end, and it
    does establish the invariants.  But in exchange we can't look
    at the result (not even its structure) until we have emerged
    from the "knot".

  * TcHsSyn.zonkTcTypeToType also can safely check/establish
    invariants.
737

738 739
This is horribly delicate.  I hate it.  A good example of how
delicate it is can be seen in Trac #7903.
Austin Seipp's avatar
Austin Seipp committed
740
-}
741 742

mkNakedTyConApp :: TyCon -> [Type] -> Type
743
-- Builds a TyConApp
744 745 746 747 748 749 750 751 752 753 754 755
--   * without being strict in TyCon,
--   * without satisfying the invariants of TyConApp
-- A subsequent zonking will establish the invariants
mkNakedTyConApp tc tys = TyConApp tc tys

mkNakedAppTys :: Type -> [Type] -> Type
mkNakedAppTys ty1                []   = ty1
mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
mkNakedAppTys ty1                tys2 = foldl AppTy ty1 tys2

zonkSigType :: TcType -> TcM TcType
-- Zonk the result of type-checking a user-written type signature
756
-- It may have kind variables in it, but no meta type variables
757
-- Because of knot-typing (see Note [Zonking inside the knot])
758
-- it may need to establish the Type invariants;
759 760 761 762 763 764
-- hence the use of mkTyConApp and mkAppTy
zonkSigType ty
  = go ty
  where
    go (TyConApp tc tys) = do tys' <- mapM go tys
                              return (mkTyConApp tc tys')
765 766
                -- Key point: establish Type invariants!
                -- See Note [Zonking inside the knot]
767 768 769 770 771 772 773 774 775 776

    go (LitTy n)         = return (LitTy n)

    go (FunTy arg res)   = do arg' <- go arg
                              res' <- go res
                              return (FunTy arg' res')

    go (AppTy fun arg)   = do fun' <- go fun
                              arg' <- go arg
                              return (mkAppTy fun' arg')
777 778 779
                -- NB the mkAppTy; we might have instantiated a
                -- type variable to a type constructor, so we need
                -- to pull the TyConApp to the top.
780

781
        -- The two interesting cases!
782
    go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
783 784
                       | otherwise       = TyVarTy <$> updateTyVarKindM go tyvar
                -- Ordinary (non Tc) tyvars occur inside quantified types
785 786 787 788

    go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
                             ; ty' <- go ty
                             ; return (ForAllTy tv' ty') }
789

Austin Seipp's avatar
Austin Seipp committed
790
{-
791 792 793 794 795
Note [Body kind of a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The body of a forall is usually a type, but in principle
there's no reason to prohibit *unlifted* types.
In fact, GHC can itself construct a function with an
796
unboxed tuple inside a for-all (via CPR analyis; see
797 798 799
typecheck/should_compile/tc170).

Moreover in instance heads we get forall-types with
800
kind Constraint.
801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834

Moreover if we have a signature
   f :: Int#
then we represent it as (HsForAll Implicit [] [] Int#).  And this must
be legal!  We can't drop the empty forall until *after* typechecking
the body because of kind polymorphism:
   Typeable :: forall k. k -> Constraint
   data Apply f t = Apply (f t)
   -- Apply :: forall k. (k -> *) -> k -> *
   instance Typeable Apply where ...
Then the dfun has type
   df :: forall k. Typeable ((k->*) -> k -> *) (Apply k)

   f :: Typeable Apply

   f :: forall (t:k->*) (a:k).  t a -> t a

   class C a b where
      op :: a b -> Typeable Apply

   data T a = MkT (Typeable Apply)
            | T2 a
      T :: * -> *
      MkT :: forall k. (Typeable ((k->*) -> k -> *) (Apply k)) -> T a

   f :: (forall (k:BOX). forall (t:: k->*) (a:k). t a -> t a) -> Int
   f :: (forall a. a -> Typeable Apply) -> Int

So we *must* keep the HsForAll on the instance type
   HsForAll Implicit [] [] (Typeable Apply)
so that we do kind generalisation on it.

Really we should check that it's a type of value kind
{*, Constraint, #}, but I'm not doing that yet
835
Example that should be rejected:
836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856
         f :: (forall (a:*->*). a) Int

Note [Inferring tuple kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
we try to figure out whether it's a tuple of kind * or Constraint.
  Step 1: look at the expected kind
  Step 2: infer argument kinds

If after Step 2 it's not clear from the arguments that it's
Constraint, then it must be *.  Once having decided that we re-check
the Check the arguments again to give good error messages
in eg. `(Maybe, Maybe)`

Note that we will still fail to infer the correct kind in this case:

  type T a = ((a,a), D a)
  type family D :: Constraint -> Constraint

While kind checking T, we do not yet know the kind of D, so we will default the
kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
857

dreixel's avatar
dreixel committed
858 859 860 861 862 863 864 865
Note [Desugaring types]
~~~~~~~~~~~~~~~~~~~~~~~
The type desugarer is phase 2 of dealing with HsTypes.  Specifically:

  * It transforms from HsType to Type

  * It zonks any kinds.  The returned type should have no mutable kind
    or type variables (hence returning Type not TcType):
866 867 868
      - any unconstrained kind variables are defaulted to AnyK just
        as in TcHsSyn.
      - there are no mutable type variables because we are
dreixel's avatar
dreixel committed
869 870 871 872 873 874 875 876 877 878 879 880 881 882 883
        kind-checking a type
    Reason: the returned type may be put in a TyCon or DataCon where
    it will never subsequently be zonked.

You might worry about nested scopes:
        ..a:kappa in scope..
            let f :: forall b. T '[a,b] -> Int
In this case, f's type could have a mutable kind variable kappa in it;
and we might then default it to AnyK when dealing with f's type
signature.  But we don't expect this to happen because we can't get a
lexically scoped type variable with a mutable kind variable in it.  A
delicate point, this.  If it becomes an issue we might need to
distinguish top-level from nested uses.

Moreover
884
  * it cannot fail,
dreixel's avatar
dreixel committed
885 886
  * it does no unifications
  * it does no validity checking, except for structural matters, such as
887 888
        (a) spurious ! annotations.
        (b) a class used as a type
889

dreixel's avatar
dreixel committed
890 891 892 893 894 895 896
Note [Kind of a type splice]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider these terms, each with TH type splice inside:
     [| e1 :: Maybe $(..blah..) |]
     [| e2 :: $(..blah..) |]
When kind-checking the type signature, we'll kind-check the splice
$(..blah..); we want to give it a kind that can fit in any context,
897
as if $(..blah..) :: forall k. k.
dreixel's avatar
dreixel committed
898 899 900

In the e1 example, the context of the splice fixes kappa to *.  But
in the e2 example, we'll desugar the type, zonking the kind unification
Krzysztof Gogolewski's avatar
Typos  
Krzysztof Gogolewski committed
901
variables as we go.  When we encounter the unconstrained kappa, we
dreixel's avatar
dreixel committed
902 903 904
want to default it to '*', not to AnyK.


905 906
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Austin Seipp's avatar
Austin Seipp committed
907
-}
908

909
addTypeCtxt :: LHsType Name -> TcM a -> TcM a
910 911 912
        -- Wrap a context around only if we want to show that contexts.
        -- Omit invisble ones and ones user's won't grok
addTypeCtxt (L _ ty) thing