TcHsType.hs 67.7 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 542 543 544 545 546 547

tc_hs_type HsWildcardTy _ = panic "tc_hs_type HsWildcardTy"
-- unnamed wildcards should have been replaced by named wildcards

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

548
---------------------------
549
tupKindSort_maybe :: TcKind -> Maybe TupleSort
550
tupKindSort_maybe k
551 552
  | isConstraintKind k = Just ConstraintTuple
  | isLiftedTypeKind k = Just BoxedTuple
553 554
  | otherwise          = Nothing

555
tc_tuple :: HsType Name -> TupleSort -> [LHsType Name] -> ExpKind -> TcM TcType
556 557 558
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
559 560
  where
    arg_kind = case tup_sort of
561 562 563
                 BoxedTuple      -> liftedTypeKind
                 UnboxedTuple    -> openTypeKind
                 ConstraintTuple -> constraintKind
dreixel's avatar
dreixel committed
564
    cxt_doc = case tup_sort of
565 566 567
                 BoxedTuple      -> ptext (sLit "a tuple")
                 UnboxedTuple    -> ptext (sLit "an unboxed tuple")
                 ConstraintTuple -> ptext (sLit "a constraint tuple")
dreixel's avatar
dreixel committed
568

569
finish_tuple :: HsType Name -> TupleSort -> [TcType] -> ExpKind -> TcM TcType
570
finish_tuple hs_ty tup_sort tau_tys exp_kind
571 572
  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr exp_kind $$ ppr exp_kind)
       ; checkExpectedKind hs_ty res_kind exp_kind
573
       ; tycon <- case tup_sort of
574 575 576 577 578 579 580 581
           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)
582 583
       ; return (mkTyConApp tycon tau_tys) }
  where
584
    arity = length tau_tys
585
    res_kind = case tup_sort of
586 587 588
                 UnboxedTuple    -> unliftedTypeKind
                 BoxedTuple      -> liftedTypeKind
                 ConstraintTuple -> constraintKind
589

590 591 592 593 594 595
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"))

596
---------------------------
597
tcInferApps :: Outputable a
598 599 600 601
       => a
       -> TcKind                        -- Function kind
       -> [LHsType Name]                -- Arg types
       -> TcM ([TcType], TcKind)        -- Kind-checked args
602 603 604
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
605 606
       ; return (args', res_kind) }

607
tcCheckApps :: Outputable a
608 609 610
            => HsType Name     -- The type being checked (for err messages only)
            -> a               -- The function
            -> TcKind -> [LHsType Name]   -- Fun kind and arg types
611 612
            -> ExpKind                    -- Expected kind
            -> TcM [TcType]
613 614 615 616
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 }
617

618
---------------------------
619 620 621
splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
splitFunKind the_fun fun_kind args
  = go 1 fun_kind args
622
  where
623 624 625 626
    go _      fk [] = return ([], fk)
    go arg_no fk (arg:args)
       = do { mb_fk <- matchExpectedFunKind fk
            ; case mb_fk of
627
                 Nothing       -> failWithTc too_many_args
628 629 630
                 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) } }
631

632
    too_many_args = quotes the_fun <+>
633
                    ptext (sLit "is applied to too many type arguments")
634

635

636
---------------------------
637 638
tcHsContext :: LHsContext Name -> TcM [PredType]
tcHsContext ctxt = mapM tcHsLPredType (unLoc ctxt)
639

640 641
tcHsLPredType :: LHsType Name -> TcM PredType
tcHsLPredType pred = tc_lhs_type pred ekConstraint
642 643

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

           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
664
           AGlobal (AConLike (RealDataCon dc))
665
             | Just tc <- promoteDataCon_maybe dc
666 667 668
             -> do { data_kinds <- xoptM Opt_DataKinds
                   ; unless data_kinds $ promotionErr name NoDataKinds
                   ; inst_tycon (mkTyConApp tc) (tyConKind tc) }
669
             | otherwise -> failWithTc (ptext (sLit "Data constructor") <+> quotes (ppr dc)
670
                                        <+> ptext (sLit "comes from an un-promotable type")
671
                                        <+> quotes (ppr (dataConTyCon dc)))
672

673
           APromotionErr err -> promotionErr name err
674 675

           _  -> wrongThingErr "type" thing name }
dreixel's avatar
dreixel committed
676
  where
677 678 679 680 681 682 683 684 685 686
    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
687
      | null kvs
688
      = return (mk_tc_app [], ki_body)
dreixel's avatar
dreixel committed
689 690
      | otherwise
      = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind)
691 692
           ; ks <- mapM (const newMetaKindVar) kvs
           ; return (mk_tc_app ks, substKiWith kvs ks ki_body) }
693
      where
694 695 696
        (kvs, ki_body) = splitForAllTys kind

tcClass :: Name -> TcM (Class, TcKind)
697
tcClass cls     -- Must be a class
698 699 700 701
  = do { thing <- tcLookup cls
       ; case thing of
           AThing kind -> return (aThingErr "tcClass" cls, kind)
           AGlobal (ATyCon tc)
702
             | Just cls <- tyConClass_maybe tc
703 704 705 706 707 708 709 710 711
             -> 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)
712

Austin Seipp's avatar
Austin Seipp committed
713
{-
714 715 716 717 718
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.
719

720
BUT the parent TyCon is knot-tied, so we can't look at it yet.
721 722

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

725 726 727
  * 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])).
728 729 730 731 732 733 734 735 736 737 738 739

  * 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.
740

741 742
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
743
-}
744 745

mkNakedTyConApp :: TyCon -> [Type] -> Type
746
-- Builds a TyConApp
747 748 749 750 751 752 753 754 755 756 757 758
--   * 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
759
-- It may have kind variables in it, but no meta type variables
760
-- Because of knot-typing (see Note [Zonking inside the knot])
761
-- it may need to establish the Type invariants;
762 763 764 765 766 767
-- 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')
768 769
                -- Key point: establish Type invariants!
                -- See Note [Zonking inside the knot]
770 771 772 773 774 775 776 777 778 779

    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')
780 781 782
                -- NB the mkAppTy; we might have instantiated a
                -- type variable to a type constructor, so we need
                -- to pull the TyConApp to the top.
783

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

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

Austin Seipp's avatar
Austin Seipp committed
793
{-
794 795 796 797 798
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
799
unboxed tuple inside a for-all (via CPR analyis; see
800 801 802
typecheck/should_compile/tc170).

Moreover in instance heads we get forall-types with
803
kind Constraint.
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 835 836 837

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
838
Example that should be rejected:
839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859
         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`.
860

dreixel's avatar
dreixel committed
861 862 863 864 865 866 867 868
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):
869 870 871
      - 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
872 873 874 875 876 877 878 879 880 881 882 883 884 885 886
        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
887
  * it cannot fail,
dreixel's avatar
dreixel committed
888 889
  * it does no unifications
  * it does no validity checking, except for structural matters, such as
890 891
        (a) spurious ! annotations.
        (b) a class used as a type
892

dreixel's avatar
dreixel committed
893 894 895 896 897 898 899
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,
900
as if $(..blah..) :: forall k. k.
dreixel's avatar
dreixel committed
901 902 903

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
904
variables as we go.  When we encounter the unconstrained kappa, we
dreixel's avatar
dreixel committed
905 906 907
want to default it to '*', not to AnyK.


908 909
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Austin Seipp's avatar
Austin Seipp committed
910
-}
911

912
addTypeCtxt :: LHsType Name -> TcM a -> TcM a
913 914 915
        -- 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