TcHsType.hs 118 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

Richard Eisenberg's avatar
Richard Eisenberg committed
8
{-# LANGUAGE CPP, TupleSections, MultiWayIf, RankNTypes #-}
Ryan Scott's avatar
Ryan Scott committed
9
{-# LANGUAGE ScopedTypeVariables #-}
Ian Lynagh's avatar
Ian Lynagh committed
10

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

        tcHsClsInstType,
Ryan Scott's avatar
Ryan Scott committed
19
        tcHsDeriv, tcDerivStrategy,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
20
        tcHsTypeApp,
21
        UserTypeCtxt(..),
22
23
        tcImplicitTKBndrs, tcImplicitTKBndrsX,
        tcExplicitTKBndrs,
24
        kcExplicitTKBndrs, kcImplicitTKBndrs,
25

26
                -- Type checking type and class decls
27
        kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
28
        tcDataKindSig,
dreixel's avatar
dreixel committed
29

30
31
32
          -- tyvars
        scopeTyVars, scopeTyVars2,

33
34
        -- Kind-checking types
        -- No kind generalisation, no checkValidType
Simon Peyton Jones's avatar
Simon Peyton Jones committed
35
        kcLHsQTyVars, kcLHsTyVarBndrs,
36
37
38
        tcWildCardBinders,
        tcHsLiftedType,   tcHsOpenType,
        tcHsLiftedTypeNC, tcHsOpenTypeNC,
Richard Eisenberg's avatar
Richard Eisenberg committed
39
        tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
40
        tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
41
        solveEqualities, -- useful re-export
batterseapower's avatar
batterseapower committed
42

43
44
45
        typeLevelMode, kindLevelMode,

        kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
46
47
        reportFloatingKvs,

48
        -- Sort-checking kinds
Simon Peyton Jones's avatar
Simon Peyton Jones committed
49
        tcLHsKindSig, badKindSig,
50

51
52
53
        -- Zonking and promoting
        zonkPromoteType,

54
        -- Pattern type signatures
55
        tcHsPatSigType, tcPatSig, funAppCtxt
56
57
58
59
   ) where

#include "HsVersions.h"

60
61
import GhcPrelude

62
import HsSyn
63
import TcRnMonad
64
import TcEvidence
65
66
import TcEnv
import TcMType
67
import TcValidity
68
69
import TcUnify
import TcIface
70
import TcSimplify
71
import TcType
72
import TcHsSyn( zonkSigType )
73
import Inst   ( tcInstTyBinders, tcInstTyBinder )
Simon Peyton Jones's avatar
Simon Peyton Jones committed
74
import TyCoRep( TyBinder(..) )  -- Used in tcDataKindSig
75
import Type
76
import Coercion
dreixel's avatar
dreixel committed
77
import Kind
78
import RdrName( lookupLocalRdrOcc )
79
import Var
80
import VarSet
81
import TyCon
Gergő Érdi's avatar
Gergő Érdi committed
82
import ConLike
83
import DataCon
84
85
import Class
import Name
86
import NameEnv
87
88
import NameSet
import VarEnv
89
90
91
import TysWiredIn
import BasicTypes
import SrcLoc
92
93
import Constants ( mAX_CTUPLE_SIZE )
import ErrUtils( MsgDoc )
94
import Unique
95
import Util
96
import UniqSupply
97
import Outputable
98
import FastString
99
import PrelNames hiding ( wildCardName )
100
import qualified GHC.LanguageExtensions as LangExt
101

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
102
import Maybes
103
import Data.List ( find, mapAccumR )
104
import Control.Monad
105

Austin Seipp's avatar
Austin Seipp committed
106
{-
107
108
109
        ----------------------------
                General notes
        ----------------------------
110

111
112
113
114
115
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.
116

117
118
119
120
121
122
123
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.
124

125
126
Generally, after type-checking, you will want to do validity checking, say
with TcValidity.checkValidType.
127
128
129

Validity checking
~~~~~~~~~~~~~~~~~
130
Some of the validity check could in principle be done by the kind checker,
131
132
133
134
but not all:

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
135
136
  e.g.  type T k = k Int
        type S a = a
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
  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.

157
158
%************************************************************************
%*                                                                      *
159
              Check types AND do validity checking
Austin Seipp's avatar
Austin Seipp committed
160
161
162
*                                                                      *
************************************************************************
-}
163

164
165
166
167
168
169
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"

170
addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
171
172
173
addSigCtxt ctxt hs_ty thing_inside
  = setSrcSpan (getLoc hs_ty) $
    addErrCtxt (pprSigCtxt ctxt hs_ty) $
174
175
    thing_inside

176
pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
177
178
179
180
181
182
183
184
185
186
187
188
189
-- (pprSigCtxt ctxt <extra> <type>)
-- prints    In the type signature for 'f':
--              f :: <type>
-- The <extra> is either empty or "the ambiguity check for"
pprSigCtxt ctxt hs_ty
  | Just n <- isSigMaybe ctxt
  = hang (text "In the type signature:")
       2 (pprPrefixOcc n <+> dcolon <+> ppr hs_ty)

  | otherwise
  = hang (text "In" <+> pprUserTypeCtxt ctxt <> colon)
       2 (ppr hs_ty)

190
tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
191
192
-- This one is used when we have a LHsSigWcType, but in
-- a place where wildards aren't allowed. The renamer has
Gabor Greif's avatar
Gabor Greif committed
193
-- already checked this, so we can simply ignore it.
194
195
tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)

196
197
kcHsSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
kcHsSigType skol_info names (HsIB { hsib_body = hs_ty
198
                                  , hsib_ext = HsIBRn { hsib_vars = sig_vars }})
199
  = addSigCtxt (funsSigCtxt names) hs_ty $
200
    discardResult $
201
    tcImplicitTKBndrs skol_info sig_vars $
202
    tc_lhs_type typeLevelMode hs_ty liftedTypeKind
203
kcHsSigType  _ _ (XHsImplicitBndrs _) = panic "kcHsSigType"
204

205
tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
206
207
-- Does not do validity checking; this must be done outside
-- the recursive class declaration "knot"
208
tcClassSigType skol_info names sig_ty
209
  = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
210
    tc_hs_sig_type_and_gen skol_info sig_ty liftedTypeKind
211

212
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
213
-- Does validity checking
214
-- See Note [Recipe for checking a signature]
215
216
tcHsSigType ctxt sig_ty
  = addSigCtxt ctxt (hsSigType sig_ty) $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
217
218
    do { traceTc "tcHsSigType {" (ppr sig_ty)
       ; kind <- case expectedKindInCtxt ctxt of
219
220
                    AnythingKind -> newMetaKindVar
                    TheKind k    -> return k
221
                    OpenKind     -> newOpenTypeKind
222
223
224
              -- The kind is checked by checkValidType, and isn't necessarily
              -- of kind * in a Template Haskell quote eg [t| Maybe |]

225
          -- Generalise here: see Note [Kind generalisation]
Richard Eisenberg's avatar
Richard Eisenberg committed
226
       ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
227
       ; ty <- if do_kind_gen
228
229
               then tc_hs_sig_type_and_gen skol_info sig_ty kind
               else tc_hs_sig_type         skol_info sig_ty kind
230

231
       ; checkValidType ctxt ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
232
       ; traceTc "end tcHsSigType }" (ppr ty)
233
       ; return ty }
234
235
  where
    skol_info = SigTypeSkol ctxt
236

237
tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
238
239
240
-- Kind-checks/desugars an 'LHsSigType',
--   solve equalities,
--   and then kind-generalizes.
Richard Eisenberg's avatar
Richard Eisenberg committed
241
242
-- This will never emit constraints, as it uses solveEqualities interally.
-- No validity checking, but it does zonk en route to generalization
243
244
tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
                                              = HsIBRn { hsib_vars = sig_vars }
245
246
247
248
                                       , hsib_body = hs_ty }) kind
  = do { (tkvs, ty) <- solveEqualities $
                       tcImplicitTKBndrs skol_info sig_vars $
                       tc_lhs_type typeLevelMode hs_ty kind
249
250
251
         -- NB the call to solveEqualities, which unifies all those
         --    kind variables floating about, immediately prior to
         --    kind generalisation
Richard Eisenberg's avatar
Richard Eisenberg committed
252

253
254
         -- We use the "InKnot" zonker, because this is called
         -- on class method sigs in the knot
255
256
257
       ; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty
       ; kvs <- kindGeneralize ty1
       ; zonkSigType (mkInvForAllTys kvs ty1) }
258

259
tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
260
261

tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
262
263
264
-- Kind-check/desugar a 'LHsSigType', but does not solve
-- the equalities that arise from doing so; instead it may
-- emit kind-equality constraints into the monad
265
-- Zonking, but no validity checking
266
tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars }
267
268
                               , hsib_body = hs_ty }) kind
  = do { (tkvs, ty) <- tcImplicitTKBndrs skol_info sig_vars $
269
                       tc_lhs_type typeLevelMode hs_ty kind
270
271
272
273

          -- need to promote any remaining metavariables; test case:
          -- dependent/should_fail/T14066e.
       ; zonkPromoteType (mkSpecForAllTys tkvs ty) }
274

275
tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
batterseapower's avatar
batterseapower committed
276

277
-----------------
Ryan Scott's avatar
Ryan Scott committed
278
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
279
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
280
-- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
281
282
-- E.g.    class C (a::*) (b::k->k)
--         data T a b = ... deriving( C Int )
283
--    returns ([k], C, [k, Int], [k->k])
284
tcHsDeriv hs_ty
285
  = do { cls_kind <- newMetaKindVar
286
287
288
289
                    -- 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
290
               tc_hs_sig_type_and_gen (SigTypeSkol DerivClauseCtxt) hs_ty cls_kind
291
       ; cls_kind <- zonkTcType cls_kind
292
       ; let (tvs, pred) = splitForAllTys ty
293
       ; let (args, _) = splitFunTys cls_kind
294
       ; case getClassPredTys_maybe pred of
Ryan Scott's avatar
Ryan Scott committed
295
           Just (cls, tys) -> return (tvs, (cls, tys, args))
296
           Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
297

Ryan Scott's avatar
Ryan Scott committed
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
-- | Typecheck something within the context of a deriving strategy.
-- This is of particular importance when the deriving strategy is @via@.
-- For instance:
--
-- @
-- deriving via (S a) instance C (T a)
-- @
--
-- We need to typecheck @S a@, and moreover, we need to extend the tyvar
-- environment with @a@ before typechecking @C (T a)@, since @S a@ quantified
-- the type variable @a@.
tcDerivStrategy
  :: forall a.
     UserTypeCtxt
  -> Maybe (DerivStrategy GhcRn) -- ^ The deriving strategy
  -> TcM ([TyVar], a) -- ^ The thing to typecheck within the context of the
                      -- deriving strategy, which might quantify some type
                      -- variables of its own.
  -> TcM (Maybe (DerivStrategy GhcTc), [TyVar], a)
     -- ^ The typechecked deriving strategy, all quantified tyvars, and
     -- the payload of the typechecked thing.
tcDerivStrategy user_ctxt mds thing_inside
  = case mds of
      Nothing -> boring_case Nothing
      Just ds -> do (ds', tvs, thing) <- tc_deriv_strategy ds
                    pure (Just ds', tvs, thing)
  where
    tc_deriv_strategy :: DerivStrategy GhcRn
                      -> TcM (DerivStrategy GhcTc, [TyVar], a)
    tc_deriv_strategy StockStrategy    = boring_case StockStrategy
    tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy
    tc_deriv_strategy NewtypeStrategy  = boring_case NewtypeStrategy
    tc_deriv_strategy (ViaStrategy ty) = do
      cls_kind <- newMetaKindVar
      ty' <- checkNoErrs $
             tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) ty cls_kind
      let (via_tvs, via_pred) = splitForAllTys ty'
      tcExtendTyVarEnv via_tvs $ do
        (thing_tvs, thing) <- thing_inside
        pure (ViaStrategy via_pred, via_tvs ++ thing_tvs, thing)

    boring_case :: mds -> TcM (mds, [TyVar], a)
    boring_case mds = do
      (thing_tvs, thing) <- thing_inside
      pure (mds, thing_tvs, thing)

344
tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
345
                -> LHsSigType GhcRn
346
347
                -> TcM ([TyVar], ThetaType, Class, [Type])
-- Like tcHsSigType, but for a class instance declaration
348
349
tcHsClsInstType user_ctxt hs_inst_ty
  = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
350
    do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
351
352
       ; checkValidInstance user_ctxt hs_inst_ty inst_ty }

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
353
354
----------------------------------------------
-- | Type-check a visible type application
355
tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
356
-- See Note [Recipe for checking a signature] in TcHsType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
357
tcHsTypeApp wc_ty kind
358
  | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
359
  = do { ty <- tcWildCardBindersX newWildTyVar Nothing sig_wcs $ \ _ ->
360
               tcCheckLHsType hs_ty kind
361
       ; ty <- zonkPromoteType ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
362
363
364
365
366
       ; 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.
367
tcHsTypeApp (XHsWildCardBndrs _) _ = panic "tcHsTypeApp"
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
368

Austin Seipp's avatar
Austin Seipp committed
369
370
371
{-
************************************************************************
*                                                                      *
372
            The main kind checker: no validity checks here
Richard Eisenberg's avatar
Richard Eisenberg committed
373
374
*                                                                      *
************************************************************************
375
376

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

dreixel's avatar
dreixel committed
379
---------------------------
380
tcHsOpenType, tcHsLiftedType,
381
  tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
382
383
-- Used for type signatures
-- Do not do validity checking
384
385
386
tcHsOpenType ty   = addTypeCtxt ty $ tcHsOpenTypeNC ty
tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty

387
tcHsOpenTypeNC   ty = do { ek <- newOpenTypeKind
388
389
                         ; tc_lhs_type typeLevelMode ty ek }
tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
390
391

-- Like tcHsType, but takes an expected kind
392
tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
393
tcCheckLHsType hs_ty exp_kind
394
  = addTypeCtxt hs_ty $
395
    tc_lhs_type typeLevelMode hs_ty exp_kind
396

397
tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
398
-- Called from outside: set the context
399
tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
dreixel's avatar
dreixel committed
400

Richard Eisenberg's avatar
Richard Eisenberg committed
401
402
403
404
405
406
407
-- Like tcLHsType, but use it in a context where type synonyms and type families
-- do not need to be saturated, like in a GHCi :kind call
tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty)
  where
    mode = allowUnsaturated typeLevelMode

408
---------------------------
409
-- | Should we generalise the kind of this type signature?
Richard Eisenberg's avatar
Richard Eisenberg committed
410
-- We *should* generalise if the type is closed
411
-- or if NoMonoLocalBinds is set. Otherwise, nope.
412
-- See Note [Kind generalisation plan]
413
decideKindGeneralisationPlan :: LHsSigType GhcRn -> TcM Bool
414
415
decideKindGeneralisationPlan sig_ty@(HsIB { hsib_ext
                                            = HsIBRn { hsib_closed = closed } })
416
  = do { mono_locals <- xoptM LangExt.MonoLocalBinds
Richard Eisenberg's avatar
Richard Eisenberg committed
417
       ; let should_gen = not mono_locals || closed
418
       ; traceTc "decideKindGeneralisationPlan"
Richard Eisenberg's avatar
Richard Eisenberg committed
419
           (ppr sig_ty $$ text "should gen?" <+> ppr should_gen)
420
       ; return should_gen }
421
422
decideKindGeneralisationPlan(XHsImplicitBndrs _)
  = panic "decideKindGeneralisationPlan"
423

424
425
426
427
428
429
430
431
432
{- Note [Kind generalisation plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When should we do kind-generalisation for user-written type signature?
Answer: we use the same rule as for value bindings:

 * We always kind-generalise if the type signature is closed
 * Additionally, we attempt to generalise if we have NoMonoLocalBinds

Trac #13337 shows the problem if we kind-generalise an open type (i.e.
433
one that mentions in-scope type variable
434
435
436
437
438
439
440
441
442
443
444
  foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
      => proxy a -> String
  foo _ = case eqT :: Maybe (k :~: Type) of
            Nothing   -> ...
            Just Refl -> case eqT :: Maybe (a :~: Int) of ...

In the expression type sig on the last line, we have (a :: k)
but (Int :: Type).  Since (:~:) is kind-homogeneous, this requires
k ~ *, which is true in the Refl branch of the outer case.

That equality will be solved if we allow it to float out to the
445
implication constraint for the Refl match, but not not if we aggressively
446
447
448
449
450
451
attempt to solve all equalities the moment they occur; that is, when
checking (Maybe (a :~: Int)).   (NB: solveEqualities fails unless it
solves all the kind equalities, which is the right thing at top level.)

So here the right thing is simply not to do kind generalisation!

452
453
454
455
456
457
458
459
460
461
462
463
************************************************************************
*                                                                      *
      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
464
-}
465

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
466
467
468
469
-- | Info about the context in which we're checking a type. Currently,
-- differentiates only between types and kinds, but this will likely
-- grow, at least to include the distinction between patterns and
-- not-patterns.
Richard Eisenberg's avatar
Richard Eisenberg committed
470
471
472
data TcTyMode
  = TcTyMode { mode_level :: TypeOrKind
             , mode_unsat :: Bool        -- True <=> allow unsaturated type families
473
             }
Richard Eisenberg's avatar
Richard Eisenberg committed
474
475
 -- The mode_unsat field is solely so that type families/synonyms can be unsaturated
 -- in GHCi :kind calls
476
477

typeLevelMode :: TcTyMode
Richard Eisenberg's avatar
Richard Eisenberg committed
478
typeLevelMode = TcTyMode { mode_level = TypeLevel, mode_unsat = False }
479
480

kindLevelMode :: TcTyMode
Richard Eisenberg's avatar
Richard Eisenberg committed
481
482
483
484
kindLevelMode = TcTyMode { mode_level = KindLevel, mode_unsat = False }

allowUnsaturated :: TcTyMode -> TcTyMode
allowUnsaturated mode = mode { mode_unsat = True }
485
486
487
488
489

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
490
491
492
instance Outputable TcTyMode where
  ppr = ppr . mode_level

493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
{-
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
511
again. This is done in calls to tcInstTyBinders.
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536

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.
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553

Note [The tcType invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
If    tc_ty = tc_hs_type hs_ty exp_kind
then
      typeKind tc_ty = exp_kind
without any zonking needed.  The reason for this is that in
tcInferApps we see (F ty), and we kind-check 'ty' with an
expected-kind coming from F.  Then, to make the resulting application
well kinded --- see Note [Ensure well-kinded types] in TcType --- we
need the kind-checked 'ty' to have exactly the kind that F expects,
with no funny zonking nonsense in between.

The tcType invariant also applies to checkExpectedKind: if
    (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
then
    typeKind tc_ty = exp_ki
554
-}
555

556
------------------------------------------
557
558
559
-- | Check and desugar a type, returning the core type and its
-- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
-- level.
560
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
561
562
tc_infer_lhs_type mode (L span ty)
  = setSrcSpan span $
563
564
    do { (ty', kind) <- tc_infer_hs_type mode ty
       ; return (ty', kind) }
565
566
567

-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
568
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
569
570
tc_infer_hs_type mode (HsParTy _ t)          = tc_infer_lhs_type mode t
tc_infer_hs_type mode (HsTyVar _ _ (L _ tv)) = tcTyVar mode tv
571

572
tc_infer_hs_type mode (HsAppTy _ ty1 ty2)
573
574
575
576
577
578
579
580
581
  = do { let (hs_fun_ty, hs_arg_tys) = splitHsAppTys ty1 [ty2]
       ; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty
         -- A worry: what if fun_kind needs zoonking?
         -- We used to zonk it here, but that got fun_ty and fun_kind
         -- out of sync (see the precondition to tcTyApps), which caused
         -- Trac #14873.  So I'm now zonking in tcTyVar, and not here.
         -- Is that enough?  Seems so, but I can't see how to be certain.
       ; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_arg_tys }

582
tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs)
583
584
585
  | not (hs_op `hasKey` funTyConKey)
  = do { (op, op_kind) <- tcTyVar mode hs_op
         -- See "A worry" in the HsApp case
586
587
       ; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind
                       [lhs, rhs] }
588

589
tc_infer_hs_type mode (HsKindSig _ ty sig)
590
  = do { sig' <- tcLHsKindSig KindSigCtxt sig
591
                 -- We must typecheck the kind signature, and solve all
592
593
                 -- its equalities etc; from this point on we may do
                 -- things like instantiate its foralls, so it needs
Richard Eisenberg's avatar
Richard Eisenberg committed
594
                 -- to be fully determined (Trac #14904)
595
       ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
596
597
       ; ty' <- tc_lhs_type mode ty sig'
       ; return (ty', sig') }
598

599
600
601
602
603
604
-- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
-- the splice location to the typechecker. Here we skip over it in order to have
-- the same kind inferred for a given expression whether it was produced from
-- splices or not.
--
-- See Note [Delaying modFinalizers in untyped splices].
605
tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
606
  = tc_infer_hs_type mode ty
607

608
609
tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
tc_infer_hs_type _    (XHsType (NHsCoreTy ty))  = return (ty, typeKind ty)
610
611
612
613
614
tc_infer_hs_type mode other_ty
  = do { kv <- newMetaKindVar
       ; ty' <- tc_hs_type mode other_ty kv
       ; return (ty', kv) }

615
------------------------------------------
616
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
617
tc_lhs_type mode (L span ty) exp_kind
618
  = setSrcSpan span $
619
    tc_hs_type mode ty exp_kind
620

621
------------------------------------------
622
623
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
            -> TcM TcType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
624
625
tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
  TypeLevel ->
626
627
628
629
    do { arg_k <- newOpenTypeKind
       ; res_k <- newOpenTypeKind
       ; ty1' <- tc_lhs_type mode ty1 arg_k
       ; ty2' <- tc_lhs_type mode ty2 res_k
630
631
       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
                           liftedTypeKind exp_kind }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
632
633
634
  KindLevel ->  -- no representation polymorphism in kinds. yet.
    do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
       ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
635
636
       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
                           liftedTypeKind exp_kind }
637

638
------------------------------------------
639
tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
640
641
642
-- See Note [The tcType invariant]
-- See Note [Bidirectional type checking]

643
644
645
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 _ bang _) _
646
647
    -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
    -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
648
649
650
651
652
653
654
655
656
    -- bangs are invalid, so fail. (#7210, #14761)
    = do { let bangError err = failWith $
                 text "Unexpected" <+> text err <+> text "annotation:" <+> ppr ty $$
                 text err <+> text "annotation cannot appear nested inside a type"
         ; case bang of
             HsSrcBang _ SrcUnpack _           -> bangError "UNPACK"
             HsSrcBang _ SrcNoUnpack _         -> bangError "NOUNPACK"
             HsSrcBang _ NoSrcUnpack SrcLazy   -> bangError "laziness"
             HsSrcBang _ _ _                   -> bangError "strictness" }
657
tc_hs_type _ ty@(HsRecTy {})      _
658
      -- Record types (which only show up temporarily in constructor
659
      -- signatures) should have been removed by now
660
    = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
661

662
663
664
665
666
-- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType'.
-- Here we get rid of it and add the finalizers to the global environment
-- while capturing the local environment.
--
-- See Note [Delaying modFinalizers in untyped splices].
667
tc_hs_type mode (HsSpliceTy _ (HsSpliced _ mod_finalizers (HsSplicedTy ty)))
668
669
670
671
           exp_kind
  = do addModFinalizersWithLclEnv mod_finalizers
       tc_hs_type mode ty exp_kind

672
673
-- This should never happen; type splices are expanded by the renamer
tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
674
  = failWithTc (text "Unexpected type splice:" <+> ppr ty)
675

676
---------- Functions and applications
677
tc_hs_type mode (HsFunTy _ ty1 ty2) exp_kind
678
  = tc_fun_type mode ty1 ty2 exp_kind
679

680
tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
681
  | op `hasKey` funTyConKey
682
  = tc_fun_type mode ty1 ty2 exp_kind
683
684

--------- Foralls
685
686
687
tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
  = do { (tvs', ty') <- tcExplicitTKBndrs (ForAllSkol (ppr forall)) hs_tvs $
                        tc_lhs_type mode ty exp_kind
688
    -- Do not kind-generalise here!  See Note [Kind generalisation]
689
    -- Why exp_kind?  See Note [Body kind of HsForAllTy]
690
691
       ; let bndrs      = mkTyVarBinders Specified tvs'
       ; return (mkForAllTys bndrs ty') }
692

693
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
694
695
696
697
  | null (unLoc ctxt)
  = tc_lhs_type mode ty exp_kind

  | otherwise
698
  = do { ctxt' <- tc_hs_context mode ctxt
699
700
701
702

         -- See Note [Body kind of a HsQualTy]
       ; ty' <- if isConstraintKind exp_kind
                then tc_lhs_type mode ty constraintKind
703
704
705
                else do { ek <- newOpenTypeKind
                                -- The body kind (result of the function)
                                -- can be * or #, hence newOpenTypeKind
706
707
                        ; ty' <- tc_lhs_type mode ty ek
                        ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
708
709

       ; return (mkPhiTy ctxt' ty') }
710
711

--------- Lists, arrays, and tuples
712
tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
713
  = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
714
       ; checkWiredInTyCon listTyCon
715
       ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
716

dreixel's avatar
dreixel committed
717
-- See Note [Distinguishing tuple kinds] in HsTypes
718
-- See Note [Inferring tuple kinds]
719
tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
720
     -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
721
  | Just tup_sort <- tupKindSort_maybe exp_kind
722
  = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
723
    tc_tuple rn_ty mode tup_sort hs_tys exp_kind
dreixel's avatar
dreixel committed
724
  | otherwise
Austin Seipp's avatar
Austin Seipp committed
725
  = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
726
727
       ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
       ; kinds <- mapM zonkTcType kinds
728
729
730
731
732
733
           -- 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)
734
735
736
               = case [ (k,s) | k <- kinds
                              , Just s <- [tupKindSort_maybe k] ] of
                    ((k,s) : _) -> (k,s)
737
                    [] -> (liftedTypeKind, BoxedTuple)
738
739
         -- In the [] case, it's not clear what the kind is, so guess *

740
       ; tys' <- sequence [ setSrcSpan loc $
741
742
                            checkExpectedKind hs_ty ty kind arg_kind
                          | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
743

744
       ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
745

dreixel's avatar
dreixel committed
746

747
tc_hs_type mode rn_ty@(HsTupleTy _ hs_tup_sort tys) exp_kind
748
  = tc_tuple rn_ty mode tup_sort tys exp_kind
749
750
751
752
753
754
755
  where
    tup_sort = case hs_tup_sort of  -- Fourth case dealt with above
                  HsUnboxedTuple    -> UnboxedTuple
                  HsBoxedTuple      -> BoxedTuple
                  HsConstraintTuple -> ConstraintTuple
                  _                 -> panic "tc_hs_type HsTupleTy"

756
tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
757
  = do { let arity = length hs_tys
758
759
       ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
       ; tau_tys   <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
760
       ; let arg_reps = map getRuntimeRepFromKind arg_kinds
Richard Eisenberg's avatar
Richard Eisenberg committed
761
             arg_tys  = arg_reps ++ tau_tys
762
763
       ; checkExpectedKind rn_ty
                           (mkTyConApp (sumTyCon arity) arg_tys)
Richard Eisenberg's avatar
Richard Eisenberg committed
764
765
                           (unboxedSumKind arg_reps)
                           exp_kind
766
       }
dreixel's avatar
dreixel committed
767

768
--------- Promoted lists and tuples
769
tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
770
  = do { tks <- mapM (tc_infer_lhs_type mode) tys
771
       ; (taus', kind) <- unifyKinds tys tks
772
       ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
773
       ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
774
  where
775
776
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
777

778
tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
779
780
781
782
783
784
  -- 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
785
             tup_k      = mkTyConApp kind_con ks
786
       ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
787
788
  where
    arity = length tys
789
790

--------- Constraint types
791
tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
792
793
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; ty' <- tc_lhs_type mode ty liftedTypeKind
794
       ; let n' = mkStrLitTy $ hsIPNameFS n
795
       ; ipClass <- tcLookupClass ipClassName
796
       ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
797
798
           constraintKind exp_kind }

799
800
801
802
803
tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
  -- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't have to
  -- handle it in 'coreView' and 'tcView'.
  = checkExpectedKind rn_ty liftedTypeKind liftedTypeKind exp_kind

804
--------- Literals
805
tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
806
  = do { checkWiredInTyCon typeNatKindCon
807
       ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
808

809
tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
810
  = do { checkWiredInTyCon typeSymbolKindCon
811
       ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
812
813
814
815
816
817
818

--------- 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
819
tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
820
821

tc_hs_type _ (HsWildCardTy wc) exp_kind
822
823
  = do { wc_ty <- tcWildCardOcc wc exp_kind
       ; return (mkNakedCastTy wc_ty (mkTcNomReflCo exp_kind))
824
825
826
         -- Take care here! Even though the coercion is Refl,
         -- we still need it to establish Note [The tcType invariant]
       }
827

828
tcWildCardOcc :: HsWildCardInfo -> Kind -> TcM TcType
829
830
831
tcWildCardOcc wc_info exp_kind
  = do { wc_tv <- tcLookupTyVar (wildCardName wc_info)
          -- The wildcard's kind should be an un-filled-in meta tyvar
832
833
       ; checkExpectedKind (HsWildCardTy wc_info) (mkTyVarTy wc_tv)
                           (tyVarKind wc_tv) exp_kind }
834

835
836
---------------------------
-- | Call 'tc_infer_hs_type' and check its result against an expected kind.
837
tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
Simon Peyton Jones's avatar
Simon Peyton Jones committed
838
839
840
tc_infer_hs_type_ek mode hs_ty ek
  = do { (ty, k) <- tc_infer_hs_type mode hs_ty
       ; checkExpectedKind hs_ty ty k ek }
thomasw's avatar
thomasw committed
841

842
---------------------------
843
tupKindSort_maybe :: TcKind -> Maybe TupleSort
844
tupKindSort_maybe k
Simon Peyton Jones's avatar
Simon Peyton Jones committed
845
  | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
Ben Gamari's avatar
Ben Gamari committed
846
  | Just k'      <- tcView k            = tupKindSort_maybe k'
847
848
  | isConstraintKind k = Just ConstraintTuple
  | isLiftedTypeKind k = Just BoxedTuple
849
850
  | otherwise          = Nothing

851
852
tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
tc_tuple rn_ty mode tup_sort tys exp_kind
853
854
  = do { arg_kinds <- case tup_sort of
           BoxedTuple      -> return (nOfThem arity liftedTypeKind)
855
           UnboxedTuple    -> mapM (\_ -> newOpenTypeKind) tys
856
857
           ConstraintTuple -> return (nOfThem arity constraintKind)
       ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
858
       ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
dreixel's avatar
dreixel committed
859
  where
860
861
    arity   = length tys

862
863
finish_tuple :: HsType GhcRn
             -> TupleSort
864
865
866
867
             -> [TcType]    -- ^ argument types
             -> [TcKind]    -- ^ of these kinds
             -> TcKind      -- ^ expected kind of the whole tuple
             -> TcM TcType
868
finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
869
870
  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
       ; let arg_tys  = case tup_sort of
871
                   -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
Richard Eisenberg's avatar
Richard Eisenberg committed
872
                 UnboxedTuple    -> tau_reps ++ tau_tys
873
874
                 BoxedTuple      -> tau_tys
                 ConstraintTuple -> tau_tys
875
       ; tycon <- case tup_sort of
876
877
878
879
880
881
882
883
           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)
884
       ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
885
  where
886
    arity = length tau_tys
887
    tau_reps = map getRuntimeRepFromKind tau_kinds
888
    res_kind = case tup_sort of
Richard Eisenberg's avatar
Richard Eisenberg committed
889
                 UnboxedTuple    -> unboxedTupleKind tau_reps
890
891
                 BoxedTuple      -> liftedTypeKind
                 ConstraintTuple -> constraintKind
892

893
894
bigConstraintTuple :: Arity -> MsgDoc
bigConstraintTuple arity
895
896
897
  = hang (text "Constraint tuple arity too large:" <+> int arity
          <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
       2 (text "Instead, use a nested tuple")
898

899
---------------------------
900
901
902
903
904
905
-- | Apply a type of a given kind to a list of arguments. This instantiates
-- invisible parameters as necessary. Always consumes all the arguments,
-- using matchExpectedFunKind as necessary.
-- 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.
906
tcInferApps :: TcTyMode
907
            -> Maybe (VarEnv Kind)  -- ^ Possibly, kind info (see above)
908
            -> LHsType GhcRn        -- ^ Function (for printing only)
909
910
            -> TcType               -- ^ Function (could be knot-tied)
            -> TcKind               -- ^ Function kind (zonked)
911
            -> [LHsType GhcRn]      -- ^ Args
912
            -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
913
914
915
916
-- Precondition: typeKind fun_ty = fun_ki
--    Reason: we will return a type application like (fun_ty arg1 ... argn),
--            and that type must be well-kinded
--            See Note [The tcType invariant]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
917
tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
Simon Peyton Jones's avatar
Simon Peyton Jones committed
918
919
920
921
  = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
       ; stuff <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
       ; traceTc "tcInferApps }" empty
       ; return stuff }
922
  where