TcHsType.hs 67 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
import Unique
65
import UniqSupply
66
import Outputable
67
import FastString
68 69
import Util

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

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

Generally speaking we now type-check types in three phases

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

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

  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
94 95 96
        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
97 98

For example, when we find
99
        (forall a m. m a -> m a)
100 101 102 103 104 105 106
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
107
        the rest of the program
108
  * For a tyvar bound in a pattern type signature, its the types
109
        mentioned in the other type signatures in that bunch of patterns
110
  * For a tyvar bound in a RULE, it's the type signatures on other
111
        universally quantified variables in the rule
112 113 114

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

115
        data T a b = MkT (a b)
116

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


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

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
128 129
  e.g.  type T k = k Int
        type S a = a
130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
  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
151 152
************************************************************************
*                                                                      *
153
              Check types AND do validity checking
Austin Seipp's avatar
Austin Seipp committed
154 155 156
*                                                                      *
************************************************************************
-}
157

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

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

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

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

tc_inst_head :: HsType Name -> TcM TcType
thomasw's avatar
thomasw committed
191
tc_inst_head (HsForAllTy _ _ hs_tvs hs_ctxt hs_ty)
192
  = tcHsTyVarBndrs hs_tvs $ \ tvs ->
193 194 195 196 197 198
    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
199

200
-----------------
201
tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type], Kind)
202
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
203 204 205 206 207 208 209 210 211 212 213
-- 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
214 215
       ; let (tvs, pred) = splitForAllTys ty
       ; case getClassPredTys_maybe pred of
216
           Just (cls, tys) -> return (tvs, cls, tys, arg_kind)
217
           Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) }
218 219 220 221 222 223

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

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


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

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

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

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

256
tcHsConArgType DataType bty = tcHsOpenType (getBangType bty)
257 258 259 260
  -- 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

261
---------------------------
262 263 264 265 266 267 268 269 270 271 272
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..] ]
273

dreixel's avatar
dreixel committed
274
---------------------------
275
tcHsOpenType, tcHsLiftedType :: LHsType Name -> TcM TcType
276 277
-- Used for type signatures
-- Do not do validity checking
278
tcHsOpenType ty   = addTypeCtxt ty $ tc_lhs_type ty ekOpen
279 280 281 282 283
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
284
  = addTypeCtxt hs_ty $
285
    tc_lhs_type hs_ty (EK exp_kind expectedKindMsg)
286 287 288 289

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
290

291
---------------------------
292
tcCheckLHsTypeAndGen :: LHsType Name -> Kind -> TcM Type
293 294
-- Typecheck a type signature, and kind-generalise it
-- The result is not necessarily zonked, and has not been checked for validity
295 296 297 298 299 300 301 302 303
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
304
tcCheckHsTypeAndGen hs_ty kind
305
  = do { ty  <- tc_hs_type hs_ty (EK kind expectedKindMsg)
306
       ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty)
307
       ; kvs <- zonkTcTypeAndFV ty
308
       ; kvs <- kindGeneralize kvs
309
       ; return (mkForAllTys kvs ty) }
310

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

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

tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType
tc_lhs_type (L span ty) exp_kind
326
  = setSrcSpan span $
327 328 329 330 331 332
    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

333 334
------------------------------------------
tc_fun_type :: HsType Name -> LHsType Name -> LHsType Name -> ExpKind -> TcM TcType
335
-- We need to recognise (->) so that we can construct a FunTy,
336 337 338 339 340 341 342 343 344
-- *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') }

345 346 347 348
------------------------------------------
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
349 350 351 352 353
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)
354
tc_hs_type (HsRecTy _)         _ = panic "tc_hs_type: record" -- Unwrapped by con decls
355
      -- Record types (which only show up temporarily in constructor
356 357 358 359 360 361 362 363
      -- 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 }

364 365
tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind
  = tc_fun_type ty ty1 ty2 exp_kind
366 367

tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind
368 369 370
  | op `hasKey` funTyConKey
  = tc_fun_type hs_ty ty1 ty2 exp_kind
  | otherwise
371 372 373 374 375 376
  = 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
377 378 379 380 381
--  | L _ (HsTyVar fun) <- fun_ty
--  , fun `hasKey` funTyConKey
--  , [fty1,fty2] <- arg_tys
--  = tc_fun_type hs_ty fty1 fty2 exp_kind
--  | otherwise
382
  = do { (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty
383 384 385
       ; 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]
386
         -- This looks fragile; how do we *know* that fun_ty isn't
Simon Peyton Jones's avatar
Simon Peyton Jones committed
387 388
         -- a TyConApp, say (which is never supposed to appear in the
         -- function position of an AppTy)?
389 390
  where
    (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
391 392

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

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

--------- Lists, arrays, and tuples
412
tc_hs_type hs_ty@(HsListTy elt_ty) exp_kind
413 414 415 416 417 418 419 420 421 422
  = 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) }
423

dreixel's avatar
dreixel committed
424
-- See Note [Distinguishing tuple kinds] in HsTypes
425
-- See Note [Inferring tuple kinds]
426
tc_hs_type hs_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind@(EK exp_k _ctxt)
427
     -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
428
  | Just tup_sort <- tupKindSort_maybe exp_k
429 430
  = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
    tc_tuple hs_ty tup_sort hs_tys exp_kind
dreixel's avatar
dreixel committed
431
  | otherwise
Austin Seipp's avatar
Austin Seipp committed
432
  = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
433
       ; (tys, kinds) <- mapAndUnzipM tc_infer_lhs_type hs_tys
434
       ; kinds <- mapM zonkTcKind kinds
435 436 437 438 439 440
           -- 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)
441 442 443
               = case [ (k,s) | k <- kinds
                              , Just s <- [tupKindSort_maybe k] ] of
                    ((k,s) : _) -> (k,s)
444
                    [] -> (liftedTypeKind, BoxedTuple)
445 446
         -- In the [] case, it's not clear what the kind is, so guess *

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

452 453
       ; finish_tuple hs_ty tup_sort tys exp_kind }

dreixel's avatar
dreixel committed
454

455
tc_hs_type hs_ty@(HsTupleTy hs_tup_sort tys) exp_kind
456
  = tc_tuple hs_ty tup_sort tys exp_kind
457 458 459 460 461 462 463
  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
464

465 466 467 468 469 470 471 472
--------- 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
473 474
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
475 476 477 478

tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
  = do { tks <- mapM tc_infer_lhs_type tys
       ; let n          = length tys
Austin Seipp's avatar
Austin Seipp committed
479 480
             kind_con   = promotedTupleTyCon   BoxedTuple n
             ty_con     = promotedTupleDataCon BoxedTuple n
481 482 483 484 485 486 487
             (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
488
  = do { ty' <- tc_lhs_type ty ekLifted
489
       ; checkExpectedKind ipTy constraintKind exp_kind
490 491 492 493
       ; ipClass <- tcLookupClass ipClassName
       ; let n' = mkStrLitTy $ hsIPNameFS n
       ; return (mkClassPred ipClass [n',ty'])
       }
494

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

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

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


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

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

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

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

thomasw's avatar
thomasw committed
537 538 539 540 541 542 543 544 545

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 }

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

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

567
finish_tuple :: HsType Name -> TupleSort -> [TcType] -> ExpKind -> TcM TcType
568
finish_tuple hs_ty tup_sort tau_tys exp_kind
569 570
  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr exp_kind $$ ppr exp_kind)
       ; checkExpectedKind hs_ty res_kind exp_kind
Austin Seipp's avatar
Austin Seipp committed
571
       ; checkWiredInTyCon tycon
572 573
       ; return (mkTyConApp tycon tau_tys) }
  where
Austin Seipp's avatar
Austin Seipp committed
574
    tycon = tupleTyCon tup_sort (length tau_tys)
575
    res_kind = case tup_sort of
576 577 578
                 UnboxedTuple    -> unliftedTypeKind
                 BoxedTuple      -> liftedTypeKind
                 ConstraintTuple -> constraintKind
579

580
---------------------------
581
tcInferApps :: Outputable a
582 583 584 585
       => a
       -> TcKind                        -- Function kind
       -> [LHsType Name]                -- Arg types
       -> TcM ([TcType], TcKind)        -- Kind-checked args
586 587 588
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
589 590
       ; return (args', res_kind) }

591
tcCheckApps :: Outputable a
592 593 594
            => HsType Name     -- The type being checked (for err messages only)
            -> a               -- The function
            -> TcKind -> [LHsType Name]   -- Fun kind and arg types
595 596
            -> ExpKind                    -- Expected kind
            -> TcM [TcType]
597 598 599 600
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 }
601

602
---------------------------
603 604 605
splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
splitFunKind the_fun fun_kind args
  = go 1 fun_kind args
606
  where
607 608 609 610
    go _      fk [] = return ([], fk)
    go arg_no fk (arg:args)
       = do { mb_fk <- matchExpectedFunKind fk
            ; case mb_fk of
611
                 Nothing       -> failWithTc too_many_args
612 613 614
                 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) } }
615

616
    too_many_args = quotes the_fun <+>
617
                    ptext (sLit "is applied to too many type arguments")
618

619

620
---------------------------
621 622
tcHsContext :: LHsContext Name -> TcM [PredType]
tcHsContext ctxt = mapM tcHsLPredType (unLoc ctxt)
623

624 625
tcHsLPredType :: LHsType Name -> TcM PredType
tcHsLPredType pred = tc_lhs_type pred ekConstraint
626 627

---------------------------
628
tcTyVar :: Name -> TcM (TcType, TcKind)
dreixel's avatar
dreixel committed
629 630
-- See Note [Type checking recursive type and class declarations]
-- in TcTyClsDecls
631
tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
dreixel's avatar
dreixel committed
632 633 634
  = do { traceTc "lk1" (ppr name)
       ; thing <- tcLookup name
       ; case thing of
635
           ATyVar _ tv
636 637 638 639 640
              | isKindVar tv
              -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr tv)
                             <+> ptext (sLit "used as a type"))
              | otherwise
              -> return (mkTyVarTy tv, tyVarKind tv)
641 642 643 644 645 646 647

           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
648
           AGlobal (AConLike (RealDataCon dc))
649
             | Just tc <- promoteDataCon_maybe dc
650 651 652
             -> do { data_kinds <- xoptM Opt_DataKinds
                   ; unless data_kinds $ promotionErr name NoDataKinds
                   ; inst_tycon (mkTyConApp tc) (tyConKind tc) }
653
             | otherwise -> failWithTc (ptext (sLit "Data constructor") <+> quotes (ppr dc)
654
                                        <+> ptext (sLit "comes from an un-promotable type")
655
                                        <+> quotes (ppr (dataConTyCon dc)))
656

657
           APromotionErr err -> promotionErr name err
658 659

           _  -> wrongThingErr "type" thing name }
dreixel's avatar
dreixel committed
660
  where
661 662 663 664 665 666 667 668 669 670
    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
671
      | null kvs
672
      = return (mk_tc_app [], ki_body)
dreixel's avatar
dreixel committed
673 674
      | otherwise
      = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind)
675 676
           ; ks <- mapM (const newMetaKindVar) kvs
           ; return (mk_tc_app ks, substKiWith kvs ks ki_body) }
677
      where
678 679 680
        (kvs, ki_body) = splitForAllTys kind

tcClass :: Name -> TcM (Class, TcKind)
681
tcClass cls     -- Must be a class
682 683 684 685
  = do { thing <- tcLookup cls
       ; case thing of
           AThing kind -> return (aThingErr "tcClass" cls, kind)
           AGlobal (ATyCon tc)
686
             | Just cls <- tyConClass_maybe tc
687 688 689 690 691 692 693 694 695
             -> 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)
696

Austin Seipp's avatar
Austin Seipp committed
697
{-
698 699 700 701 702
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.
703

704
BUT the parent TyCon is knot-tied, so we can't look at it yet.
705 706

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

709 710 711
  * 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])).
712 713 714 715 716 717 718 719 720 721 722 723

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

725 726
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
727
-}
728 729

mkNakedTyConApp :: TyCon -> [Type] -> Type
730
-- Builds a TyConApp
731 732 733 734 735 736 737 738 739 740 741 742
--   * 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
743
-- It may have kind variables in it, but no meta type variables
744
-- Because of knot-typing (see Note [Zonking inside the knot])
745
-- it may need to establish the Type invariants;
746 747 748 749 750 751
-- 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')
752 753
                -- Key point: establish Type invariants!
                -- See Note [Zonking inside the knot]
754 755 756 757 758 759 760 761 762 763

    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')
764 765 766
                -- NB the mkAppTy; we might have instantiated a
                -- type variable to a type constructor, so we need
                -- to pull the TyConApp to the top.
767

768
        -- The two interesting cases!
769
    go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
770 771
                       | otherwise       = TyVarTy <$> updateTyVarKindM go tyvar
                -- Ordinary (non Tc) tyvars occur inside quantified types
772 773 774 775

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

Austin Seipp's avatar
Austin Seipp committed
777
{-
778 779 780 781 782
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
783
unboxed tuple inside a for-all (via CPR analyis; see
784 785 786
typecheck/should_compile/tc170).

Moreover in instance heads we get forall-types with
787
kind Constraint.
788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821

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
822
Example that should be rejected:
823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843
         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`.
844

dreixel's avatar
dreixel committed
845 846 847 848 849 850 851 852
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):
853 854 855
      - 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
856 857 858 859 860 861 862 863 864 865 866 867 868 869 870
        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
871
  * it cannot fail,
dreixel's avatar
dreixel committed
872 873
  * it does no unifications
  * it does no validity checking, except for structural matters, such as
874 875
        (a) spurious ! annotations.
        (b) a class used as a type
876

dreixel's avatar
dreixel committed
877 878 879 880 881 882 883
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,
884
as if $(..blah..) :: forall k. k.
dreixel's avatar
dreixel committed
885 886 887

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
888
variables as we go.  When we encounter the unconstrained kappa, we
dreixel's avatar
dreixel committed
889 890 891
want to default it to '*', not to AnyK.


892 893
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Austin Seipp's avatar
Austin Seipp committed
894
-}
895

896
addTypeCtxt :: LHsType Name -> TcM a -> TcM a
897 898 899
        -- 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
900 901 902
  = addErrCtxt doc thing
  where
    doc = ptext (sLit "In the type") <+> quotes (ppr ty)
903

Austin Seipp's avatar
Austin Seipp committed
904 905 906
{-
************************************************************************
*                                                                      *
907
                Type-variable binders
Austin Seipp's avatar
Austin Seipp committed
908 909 910
*                                                                      *
************************************************************************
-}
911