TcHsType.hs 66.9 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 12 13
        tcHsSigType, tcHsSigTypeNC, tcHsDeriv, tcHsVectInst,
        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,
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, tcHsSigTypeNC :: 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
tcHsSigType ctxt hs_ty
163
  = addErrCtxt (pprSigCtxt ctxt empty (ppr hs_ty)) $
164 165
    tcHsSigTypeNC ctxt hs_ty

166 167 168 169 170 171
tcHsSigTypeNC ctxt (L loc hs_ty)
  = setSrcSpan loc $    -- The "In the type..." context
                        -- comes from the caller; hence "NC"
    do  { kind <- case expectedKindInCtxt ctxt of
                    Nothing -> newMetaKindVar
                    Just k  -> return k
172 173
          -- The kind is checked by checkValidType, and isn't necessarily
          -- of kind * in a Template Haskell quote eg [t| Maybe |]
174

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

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

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

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

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

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

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


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

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

249 250 251 252
tcClassSigType :: LHsType Name -> TcM Type
tcClassSigType lhs_ty@(L _ hs_ty)
  = addTypeCtxt lhs_ty $
    do { ty <- tcCheckHsTypeAndGen hs_ty liftedTypeKind
253
       ; zonkSigType ty }
254 255 256 257 258 259 260

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

261
tcHsConArgType DataType bty = tcHsOpenType (getBangType bty)
262 263 264 265
  -- 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

266
---------------------------
267 268 269 270 271 272 273 274 275 276 277
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..] ]
278

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

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
295

296
---------------------------
297 298 299 300 301
tcCheckHsTypeAndGen :: HsType Name -> Kind -> TcM Type
-- Input type is HsType, not LhsType; the caller adds the context
-- Typecheck a type signature, and kind-generalise it
-- The result is not necessarily zonked, and has not been checked for validity
tcCheckHsTypeAndGen hs_ty kind
302
  = do { ty  <- tc_hs_type hs_ty (EK kind expectedKindMsg)
303
       ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty)
304
       ; kvs <- zonkTcTypeAndFV ty
305
       ; kvs <- kindGeneralize kvs
306
       ; return (mkForAllTys kvs ty) }
307

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

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

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

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

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

362 363
tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind
  = tc_fun_type ty ty1 ty2 exp_kind
364 365

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

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

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

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

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

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

450 451
       ; finish_tuple hs_ty tup_sort tys exp_kind }

dreixel's avatar
dreixel committed
452

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

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

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

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

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

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


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

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

525
tc_hs_type hs_ty@(HsTyLit (HsNumTy n)) exp_kind
526 527 528 529
  = do { checkExpectedKind hs_ty typeNatKind exp_kind
       ; checkWiredInTyCon typeNatKindCon
       ; return (mkNumLitTy n) }

530
tc_hs_type hs_ty@(HsTyLit (HsStrTy s)) exp_kind
531 532
  = do { checkExpectedKind hs_ty typeSymbolKind exp_kind
       ; checkWiredInTyCon typeSymbolKindCon
533
       ; return (mkStrLitTy s) }
534

thomasw's avatar
thomasw committed
535 536 537 538 539 540 541 542 543

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 }

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

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

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

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

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

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

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

617

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

622 623
tcHsLPredType :: LHsType Name -> TcM PredType
tcHsLPredType pred = tc_lhs_type pred ekConstraint
624 625

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

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

655
           APromotionErr err -> promotionErr name err
656 657

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

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

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

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

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

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

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

723 724
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
725
-}
726 727

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

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

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

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

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

Moreover in instance heads we get forall-types with
785
kind Constraint.
786 787 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

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

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

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

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


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

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

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

910 911
mkKindSigVar :: Name -> TcM KindVar
-- Use the specified name; don't clone it
912
mkKindSigVar n
913 914 915 916 917 918 919
  = do { mb_thing <- tcLookupLcl_maybe n
       ; case mb_thing of
           Just (AThing k)
             | Just kvar <- getTyVar_maybe k
             -> return kvar
           _ -> return $ mkTcTyVar n superKind (SkolemTv False) }

920
kcScopedKindVars :: [Name] -> TcM a -> TcM a