TcHsType.hs 93.1 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, TupleSections, MultiWayIf #-}
Ian Lynagh's avatar
Ian Lynagh committed
9

10
module TcHsType (
11
        -- Type signatures
Alan Zimmerman's avatar
Alan Zimmerman committed
12
        kcHsSigType, tcClassSigType,
13
14
15
16
17
        tcHsSigType, tcHsSigWcType,
        funsSigCtxt, addSigCtxt,

        tcHsClsInstType,
        tcHsDeriv, tcHsVectInst,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
18
        tcHsTypeApp,
19
        UserTypeCtxt(..),
20
        tcImplicitTKBndrs, tcImplicitTKBndrsType, tcHsTyVarBndrs,
21

22
                -- Type checking type and class decls
23
24
        kcLookupKind, kcTyClTyVars, tcTyClTyVars,
        tcHsConArgType, tcDataKindSig,
dreixel's avatar
dreixel committed
25

26
27
28
        -- Kind-checking types
        -- No kind generalisation, no checkValidType
        tcWildCardBinders,
29
        kcHsTyVarBndrs,
30
31
32
        tcHsLiftedType,   tcHsOpenType,
        tcHsLiftedTypeNC, tcHsOpenTypeNC,
        tcLHsType, tcCheckLHsType,
33
34
        tcHsContext, tcLHsPredType, tcInferApps, tcInferArgs,
        solveEqualities, -- useful re-export
batterseapower's avatar
batterseapower committed
35

36
        kindGeneralize,
37

38
        -- Sort-checking kinds
39
        tcLHsKind,
40

41
        -- Pattern type signatures
42
        tcHsPatSigType, tcPatSig, funAppCtxt
43
44
45
46
   ) where

#include "HsVersions.h"

47
import HsSyn
48
import TcRnMonad
49
import TcEvidence
50
51
import TcEnv
import TcMType
52
import TcValidity
53
54
import TcUnify
import TcIface
55
import TcSimplify ( solveEqualities )
56
import TcType
57
import Type
dreixel's avatar
dreixel committed
58
import Kind
59
import RdrName( lookupLocalRdrOcc )
60
import Var
61
import VarSet
62
import TyCon
Gergő Érdi's avatar
Gergő Érdi committed
63
import ConLike
64
import DataCon
65
import TysPrim ( tYPE )
66
67
import Class
import Name
68
import NameEnv
69
70
import NameSet
import VarEnv
71
72
73
import TysWiredIn
import BasicTypes
import SrcLoc
74
75
import Constants ( mAX_CTUPLE_SIZE )
import ErrUtils( MsgDoc )
76
import Unique
77
import Util
78
import UniqSupply
79
import Outputable
80
import FastString
81
82
import PrelNames hiding ( wildCardName )
import Pair
83
import qualified GHC.LanguageExtensions as LangExt
84

85
import Data.Maybe
86
import Data.List ( partition )
87
import Control.Monad
88

Austin Seipp's avatar
Austin Seipp committed
89
{-
90
91
92
        ----------------------------
                General notes
        ----------------------------
93

94
95
96
97
98
Unlike with expressions, type-checking types both does some checking and
desugars at the same time. This is necessary because we often want to perform
equality checks on the types right away, and it would be incredibly painful
to do this on un-desugared types. Luckily, desugared types are close enough
to HsTypes to make the error messages sane.
99

100
101
102
103
104
105
106
During type-checking, we perform as little validity checking as possible.
This is because some type-checking is done in a mutually-recursive knot, and
if we look too closely at the tycons, we'll loop. This is why we always must
use mkNakedTyConApp and mkNakedAppTys, etc., which never look at a tycon.
The mkNamed... functions don't uphold Type invariants, but zonkTcTypeToType
will repair this for us. Note that zonkTcType *is* safe within a knot, and
can be done repeatedly with no ill effect: it just squeezes out metavariables.
107

108
109
Generally, after type-checking, you will want to do validity checking, say
with TcValidity.checkValidType.
110
111
112

Validity checking
~~~~~~~~~~~~~~~~~
113
Some of the validity check could in principle be done by the kind checker,
114
115
116
117
but not all:

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
118
119
  e.g.  type T k = k Int
        type S a = a
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
  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.

140
141
%************************************************************************
%*                                                                      *
142
              Check types AND do validity checking
Austin Seipp's avatar
Austin Seipp committed
143
144
145
*                                                                      *
************************************************************************
-}
146

147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
funsSigCtxt :: [Located Name] -> UserTypeCtxt
-- Returns FunSigCtxt, with no redundant-context-reporting,
-- form a list of located names
funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
funsSigCtxt []              = panic "funSigCtxt"

addSigCtxt :: UserTypeCtxt -> LHsType Name -> TcM a -> TcM a
addSigCtxt ctxt sig_ty thing_inside
  = setSrcSpan (getLoc sig_ty) $
    addErrCtxt (pprSigCtxt ctxt empty (ppr sig_ty)) $
    thing_inside

tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType Name -> TcM Type
-- This one is used when we have a LHsSigWcType, but in
-- a place where wildards aren't allowed. The renamer has
-- alrady checked this, so we can simply ignore it.
tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)

Alan Zimmerman's avatar
Alan Zimmerman committed
165
166
kcHsSigType :: [Located Name] -> LHsSigType Name -> TcM ()
kcHsSigType names (HsIB { hsib_body = hs_ty
167
                        , hsib_vars = sig_vars })
168
  = addSigCtxt (funsSigCtxt names) hs_ty $
169
170
171
    discardResult $
    tcImplicitTKBndrsType sig_vars $
    tc_lhs_type typeLevelMode hs_ty liftedTypeKind
172
173
174
175
176
177

tcClassSigType :: [Located Name] -> LHsSigType Name -> TcM Type
-- Does not do validity checking; this must be done outside
-- the recursive class declaration "knot"
tcClassSigType names sig_ty
  = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
178
179
    do { ty <- tc_hs_sig_type sig_ty liftedTypeKind
       ; kindGeneralizeType ty }
180
181
182
183
184
185

tcHsSigType :: UserTypeCtxt -> LHsSigType Name -> TcM Type
-- Does validity checking
tcHsSigType ctxt sig_ty
  = addSigCtxt ctxt (hsSigType sig_ty) $
    do { kind <- case expectedKindInCtxt ctxt of
186
187
188
189
                    AnythingKind -> newMetaKindVar
                    TheKind k    -> return k
                    OpenKind     -> do { lev <- newFlexiTyVarTy levityTy
                                       ; return $ tYPE lev }
190
191
192
193
              -- The kind is checked by checkValidType, and isn't necessarily
              -- of kind * in a Template Haskell quote eg [t| Maybe |]

       ; ty <- tc_hs_sig_type sig_ty kind
194
195
          -- Generalise here: see Note [Kind generalisation]
       ; ty <- maybeKindGeneralizeType ty -- also zonks
196
197
198
199
       ; checkValidType ctxt ty
       ; return ty }

tc_hs_sig_type :: LHsSigType Name -> Kind -> TcM Type
200
-- Does not do validity checking or zonking
201
tc_hs_sig_type (HsIB { hsib_body = hs_ty
202
203
204
205
                     , hsib_vars = sig_vars }) kind
  = do { (tkvs, ty) <- solveEqualities $
                       tcImplicitTKBndrsType sig_vars $
                       tc_lhs_type typeLevelMode hs_ty kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
206
       ; return (mkSpecForAllTys tkvs ty) }
batterseapower's avatar
batterseapower committed
207

208
-----------------
209
tcHsDeriv :: LHsSigType Name -> TcM ([TyVar], Class, [Type], Kind)
210
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
211
212
213
214
215
216
217
218
-- 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
219
220
221
222
223
224
225
                    -- always safe to kind-generalize, because there
                    -- can be no covars in an outer scope
       ; ty <- checkNoErrs $
                 -- avoid redundant error report with "illegal deriving", below
               tc_hs_sig_type hs_ty (mkFunTy arg_kind constraintKind)
       ; ty <- kindGeneralizeType ty  -- also zonks
       ; arg_kind <- zonkTcType arg_kind
226
227
       ; let (tvs, pred) = splitForAllTys ty
       ; case getClassPredTys_maybe pred of
228
           Just (cls, tys) -> return (tvs, cls, tys, arg_kind)
229
           Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) }
230

231
232
233
234
235
236
tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
                -> LHsSigType Name
                -> TcM ([TyVar], ThetaType, Class, [Type])
-- Like tcHsSigType, but for a class instance declaration
-- The significant difference is that we expect a /constraint/
-- not a /type/ for the bit after the '=>'.
237
tcHsClsInstType user_ctxt hs_inst_ty@(HsIB { hsib_vars = sig_vars
238
239
240
241
                                           , hsib_body = hs_qual_ty })
    -- An explicit forall in an instance declaration isn't
    -- allowed, so there won't be any HsForAllTy here
  = setSrcSpan (getLoc hs_qual_ty) $
242
243
    do { (tkvs, phi_ty) <- solveEqualities $
                           tcImplicitTKBndrsType sig_vars $
244
                    do { theta    <- tcHsContext cxt
245
246
247
                       ; head_ty' <- tc_lhs_type typeLevelMode
                                                 head_ty constraintKind
                       ; return (mkPhiTy theta head_ty') }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
248
       ; let inst_ty = mkSpecForAllTys tkvs phi_ty
249
       ; inst_ty <- kindGeneralizeType inst_ty
250
       ; inst_ty <- zonkTcType inst_ty
251
       ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
252
253
  where
    (cxt, head_ty) = splitLHsQualTy hs_qual_ty
254

255
256
-- Used for 'VECTORISE [SCALAR] instance' declarations
--
257
tcHsVectInst :: LHsSigType Name -> TcM (Class, [Type])
258
tcHsVectInst ty
259
  | Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe (hsSigType ty)
260
    -- Ignoring the binders looks pretty dodgy to me
261
  = do { (cls, cls_kind) <- tcClass cls_name
262
263
264
265
266
267
       ; (applied_class, _res_kind)
           <- tcInferApps typeLevelMode cls_name (mkClassPred cls []) cls_kind tys
       ; case tcSplitTyConApp_maybe applied_class of
           Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
                               return (cls, args)
           _ -> failWithTc (text "Too many arguments passed to" <+> ppr cls_name) }
268
269
  | otherwise
  = failWithTc $ ptext (sLit "Malformed instance type")
270

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
----------------------------------------------
-- | Type-check a visible type application
tcHsTypeApp :: LHsWcType Name -> Kind -> TcM Type
tcHsTypeApp wc_ty kind
  | HsWC { hswc_wcs = sig_wcs, hswc_ctx = extra, hswc_body = hs_ty } <- wc_ty
  = ASSERT( isNothing extra )  -- handled in RnTypes.rnExtraConstraintWildCard
    tcWildCardBinders sig_wcs $ \ _ ->
    do { ty <- tcCheckLHsType hs_ty kind
       ; ty <- zonkTcType ty
       ; checkValidType TypeAppCtxt ty
       ; return ty }
        -- NB: we don't call emitWildcardHoleConstraints here, because
        -- we want any holes in visible type applications to be used
        -- without fuss. No errors, warnings, extensions, etc.

Austin Seipp's avatar
Austin Seipp committed
286
{-
287
288
289
        These functions are used during knot-tying in
        type and class declarations, when we have to
        separate kind-checking, desugaring, and validity checking
290
291


Austin Seipp's avatar
Austin Seipp committed
292
293
************************************************************************
*                                                                      *
294
            The main kind checker: no validity checks here
295
296
%*                                                                      *
%************************************************************************
297
298

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

301
302
303
304
305
306
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

307
tcHsConArgType DataType bty = tcHsOpenType (getBangType bty)
308
309
310
311
  -- 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

dreixel's avatar
dreixel committed
312
---------------------------
313
314
tcHsOpenType, tcHsLiftedType,
  tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType Name -> TcM TcType
315
316
-- Used for type signatures
-- Do not do validity checking
317
318
319
tcHsOpenType ty   = addTypeCtxt ty $ tcHsOpenTypeNC ty
tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty

320
321
322
tcHsOpenTypeNC   ty = do { ek <- ekOpen
                         ; tc_lhs_type typeLevelMode ty ek }
tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
323
324
325
326

-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType Name -> Kind -> TcM Type
tcCheckLHsType hs_ty exp_kind
327
  = addTypeCtxt hs_ty $
328
    tc_lhs_type typeLevelMode hs_ty exp_kind
329
330
331

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

334
---------------------------
335
336
337
338
339
-- | Should we generalise the kind of this type?
-- We *should* generalise if the type is mentions no scoped type variables
-- or if NoMonoLocalBinds is set. Otherwise, nope.
decideKindGeneralisationPlan :: Type -> TcM Bool
decideKindGeneralisationPlan ty
340
  = do { mono_locals <- xoptM LangExt.MonoLocalBinds
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
       ; in_scope <- getInLocalScope
       ; let fvs        = tyCoVarsOfTypeList ty
             should_gen = not mono_locals || all (not . in_scope . getName) fvs
       ; traceTc "decideKindGeneralisationPlan"
           (vcat [ text "type:" <+> ppr ty
                 , text "ftvs:" <+> ppr fvs
                 , text "should gen?" <+> ppr should_gen ])
       ; return should_gen }

maybeKindGeneralizeType :: TcType -> TcM Type
maybeKindGeneralizeType ty
  = do { should_gen <- decideKindGeneralisationPlan ty
       ; if should_gen
         then kindGeneralizeType ty
         else zonkTcType ty }

Austin Seipp's avatar
Austin Seipp committed
357
{-
358
359
360
361
362
363
364
365
366
367
368
369
************************************************************************
*                                                                      *
      Type-checking modes
*                                                                      *
************************************************************************

The kind-checker is parameterised by a TcTyMode, which contains some
information about where we're checking a type.

The renamer issues errors about what it can. All errors issued here must
concern things that the renamer can't handle.

Austin Seipp's avatar
Austin Seipp committed
370
-}
371

372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
data TcTyMode
  = TcTyMode { mode_level :: TypeOrKind  -- True <=> type, False <=> kind
                                         -- used only for -XNoTypeInType errors
             }

typeLevelMode :: TcTyMode
typeLevelMode = TcTyMode { mode_level = TypeLevel }

kindLevelMode :: TcTyMode
kindLevelMode = TcTyMode { mode_level = KindLevel }

-- switch to kind level
kindLevel :: TcTyMode -> TcTyMode
kindLevel mode = mode { mode_level = KindLevel }

{-
Note [Bidirectional type checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In expressions, whenever we see a polymorphic identifier, say `id`, we are
free to instantiate it with metavariables, knowing that we can always
re-generalize with type-lambdas when necessary. For example:

  rank2 :: (forall a. a -> a) -> ()
  x = rank2 id

When checking the body of `x`, we can instantiate `id` with a metavariable.
Then, when we're checking the application of `rank2`, we notice that we really
need a polymorphic `id`, and then re-generalize over the unconstrained
metavariable.

In types, however, we're not so lucky, because *we cannot re-generalize*!
There is no lambda. So, we must be careful only to instantiate at the last
possible moment, when we're sure we're never going to want the lost polymorphism
again. This is done in calls to tcInstBinders and tcInstBindersX.

To implement this behavior, we use bidirectional type checking, where we
explicitly think about whether we know the kind of the type we're checking
or not. Note that there is a difference between not knowing a kind and
knowing a metavariable kind: the metavariables are TauTvs, and cannot become
forall-quantified kinds. Previously (before dependent types), there were
no higher-rank kinds, and so we could instantiate early and be sure that
no types would have polymorphic kinds, and so we could always assume that
the kind of a type was a fresh metavariable. Not so anymore, thus the
need for two algorithms.

For HsType forms that can never be kind-polymorphic, we implement only the
"down" direction, where we safely assume a metavariable kind. For HsType forms
that *can* be kind-polymorphic, we implement just the "up" (functions with
"infer" in their name) version, as we gain nothing by also implementing the
"down" version.

Note [Future-proofing the type checker]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As discussed in Note [Bidirectional type checking], each HsType form is
handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
are mutually recursive, so that either one can work for any type former.
But, we want to make sure that our pattern-matches are complete. So,
we have a bunch of repetitive code just so that we get warnings if we're
missing any patterns.
-}
432

433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
-- | Check and desugar a type, returning the core type and its
-- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
-- level.
tc_infer_lhs_type :: TcTyMode -> LHsType Name -> TcM (TcType, TcKind)
tc_infer_lhs_type mode (L span ty)
  = setSrcSpan span $
    do { traceTc "tc_infer_lhs_type:" (ppr ty)
       ; tc_infer_hs_type mode ty }

-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
tc_infer_hs_type :: TcTyMode -> HsType Name -> TcM (TcType, TcKind)
tc_infer_hs_type mode (HsTyVar (L _ tv)) = tcTyVar mode tv
tc_infer_hs_type mode (HsAppTy ty1 ty2)
  = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
       ; (fun_ty', fun_kind) <- tc_infer_lhs_type mode fun_ty
       ; fun_kind' <- zonkTcType fun_kind
       ; tcInferApps mode fun_ty fun_ty' fun_kind' arg_tys }
tc_infer_hs_type mode (HsParTy t)     = tc_infer_lhs_type mode t
tc_infer_hs_type mode (HsOpTy lhs (L _ op) rhs)
  | not (op `hasKey` funTyConKey)
  = do { (op', op_kind) <- tcTyVar mode op
       ; op_kind' <- zonkTcType op_kind
       ; tcInferApps mode op op' op_kind' [lhs, rhs] }
tc_infer_hs_type mode (HsKindSig ty sig)
  = do { sig' <- tc_lhs_kind (kindLevel mode) sig
       ; ty' <- tc_lhs_type mode ty sig'
       ; return (ty', sig') }
tc_infer_hs_type mode (HsDocTy ty _) = tc_infer_lhs_type mode ty
tc_infer_hs_type _    (HsCoreTy ty)  = return (ty, typeKind ty)
tc_infer_hs_type mode other_ty
  = do { kv <- newMetaKindVar
       ; ty' <- tc_hs_type mode other_ty kv
       ; return (ty', kv) }

tc_lhs_type :: TcTyMode -> LHsType Name -> TcKind -> TcM TcType
tc_lhs_type mode (L span ty) exp_kind
470
  = setSrcSpan span $
471
    do { traceTc "tc_lhs_type:" (ppr ty $$ ppr exp_kind)
472
       ; tc_hs_type mode ty exp_kind }
473

474
------------------------------------------
475
476
477
478
479
480
481
tc_fun_type :: TcTyMode -> LHsType Name -> LHsType Name -> TcKind -> TcM TcType
tc_fun_type mode ty1 ty2 exp_kind
  = do { arg_lev <- newFlexiTyVarTy levityTy
       ; res_lev <- newFlexiTyVarTy levityTy
       ; ty1' <- tc_lhs_type mode ty1 (tYPE arg_lev)
       ; ty2' <- tc_lhs_type mode ty2 (tYPE res_lev)
       ; checkExpectedKind (mkNakedFunTy ty1' ty2') liftedTypeKind exp_kind }
482

483
------------------------------------------
484
485
486
487
488
-- See also Note [Bidirectional type checking]
tc_hs_type :: TcTyMode -> HsType Name -> TcKind -> TcM TcType
tc_hs_type mode (HsParTy ty)   exp_kind = tc_lhs_type mode ty exp_kind
tc_hs_type mode (HsDocTy ty _) exp_kind = tc_lhs_type mode ty exp_kind
tc_hs_type _ ty@(HsBangTy {}) _
489
490
491
492
    -- 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)
493
tc_hs_type _ ty@(HsRecTy _)      _
494
      -- Record types (which only show up temporarily in constructor
495
      -- signatures) should have been removed by now
Alan Zimmerman's avatar
Alan Zimmerman committed
496
    = failWithTc (ptext (sLit "Record syntax is illegal here:") <+> ppr ty)
497

498
499
500
-- This should never happen; type splices are expanded by the renamer
tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
  = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
501

502
503
504
---------- Functions and applications
tc_hs_type mode (HsFunTy ty1 ty2) exp_kind
  = tc_fun_type mode ty1 ty2 exp_kind
505

506
tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
507
  | op `hasKey` funTyConKey
508
  = tc_fun_type mode ty1 ty2 exp_kind
509
510

--------- Foralls
511
512
513
tc_hs_type mode hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
    -- Do not kind-generalise here.  See Note [Kind generalisation]
  | isConstraintKind exp_kind
514
515
516
  = failWithTc (hang (ptext (sLit "Illegal constraint:")) 2 (ppr hs_ty))

  | otherwise
517
518
  = fmap fst $
    tcHsTyVarBndrs hs_tvs $ \ tvs' ->
519
    -- Do not kind-generalise here!  See Note [Kind generalisation]
520
521
522
    -- Why exp_kind?  See Note [Body kind of forall]
    do { ty' <- tc_lhs_type mode ty exp_kind
       ; let bound_vars = allBoundVariables ty'
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
523
       ; return (mkNakedSpecSigmaTy tvs' [] ty', bound_vars) }
524

525
526
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
  = do { ctxt' <- tc_hs_context mode ctxt
527
       ; ty' <- if null (unLoc ctxt) then  -- Plain forall, no context
528
529
                   tc_lhs_type mode ty exp_kind
                     -- Why exp_kind?  See Note [Body kind of forall]
530
                else
531
                   -- If there is a context, then this forall is really a
532
                   -- _function_, so the kind of the result really is *
533
                   -- The body kind (result of the function) can be * or #, hence ekOpen
534
535
536
537
538
539
540
541
542
                   do { ek <- ekOpen
                      ; ty <- tc_lhs_type mode ty ek
                      ; checkExpectedKind ty liftedTypeKind exp_kind }

       ; return (mkNakedPhiTy ctxt' ty') }

--------- Lists, arrays, and tuples
tc_hs_type mode (HsListTy elt_ty) exp_kind
  = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
543
       ; checkWiredInTyCon listTyCon
544
       ; checkExpectedKind (mkListTy tau_ty) liftedTypeKind exp_kind }
545

546
547
548
tc_hs_type mode (HsPArrTy elt_ty) exp_kind
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
549
       ; checkWiredInTyCon parrTyCon
550
       ; checkExpectedKind (mkPArrTy tau_ty) liftedTypeKind exp_kind }
551

dreixel's avatar
dreixel committed
552
-- See Note [Distinguishing tuple kinds] in HsTypes
553
-- See Note [Inferring tuple kinds]
554
tc_hs_type mode (HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
555
     -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
556
  | Just tup_sort <- tupKindSort_maybe exp_kind
557
  = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
558
    tc_tuple mode tup_sort hs_tys exp_kind
dreixel's avatar
dreixel committed
559
  | otherwise
Austin Seipp's avatar
Austin Seipp committed
560
  = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
561
562
       ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
       ; kinds <- mapM zonkTcType kinds
563
564
565
566
567
568
           -- 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)
569
570
571
               = case [ (k,s) | k <- kinds
                              , Just s <- [tupKindSort_maybe k] ] of
                    ((k,s) : _) -> (k,s)
572
                    [] -> (liftedTypeKind, BoxedTuple)
573
574
         -- In the [] case, it's not clear what the kind is, so guess *

575
576
577
       ; tys' <- sequence [ setSrcSpan loc $
                            checkExpectedKind ty kind arg_kind
                          | ((L loc _),ty,kind) <- zip3 hs_tys tys kinds ]
578

579
       ; finish_tuple tup_sort tys' (map (const arg_kind) tys') exp_kind }
580

dreixel's avatar
dreixel committed
581

582
583
tc_hs_type mode (HsTupleTy hs_tup_sort tys) exp_kind
  = tc_tuple mode tup_sort tys exp_kind
584
585
586
587
588
589
590
  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
591

592
--------- Promoted lists and tuples
593
594
595
596
597
tc_hs_type mode (HsExplicitListTy _k tys) exp_kind
  = do { tks <- mapM (tc_infer_lhs_type mode) tys
       ; (taus', kind) <- unifyKinds tks
       ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
       ; checkExpectedKind ty (mkListTy kind) exp_kind }
598
  where
599
600
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
601

602
tc_hs_type mode (HsExplicitTupleTy _ tys) exp_kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
603
604
605
606
607
608
  -- using newMetaKindVar means that we force instantiations of any polykinded
  -- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
  = do { ks   <- replicateM arity newMetaKindVar
       ; taus <- zipWithM (tc_lhs_type mode) tys ks
       ; let kind_con   = tupleTyCon           Boxed arity
             ty_con     = promotedTupleDataCon Boxed arity
609
             tup_k      = mkTyConApp kind_con ks
610
       ; checkExpectedKind (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
611
612
  where
    arity = length tys
613
614

--------- Constraint types
615
616
617
tc_hs_type mode (HsIParamTy n ty) exp_kind
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; ty' <- tc_lhs_type mode ty liftedTypeKind
618
       ; let n' = mkStrLitTy $ hsIPNameFS n
619
       ; ipClass <- tcLookupClass ipClassName
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
       ; checkExpectedKind (mkClassPred ipClass [n',ty'])
           constraintKind exp_kind }

tc_hs_type mode (HsEqTy ty1 ty2) exp_kind
  = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
       ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
       ; ty2'' <- checkExpectedKind ty2' kind2 kind1
       ; eq_tc <- tcLookupTyCon eqTyConName
       ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
       ; checkExpectedKind ty' constraintKind exp_kind }

--------- Literals
tc_hs_type _ (HsTyLit (HsNumTy _ n)) exp_kind
  = do { checkWiredInTyCon typeNatKindCon
       ; checkExpectedKind (mkNumLitTy n) typeNatKind exp_kind }

tc_hs_type _ (HsTyLit (HsStrTy _ s)) exp_kind
  = do { checkWiredInTyCon typeSymbolKindCon
       ; checkExpectedKind (mkStrLitTy s) typeSymbolKind exp_kind }

--------- Potentially kind-polymorphic types: call the "up" checker
-- See Note [Future-proofing the type checker]
tc_hs_type mode ty@(HsTyVar {})   ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsAppTy {})   ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsOpTy {})    ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsCoreTy {})  ek = tc_infer_hs_type_ek mode ty ek

tc_hs_type _ (HsWildCardTy wc) exp_kind
thomasw's avatar
thomasw committed
649
  = do { let name = wildCardName wc
650
       ; tv <- tcLookupTyVar name
651
652
653
654
655
656
657
658
659
660
661
662
       ; checkExpectedKind (mkTyVarTy tv) (tyVarKind tv) exp_kind }

-- disposed of by renamer
tc_hs_type _ ty@(HsAppsTy {}) _
  = pprPanic "tc_hs_tyep HsAppsTy" (ppr ty)

---------------------------
-- | Call 'tc_infer_hs_type' and check its result against an expected kind.
tc_infer_hs_type_ek :: TcTyMode -> HsType Name -> TcKind -> TcM TcType
tc_infer_hs_type_ek mode ty ek
  = do { (ty', k) <- tc_infer_hs_type mode ty
       ; checkExpectedKind ty' k ek }
thomasw's avatar
thomasw committed
663

664
---------------------------
665
tupKindSort_maybe :: TcKind -> Maybe TupleSort
666
tupKindSort_maybe k
Simon Peyton Jones's avatar
Simon Peyton Jones committed
667
668
  | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
  | Just k'      <- coreView k          = tupKindSort_maybe k'
669
670
  | isConstraintKind k = Just ConstraintTuple
  | isLiftedTypeKind k = Just BoxedTuple
671
672
  | otherwise          = Nothing

673
674
675
676
677
678
679
680
681
tc_tuple :: TcTyMode -> TupleSort -> [LHsType Name] -> TcKind -> TcM TcType
tc_tuple mode tup_sort tys exp_kind
  = do { arg_kinds <- case tup_sort of
           BoxedTuple      -> return (nOfThem arity liftedTypeKind)
           UnboxedTuple    -> do { levs <- newFlexiTyVarTys arity levityTy
                                 ; return $ map tYPE levs }
           ConstraintTuple -> return (nOfThem arity constraintKind)
       ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
       ; finish_tuple tup_sort tau_tys arg_kinds exp_kind }
dreixel's avatar
dreixel committed
682
  where
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
    arity   = length tys

finish_tuple :: TupleSort
             -> [TcType]    -- ^ argument types
             -> [TcKind]    -- ^ of these kinds
             -> TcKind      -- ^ expected kind of the whole tuple
             -> TcM TcType
finish_tuple tup_sort tau_tys tau_kinds exp_kind
  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
       ; let arg_tys  = case tup_sort of
                   -- See also Note [Unboxed tuple levity vars] in TyCon
                 UnboxedTuple    -> map (getLevityFromKind "finish_tuple") tau_kinds
                                    ++ tau_tys
                 BoxedTuple      -> tau_tys
                 ConstraintTuple -> tau_tys
698
       ; tycon <- case tup_sort of
699
700
701
702
703
704
705
706
           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)
707
       ; checkExpectedKind (mkTyConApp tycon arg_tys) res_kind exp_kind }
708
  where
709
    arity = length tau_tys
710
    res_kind = case tup_sort of
711
712
713
                 UnboxedTuple    -> unliftedTypeKind
                 BoxedTuple      -> liftedTypeKind
                 ConstraintTuple -> constraintKind
714

715
716
717
718
719
720
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"))

721
---------------------------
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
-- | Apply a type of a given kind to a list of arguments. This instantiates
-- invisible parameters as necessary. However, it does *not* necessarily
-- apply all the arguments, if the kind runs out of binders.
-- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
-- These kinds should be used to instantiate invisible kind variables;
-- they come from an enclosing class for an associated type/data family.
-- This version will instantiate all invisible arguments left over after
-- the visible ones.
tcInferArgs :: Outputable fun
            => fun                      -- ^ the function
            -> TcKind                   -- ^ function kind (zonked)
            -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
            -> [LHsType Name]           -- ^ args
            -> TcM (TcKind, [TcType], [LHsType Name], Int)
               -- ^ (result kind, typechecked args, untypechecked args, n)
tcInferArgs fun fun_kind mb_kind_info args
  = do { (res_kind, args', leftovers, n)
           <- tc_infer_args typeLevelMode fun fun_kind mb_kind_info args 1
        -- now, we need to instantiate any remaining invisible arguments
       ; let (invis_bndrs, really_res_kind) = splitPiTysInvisible res_kind
       ; (subst, invis_args)
           <- tcInstBindersX emptyTCvSubst mb_kind_info invis_bndrs
       ; return ( substTy subst really_res_kind, args' `chkAppend` invis_args
                , leftovers, n ) }

-- | See comments for 'tcInferArgs'. But this version does not instantiate
-- any remaining invisible arguments.
tc_infer_args :: Outputable fun
              => TcTyMode
              -> fun                      -- ^ the function
              -> TcKind                   -- ^ function kind (zonked)
              -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
              -> [LHsType Name]           -- ^ args
              -> Int                      -- ^ number to start arg counter at
              -> TcM (TcKind, [TcType], [LHsType Name], Int)
tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
  = do { traceTc "tcInferApps" (ppr ki $$ ppr orig_args)
       ; go emptyTCvSubst ki orig_args n0 [] }
  where
    go subst fun_kind []   n acc
      = return ( substTy subst fun_kind, reverse acc, [], n )
    -- when we call this when checking type family patterns, we really
    -- do want to instantiate all invisible arguments. During other
    -- typechecking, we don't.

    go subst fun_kind all_args n acc
      | Just fun_kind' <- coreView fun_kind
      = go subst fun_kind' all_args n acc

      | Just tv <- getTyVar_maybe fun_kind
      , Just fun_kind' <- lookupTyVar subst tv
      = go subst fun_kind' all_args n acc

      | (inv_bndrs, res_k) <- splitPiTysInvisible fun_kind
      , not (null inv_bndrs)
      = do { (subst', args') <- tcInstBindersX subst mb_kind_info inv_bndrs
           ; go subst' res_k all_args n (reverse args' ++ acc) }

      | Just (bndr, res_k) <- splitPiTy_maybe fun_kind
      , arg:args <- all_args  -- this actually has to succeed
      = ASSERT( isVisibleBinder bndr )
        do { let mode' | isNamedBinder bndr = kindLevel mode
                       | otherwise          = mode
           ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
                     tc_lhs_type mode' arg (substTy subst $ binderType bndr)
           ; let subst' = case binderVar_maybe bndr of
                   Just tv -> extendTCvSubst subst tv arg'
                   Nothing -> subst
           ; go subst' res_k args (n+1) (arg' : acc) }
791

792
793
794
795
796
797
798
799
800
801
802
803
804
      | otherwise
      = return (substTy subst fun_kind, reverse acc, all_args, n)

-- | Applies a type to a list of arguments. Always consumes all the
-- arguments.
tcInferApps :: Outputable fun
             => TcTyMode
             -> fun                  -- ^ Function (for printing only)
             -> TcType               -- ^ Function (could be knot-tied)
             -> TcKind               -- ^ Function kind (zonked)
             -> [LHsType Name]       -- ^ Args
             -> TcM (TcType, TcKind) -- ^ (f args, result kind)
tcInferApps mode orig_ty ty ki args = go ty ki args 1
805
  where
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
838
839
840
841
842
843
844
845
846
847
848
849
    go fun fun_kind []   _ = return (fun, fun_kind)
    go fun fun_kind args n
      | Just fun_kind' <- coreView fun_kind
      = go fun fun_kind' args n

      | isPiTy fun_kind
      = do { (res_kind, args', leftover_args, n')
                <- tc_infer_args mode orig_ty fun_kind Nothing args n
           ; go (mkNakedAppTys fun args') res_kind leftover_args n' }

    go fun fun_kind all_args@(arg:args) n
      = do { (co, arg_k, res_k) <- matchExpectedFunKind (length all_args)
                                                        fun fun_kind
           ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
                     tc_lhs_type mode arg arg_k
           ; go (mkNakedAppTy (fun `mkNakedCastTy` co) arg')
                res_k args (n+1) }

---------------------------
-- | This is used to instantiate binders when type-checking *types* only.
-- Precondition: all binders are invisible. See also Note [Bidirectional type checking]
tcInstBinders :: [TyBinder] -> TcM (TCvSubst, [TcType])
tcInstBinders = tcInstBindersX emptyTCvSubst Nothing

-- | This is used to instantiate binders when type-checking *types* only.
-- Precondition: all binders are invisible.
-- The @VarEnv Kind@ gives some known instantiations.
-- See also Note [Bidirectional type checking]
tcInstBindersX :: TCvSubst -> Maybe (VarEnv Kind)
               -> [TyBinder] -> TcM (TCvSubst, [TcType])
tcInstBindersX subst mb_kind_info bndrs
  = do { (subst, args) <- mapAccumLM (tcInstBinderX mb_kind_info) subst bndrs
       ; traceTc "instantiating implicit dependent vars:"
           (vcat $ zipWith (\bndr arg -> ppr bndr <+> text ":=" <+> ppr arg)
                           bndrs args)
       ; return (subst, args) }

-- | Used only in *types*
tcInstBinderX :: Maybe (VarEnv Kind)
              -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
tcInstBinderX mb_kind_info subst binder
  | Just tv <- binderVar_maybe binder
  = case lookup_tv tv of
      Just ki -> return (extendTCvSubst subst tv ki, ki)
850
      Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
851
852
853
854
855
856
857
858
859
860
861
862
863
                    ; return (subst', mkTyVarTy tv') }

     -- This is the *only* constraint currently handled in types.
  | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty
  = do { let origin = TypeEqOrigin { uo_actual   = k1
                                   , uo_expected = k2
                                   , uo_thing    = Nothing }
       ; co <- case role of
                 Nominal          -> unifyKind noThing k1 k2
                 Representational -> emitWantedEq origin KindLevel role k1 k2
                 Phantom          -> pprPanic "tcInstBinderX Phantom" (ppr binder)
       ; arg' <- mk co k1 k2
       ; return (subst, arg') }
864

865
866
867
868
869
870
871
872
  | otherwise
  = do { let (env, tidy_ty) = tidyOpenType emptyTidyEnv substed_ty
       ; addErrTcM (env, text "Illegal constraint in a type:" <+> ppr tidy_ty)

         -- just invent a new variable so that we can continue
       ; u <- newUnique
       ; let name = mkSysTvName u (fsLit "dict")
       ; return (subst, mkTyVarTy $ mkTyVar name substed_ty) }
873

874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
  where
    substed_ty = substTy subst (binderType binder)

    lookup_tv tv = do { env <- mb_kind_info   -- `Maybe` monad
                      ; lookupVarEnv env tv }

      -- handle boxed equality constraints, because it's so easy
    get_pred_tys_maybe ty
      | Just (r, k1, k2) <- getEqPredTys_maybe ty
      = Just (\co _ _ -> return $ mkCoercionTy co, r, k1, k2)
      | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
      = if | tc `hasKey` heqTyConKey
             -> Just (mkHEqBoxTy, Nominal, k1, k2)
           | otherwise
             -> Nothing
      | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
      = if | tc `hasKey` eqTyConKey
             -> Just (mkEqBoxTy, Nominal, k1, k2)
           | tc `hasKey` coercibleTyConKey
             -> Just (mkCoercibleBoxTy, Representational, k1, k2)
           | otherwise
             -> Nothing
      | otherwise
      = Nothing

-------------------------------
-- | This takes @a ~# b@ and returns @a ~~ b@.
mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
-- monadic just for convenience with mkEqBoxTy
mkHEqBoxTy co ty1 ty2
  = return $
    mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
  where k1 = typeKind ty1
        k2 = typeKind ty2

-- | This takes @a ~# b@ and returns @a ~ b@.
mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
mkEqBoxTy co ty1 ty2
  = do { eq_tc <- tcLookupTyCon eqTyConName
       ; let [datacon] = tyConDataCons eq_tc
       ; hetero <- mkHEqBoxTy co ty1 ty2
       ; return $ mkTyConApp (promoteDataCon datacon) [k, ty1, ty2, hetero] }
  where k = typeKind ty1

-- | This takes @a ~R# b@ and returns @Coercible a b@.
mkCoercibleBoxTy :: TcCoercion -> Type -> Type -> TcM Type
-- monadic just for convenience with mkEqBoxTy
mkCoercibleBoxTy co ty1 ty2
  = do { return $
         mkTyConApp (promoteDataCon coercibleDataCon)
                    [k, ty1, ty2, mkCoercionTy co] }
  where k = typeKind ty1


--------------------------
checkExpectedKind :: TcType               -- the type whose kind we're checking
                  -> TcKind               -- the known kind of that type, k
                  -> TcKind               -- the expected kind, exp_kind
                  -> TcM TcType    -- a possibly-inst'ed, casted type :: exp_kind
-- Instantiate a kind (if necessary) and then call unifyType
--      (checkExpectedKind ty act_kind exp_kind)
-- checks that the actual kind act_kind is compatible
--      with the expected kind exp_kind
checkExpectedKind ty act_kind exp_kind
 = do { (ty', act_kind') <- instantiate ty act_kind exp_kind
      ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                  , uo_expected = exp_kind
                                  , uo_thing    = Just $ mkTypeErrorThing ty'
                                  }
      ; co_k <- uType origin KindLevel act_kind' exp_kind
      ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
                                          , ppr exp_kind
                                          , ppr co_k ])
      ; let result_ty = ty' `mkNakedCastTy` co_k
      ; return result_ty }
  where
    -- we need to make sure that both kinds have the same number of implicit
    -- foralls out front. If the actual kind has more, instantiate accordingly.
    -- Otherwise, just pass the type & kind through -- the errors are caught
    -- in unifyType.
    instantiate :: TcType    -- the type
                -> TcKind    -- of this kind
                -> TcKind   -- but expected to be of this one
                -> TcM ( TcType   -- the inst'ed type
                       , TcKind ) -- its new kind
    instantiate ty act_ki exp_ki
      = let (exp_bndrs, _) = splitPiTysInvisible exp_ki in
        instantiateTyN (length exp_bndrs) ty act_ki

-- | Instantiate a type to have at most @n@ invisible arguments.
instantiateTyN :: Int    -- ^ @n@
               -> TcType -- ^ the type
               -> TcKind -- ^ its kind
               -> TcM (TcType, TcKind)   -- ^ The inst'ed type with kind
instantiateTyN n ty ki
  = let (bndrs, inner_ki)            = splitPiTysInvisible ki
        num_to_inst                  = length bndrs - n
           -- NB: splitAt is forgiving with invalid numbers
        (inst_bndrs, leftover_bndrs) = splitAt num_to_inst bndrs
    in
    if num_to_inst <= 0 then return (ty, ki) else
    do { (subst, inst_args) <- tcInstBinders inst_bndrs
       ; let rebuilt_ki = mkForAllTys leftover_bndrs inner_ki
             ki'        = substTy subst rebuilt_ki
       ; return (mkNakedAppTys ty inst_args, ki') }
979

980
---------------------------
981
tcHsContext :: LHsContext Name -> TcM [PredType]
982
tcHsContext = tc_hs_context typeLevelMode
983

984
tcLHsPredType :: LHsType Name -> TcM PredType
985
986
987
988
989
990
991
tcLHsPredType = tc_lhs_pred typeLevelMode

tc_hs_context :: TcTyMode -> LHsContext Name -> TcM [PredType]
tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)

tc_lhs_pred :: TcTyMode -> LHsType Name -> TcM PredType
tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
992
993

---------------------------
994
tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
dreixel's avatar
dreixel committed
995
996
-- See Note [Type checking recursive type and class declarations]
-- in TcTyClsDecls
997
tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
dreixel's avatar
dreixel committed
998
999
1000
  = do { traceTc "lk1" (ppr name)
       ; thing <- tcLookup name
       ; case thing of
1001
1002
           ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)

1003
1004
1005
1006
1007
1008
           ATcTyCon tc_tc -> do { data_kinds <- xoptM LangExt.DataKinds
                                ; unless (isTypeLevel (mode_level mode) ||
                                          data_kinds) $
                                  promotionErr name NoDataKinds
                                ; tc <- get_loopy_tc name tc_tc
                                ; return (mkNakedTyConApp tc [], tyConKind tc_tc) }
1009
1010
1011
1012
                             -- mkNakedTyConApp: see Note [Type-checking inside the knot]
                 -- NB: we really should check if we're at the kind level
                 -- and if the tycon is promotable if -XNoTypeInType is set.
                 -- But this is a terribly large amount of work! Not worth it.
1013

1014
           AGlobal (ATyCon tc)
1015
1016
             -> do { type_in_type <- xoptM LangExt.TypeInType
                   ; data_kinds   <- xoptM LangExt.DataKinds
1017
1018
1019
1020
1021
1022
1023
1024
1025
                   ; unless (isTypeLevel (mode_level mode) ||
                             data_kinds ||
                             isKindTyCon tc) $
                       promotionErr name NoDataKinds
                   ; unless (isTypeLevel (mode_level mode) ||
                             type_in_type ||
                             isLegacyPromotableTyCon tc) $
                       promotionErr name NoTypeInTypeTC
                   ; return (mkTyConApp tc [], tyConKind tc) }
1026

Gergő Érdi's avatar
Gergő Érdi committed
1027
           AGlobal (AConLike (RealDataCon dc))
1028
             -> do { data_kinds <- xoptM LangExt.DataKinds
1029
1030
                   ; unless (data_kinds || specialPromotedDc dc) $
                       promotionErr name NoDataKinds
1031
                   ; type_in_type <- xoptM LangExt.TypeInType
1032
1033
1034
1035
1036
1037
1038
1039
                   ; unless ( type_in_type ||
                              ( isTypeLevel (mode_level mode) &&
                                isLegacyPromotableDataCon dc ) ||
                              ( isKindLevel (mode_level mode) &&
                                specialPromotedDc dc ) ) $
                       promotionErr name NoTypeInTypeDC
                   ; let tc = promoteDataCon dc
                   ; return (mkNakedTyConApp tc [], tyConKind tc) }
1040

1041
           APromotionErr err -> promotionErr name err
1042
1043

           _  -> wrongThingErr "type" thing name }
dreixel's avatar
dreixel committed
1044
  where
1045
1046
1047
1048
1049
1050
    get_loopy_tc :: Name -> TyCon -> TcM TyCon
    -- Return the knot-tied global TyCon if there is one
    -- Otherwise the local TcTyCon; we must be doing kind checking
    -- but we still want to return a TyCon of some sort to use in
    -- error messages
    get_loopy_tc name tc_tc
1051
1052
1053
      = do { env <- getGblEnv
           ; case lookupNameEnv (tcg_type_env env) name of
                Just (ATyCon tc) -> return tc
1054
1055
                _                -> do { traceTc "lk1 (loopy)" (ppr name)
                                       ; return tc_tc } }
1056
1057

tcClass :: Name -> TcM (Class, TcKind)
1058
tcClass cls     -- Must be a class
1059
1060
  = do { thing <- tcLookup cls
       ; case thing of
1061
           ATcTyCon tc -> return (aThingErr "tcClass" cls, tyConKind tc)
1062
           AGlobal (ATyCon tc)
1063
             | Just cls <- tyConClass_maybe tc
1064
1065
1066
1067
1068
1069
1070
1071
1072
             -> 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)
1073

Austin Seipp's avatar
Austin Seipp committed
1074
{-
1075
Note [Type-checking inside the knot]
1076
1077
1078
1079
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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.
1080

1081
BUT the parent TyCon is knot-tied, so we can't look at it yet.
1082
1083

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

1086
  * Hence the use of mkNakedXXX functions. These do *not* enforce
1087
    the invariants (for example that we use (ForAllTy (Anon s) t) rather
1088
    than (TyConApp (->) [s,t])).
1089

1090
1091
1092
1093
1094
1095
  * The zonking functions establish invariants (even zonkTcType, a change from
    previous behaviour). So we must never inspect the result of a
    zonk that might mention a knot-tied TyCon. This is generally OK
    because we zonk *kinds* while kind-checking types. And the TyCons
    in kinds shouldn't be knot-tied, because they come from a previous
    mutually recursive group.
1096
1097
1098

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

1100
1101
This is horribly delicate.  I hate it.  A good example of how
delicate it is can be seen in Trac #7903.
1102
1103
1104
1105
1106
1107

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
1108
unboxed tuple inside a for-all (via CPR analyis; see
1109
1110
1111
typecheck/should_compile/tc170).

Moreover in instance heads we get forall-types with
1112
kind Constraint.
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137

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

1138
   f :: (forall (k:*). forall (t:: k->*) (a:k). t a -> t a) -> Int
1139
1140
1141
1142
1143
1144
   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.

1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
It's tempting to check that the body kind is either * or #. But this is
wrong. For example:

  class C a b
  newtype N = Mk Foo deriving (C a)

We're doing newtype-deriving for C. But notice how `a` isn't in scope in
the predicate `C a`. So we quantify, yielding `forall a. C a` even though
`C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
convenient. Bottom line: don't check for * or # here.
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174

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`.
1175

dreixel's avatar
dreixel committed
1176
1177
1178
1179
1180
1181
1182
1183
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):
1184
      - any unconstrained kind variables are defaulted to (Any *) just
1185
1186
        as in TcHsSyn.
      - there are no mutable type variables because we are
dreixel's avatar
dreixel committed
1187
1188
1189
1190
1191
1192
1193
1194
        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;
1195
and we might then default it to (Any *) when dealing with f's type
dreixel's avatar
dreixel committed
1196
1197
1198
1199
1200
1201
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
1202
  * it cannot fail,
dreixel's avatar
dreixel committed
1203
1204
  * it does no unifications
  * it does no validity checking, except for structural matters, such as
1205
1206
        (a) spurious ! annotations.
        (b) a class used as a type
1207

dreixel's avatar
dreixel committed
1208
1209
1210
1211
1212
1213
1214
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,
1215
as if $(..blah..) :: forall k. k.
dreixel's avatar
dreixel committed
1216
1217
1218

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
1219
variables as we go.  When we encounter the unconstrained kappa, we
1220
want to default it to '*', not to (Any *).
dreixel's avatar
dreixel committed
1221
1222


1223
1224
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Austin Seipp's avatar
Austin Seipp committed
1225
-}
1226

1227
addTypeCtxt :: LHsType Name -> TcM a -> TcM a
1228
1229
1230
        -- 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
1231
1232
1233
  = addErrCtxt doc thing
  where
    doc = ptext (sLit "In the type") <+> quotes (ppr ty)
1234

Austin Seipp's avatar
Austin Seipp committed
1235
1236
1237
{-
************************************************************************
*                                                                      *
1238
                Type-variable binders
1239
1240
1241
1242
1243
1244
1245
1246