TcHsType.hs 95.2 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 #-}
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
        tcHsSigType, tcHsSigWcType,
14 15
        tcHsPartialSigType,
        funsSigCtxt, addSigCtxt, pprSigCtxt,
16 17 18

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

23
                -- Type checking type and class decls
24
        kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
25
        tcDataKindSig,
dreixel's avatar
dreixel committed
26

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

37 38 39
        typeLevelMode, kindLevelMode,

        kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
40

41
        -- Sort-checking kinds
42
        tcLHsKindSig,
43

44
        -- Pattern type signatures
45
        tcHsPatSigType, tcPatSig, funAppCtxt
46 47 48 49
   ) where

#include "HsVersions.h"

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
88
import Maybes
89
import Data.List ( partition, zipWith4 )
90
import Control.Monad
91

Austin Seipp's avatar
Austin Seipp committed
92
{-
93 94 95
        ----------------------------
                General notes
        ----------------------------
96

97 98 99 100 101
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.
102

103 104 105 106 107 108 109
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.
110

111 112
Generally, after type-checking, you will want to do validity checking, say
with TcValidity.checkValidType.
113 114 115

Validity checking
~~~~~~~~~~~~~~~~~
116
Some of the validity check could in principle be done by the kind checker,
117 118 119 120
but not all:

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

143 144
%************************************************************************
%*                                                                      *
145
              Check types AND do validity checking
Austin Seipp's avatar
Austin Seipp committed
146 147 148
*                                                                      *
************************************************************************
-}
149

150 151 152 153 154 155
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"

156
addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
157 158 159
addSigCtxt ctxt hs_ty thing_inside
  = setSrcSpan (getLoc hs_ty) $
    addErrCtxt (pprSigCtxt ctxt hs_ty) $
160 161
    thing_inside

162
pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
163 164 165 166 167 168 169 170 171 172 173 174 175
-- (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)

176
tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
177 178
-- 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
179
-- already checked this, so we can simply ignore it.
180 181
tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)

182
kcHsSigType :: [Located Name] -> LHsSigType GhcRn -> TcM ()
Alan Zimmerman's avatar
Alan Zimmerman committed
183
kcHsSigType names (HsIB { hsib_body = hs_ty
184
                        , hsib_vars = sig_vars })
185
  = addSigCtxt (funsSigCtxt names) hs_ty $
186 187 188
    discardResult $
    tcImplicitTKBndrsType sig_vars $
    tc_lhs_type typeLevelMode hs_ty liftedTypeKind
189

190
tcClassSigType :: [Located Name] -> LHsSigType GhcRn -> TcM Type
191 192 193 194
-- 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) $
Richard Eisenberg's avatar
Richard Eisenberg committed
195
    tc_hs_sig_type_and_gen sig_ty liftedTypeKind
196

197
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
198 199 200 201
-- Does validity checking
tcHsSigType ctxt sig_ty
  = addSigCtxt ctxt (hsSigType sig_ty) $
    do { kind <- case expectedKindInCtxt ctxt of
202 203
                    AnythingKind -> newMetaKindVar
                    TheKind k    -> return k
204
                    OpenKind     -> newOpenTypeKind
205 206 207
              -- The kind is checked by checkValidType, and isn't necessarily
              -- of kind * in a Template Haskell quote eg [t| Maybe |]

208
          -- Generalise here: see Note [Kind generalisation]
Richard Eisenberg's avatar
Richard Eisenberg committed
209
       ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
210
       ; ty <- if do_kind_gen
Richard Eisenberg's avatar
Richard Eisenberg committed
211 212
               then tc_hs_sig_type_and_gen sig_ty kind
               else tc_hs_sig_type         sig_ty kind >>= zonkTcType
213

214 215 216
       ; checkValidType ctxt ty
       ; return ty }

217
tc_hs_sig_type_and_gen :: LHsSigType GhcRn -> Kind -> TcM Type
218 219 220
-- Kind-checks/desugars an 'LHsSigType',
--   solve equalities,
--   and then kind-generalizes.
Richard Eisenberg's avatar
Richard Eisenberg committed
221 222
-- This will never emit constraints, as it uses solveEqualities interally.
-- No validity checking, but it does zonk en route to generalization
223 224 225 226 227 228
tc_hs_sig_type_and_gen hs_ty kind
  = do { ty <- solveEqualities $
               tc_hs_sig_type hs_ty kind
         -- 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
229 230
       ; kindGeneralizeType ty }

231
tc_hs_sig_type :: LHsSigType GhcRn -> Kind -> TcM Type
232 233 234
-- 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
Richard Eisenberg's avatar
Richard Eisenberg committed
235
-- No zonking or validity checking
236 237 238
tc_hs_sig_type (HsIB { hsib_vars = sig_vars
                     , hsib_body = hs_ty }) kind
  = do { (tkvs, ty) <- tcImplicitTKBndrsType sig_vars $
239
                       tc_lhs_type typeLevelMode hs_ty kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
240
       ; return (mkSpecForAllTys tkvs ty) }
batterseapower's avatar
batterseapower committed
241

242
-----------------
243
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
244
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
245
-- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
246 247
-- E.g.    class C (a::*) (b::k->k)
--         data T a b = ... deriving( C Int )
248
--    returns ([k], C, [k, Int], [k->k])
249
tcHsDeriv hs_ty
250
  = do { cls_kind <- newMetaKindVar
251 252 253 254
                    -- 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
Richard Eisenberg's avatar
Richard Eisenberg committed
255
               tc_hs_sig_type_and_gen hs_ty cls_kind
256
       ; cls_kind <- zonkTcType cls_kind
257
       ; let (tvs, pred) = splitForAllTys ty
258
       ; let (args, _) = splitFunTys cls_kind
259
       ; case getClassPredTys_maybe pred of
260
           Just (cls, tys) -> return (tvs, cls, tys, args)
261
           Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
262

263
tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
264
                -> LHsSigType GhcRn
265 266
                -> TcM ([TyVar], ThetaType, Class, [Type])
-- Like tcHsSigType, but for a class instance declaration
267 268
tcHsClsInstType user_ctxt hs_inst_ty
  = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
Richard Eisenberg's avatar
Richard Eisenberg committed
269
    do { inst_ty <- tc_hs_sig_type_and_gen hs_inst_ty constraintKind
270 271
       ; checkValidInstance user_ctxt hs_inst_ty inst_ty }

272
-- Used for 'VECTORISE [SCALAR] instance' declarations
273
tcHsVectInst :: LHsSigType GhcRn -> TcM (Class, [Type])
274
tcHsVectInst ty
275 276
  | let hs_cls_ty = hsSigType ty
  , Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe hs_cls_ty
277
    -- Ignoring the binders looks pretty dodgy to me
278
  = do { (cls, cls_kind) <- tcClass cls_name
279
       ; (applied_class, _res_kind)
280
           <- tcTyApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
281 282 283 284
       ; 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) }
285
  | otherwise
286
  = failWithTc $ text "Malformed instance type"
287

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
288 289
----------------------------------------------
-- | Type-check a visible type application
290
tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
291
tcHsTypeApp wc_ty kind
292
  | HsWC { hswc_wcs = sig_wcs, hswc_body = hs_ty } <- wc_ty
Richard Eisenberg's avatar
Richard Eisenberg committed
293
  = do { ty <- tcWildCardBindersX newWildTyVar sig_wcs $ \ _ ->
294
               tcCheckLHsType hs_ty kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
295 296 297 298 299 300 301
       ; 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
302 303 304
{-
************************************************************************
*                                                                      *
305
            The main kind checker: no validity checks here
Richard Eisenberg's avatar
Richard Eisenberg committed
306 307
*                                                                      *
************************************************************************
308 309

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

dreixel's avatar
dreixel committed
312
---------------------------
313
tcHsOpenType, tcHsLiftedType,
314
  tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> 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
tcHsOpenTypeNC   ty = do { ek <- newOpenTypeKind
321 322
                         ; tc_lhs_type typeLevelMode ty ek }
tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
323 324

-- Like tcHsType, but takes an expected kind
325
tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
326
tcCheckLHsType hs_ty exp_kind
327
  = addTypeCtxt hs_ty $
328
    tc_lhs_type typeLevelMode hs_ty exp_kind
329

330
tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
331
-- 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
-- | Should we generalise the kind of this type signature?
Richard Eisenberg's avatar
Richard Eisenberg committed
336
-- We *should* generalise if the type is closed
337
-- or if NoMonoLocalBinds is set. Otherwise, nope.
338
-- See Note [Kind generalisation plan]
339
decideKindGeneralisationPlan :: LHsSigType GhcRn -> TcM Bool
Richard Eisenberg's avatar
Richard Eisenberg committed
340
decideKindGeneralisationPlan sig_ty@(HsIB { hsib_closed = closed })
341
  = do { mono_locals <- xoptM LangExt.MonoLocalBinds
Richard Eisenberg's avatar
Richard Eisenberg committed
342
       ; let should_gen = not mono_locals || closed
343
       ; traceTc "decideKindGeneralisationPlan"
Richard Eisenberg's avatar
Richard Eisenberg committed
344
           (ppr sig_ty $$ text "should gen?" <+> ppr should_gen)
345 346
       ; return should_gen }

347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374
{- 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.
one that mentions in-scope tpe variable
  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
implication constraint for the Refl match, bnot not if we aggressively
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!

375 376 377 378 379 380 381 382 383 384 385 386
************************************************************************
*                                                                      *
      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
387
-}
388

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
389 390 391 392 393
-- | 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.
newtype TcTyMode
394 395 396 397 398 399 400 401 402 403 404 405 406
  = TcTyMode { mode_level :: TypeOrKind  -- True <=> type, False <=> kind
             }

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 }

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
407 408 409
instance Outputable TcTyMode where
  ppr = ppr . mode_level

410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427
{-
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
428
again. This is done in calls to tcInstBinders.
429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454

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.
-}
455

456
------------------------------------------
457 458 459
-- | Check and desugar a type, returning the core type and its
-- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
-- level.
460
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
461 462
tc_infer_lhs_type mode (L span ty)
  = setSrcSpan span $
463 464
    do { (ty', kind) <- tc_infer_hs_type mode ty
       ; return (ty', kind) }
465 466 467

-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
468
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
Alan Zimmerman's avatar
Alan Zimmerman committed
469
tc_infer_hs_type mode (HsTyVar _ (L _ tv)) = tcTyVar mode tv
470 471 472 473
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
474
       ; tcTyApps mode fun_ty fun_ty' fun_kind' arg_tys }
475
tc_infer_hs_type mode (HsParTy t)     = tc_infer_lhs_type mode t
476
tc_infer_hs_type mode (HsOpTy lhs (L loc_op op) rhs)
477 478 479
  | not (op `hasKey` funTyConKey)
  = do { (op', op_kind) <- tcTyVar mode op
       ; op_kind' <- zonkTcType op_kind
480
       ; tcTyApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
481 482 483 484
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') }
485 486 487 488 489 490 491 492
-- 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].
tc_infer_hs_type mode (HsSpliceTy (HsSpliced _ (HsSplicedTy ty)) _)
  = tc_infer_hs_type mode ty
493 494 495 496 497 498 499
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) }

500
------------------------------------------
501
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
502
tc_lhs_type mode (L span ty) exp_kind
503
  = setSrcSpan span $
504 505
    do { ty' <- tc_hs_type mode ty exp_kind
       ; return ty' }
506

507
------------------------------------------
508 509
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
            -> TcM TcType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
510 511
tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
  TypeLevel ->
512 513 514 515
    do { arg_k <- newOpenTypeKind
       ; res_k <- newOpenTypeKind
       ; ty1' <- tc_lhs_type mode ty1 arg_k
       ; ty2' <- tc_lhs_type mode ty2 res_k
516
       ; checkExpectedKind (HsFunTy ty1 ty2) (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
517 518 519
  KindLevel ->  -- no representation polymorphism in kinds. yet.
    do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
       ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
520
       ; checkExpectedKind (HsFunTy ty1 ty2) (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
521

522
------------------------------------------
523
-- See also Note [Bidirectional type checking]
524
tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
525 526 527
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 {}) _
528 529 530
    -- 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)
531
    = failWithTc (text "Unexpected strictness annotation:" <+> ppr ty)
532
tc_hs_type _ ty@(HsRecTy _)      _
533
      -- Record types (which only show up temporarily in constructor
534
      -- signatures) should have been removed by now
535
    = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
536

537 538 539 540 541 542 543 544 545 546 547 548
-- 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].
tc_hs_type mode (HsSpliceTy (HsSpliced mod_finalizers (HsSplicedTy ty))
                            _
                )
           exp_kind
  = do addModFinalizersWithLclEnv mod_finalizers
       tc_hs_type mode ty exp_kind

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

553 554 555
---------- Functions and applications
tc_hs_type mode (HsFunTy ty1 ty2) exp_kind
  = tc_fun_type mode ty1 ty2 exp_kind
556

557
tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
558
  | op `hasKey` funTyConKey
559
  = tc_fun_type mode ty1 ty2 exp_kind
560 561

--------- Foralls
562
tc_hs_type mode (HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
563
  = fmap fst $
564
    tcExplicitTKBndrs hs_tvs $ \ tvs' ->
565
    -- Do not kind-generalise here!  See Note [Kind generalisation]
566
    -- Why exp_kind?  See Note [Body kind of HsForAllTy]
567 568
    do { ty' <- tc_lhs_type mode ty exp_kind
       ; let bound_vars = allBoundVariables ty'
Simon Peyton Jones's avatar
Simon Peyton Jones committed
569
             bndrs      = mkTyVarBinders Specified tvs'
570
       ; return (mkForAllTys bndrs ty', bound_vars) }
571

572
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
573 574 575 576
  | null (unLoc ctxt)
  = tc_lhs_type mode ty exp_kind

  | otherwise
577
  = do { ctxt' <- tc_hs_context mode ctxt
578 579 580 581

         -- See Note [Body kind of a HsQualTy]
       ; ty' <- if isConstraintKind exp_kind
                then tc_lhs_type mode ty constraintKind
582 583 584
                else do { ek <- newOpenTypeKind
                                -- The body kind (result of the function)
                                -- can be * or #, hence newOpenTypeKind
585 586
                        ; ty' <- tc_lhs_type mode ty ek
                        ; checkExpectedKind (unLoc ty) ty' liftedTypeKind exp_kind }
587 588

       ; return (mkPhiTy ctxt' ty') }
589 590

--------- Lists, arrays, and tuples
591
tc_hs_type mode rn_ty@(HsListTy elt_ty) exp_kind
592
  = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
593
       ; checkWiredInTyCon listTyCon
594
       ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
595

596
tc_hs_type mode rn_ty@(HsPArrTy elt_ty) exp_kind
597 598
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
599
       ; checkWiredInTyCon parrTyCon
600
       ; checkExpectedKind rn_ty (mkPArrTy tau_ty) liftedTypeKind exp_kind }
601

dreixel's avatar
dreixel committed
602
-- See Note [Distinguishing tuple kinds] in HsTypes
603
-- See Note [Inferring tuple kinds]
604
tc_hs_type mode rn_ty@(HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
605
     -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
606
  | Just tup_sort <- tupKindSort_maybe exp_kind
607
  = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
608
    tc_tuple rn_ty mode tup_sort hs_tys exp_kind
dreixel's avatar
dreixel committed
609
  | otherwise
Austin Seipp's avatar
Austin Seipp committed
610
  = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
611 612
       ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
       ; kinds <- mapM zonkTcType kinds
613 614 615 616 617 618
           -- 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)
619 620 621
               = case [ (k,s) | k <- kinds
                              , Just s <- [tupKindSort_maybe k] ] of
                    ((k,s) : _) -> (k,s)
622
                    [] -> (liftedTypeKind, BoxedTuple)
623 624
         -- In the [] case, it's not clear what the kind is, so guess *

625
       ; tys' <- sequence [ setSrcSpan loc $
626 627
                            checkExpectedKind hs_ty ty kind arg_kind
                          | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
628

629
       ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
630

dreixel's avatar
dreixel committed
631

632 633
tc_hs_type mode rn_ty@(HsTupleTy hs_tup_sort tys) exp_kind
  = tc_tuple rn_ty mode tup_sort tys exp_kind
634 635 636 637 638 639 640
  where
    tup_sort = case hs_tup_sort of  -- Fourth case dealt with above
                  HsUnboxedTuple    -> UnboxedTuple
                  HsBoxedTuple      -> BoxedTuple
                  HsConstraintTuple -> ConstraintTuple
                  _                 -> panic "tc_hs_type HsTupleTy"

641
tc_hs_type mode rn_ty@(HsSumTy hs_tys) exp_kind
642
  = do { let arity = length hs_tys
643 644
       ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
       ; tau_tys   <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
645
       ; let arg_reps = map getRuntimeRepFromKind arg_kinds
Richard Eisenberg's avatar
Richard Eisenberg committed
646
             arg_tys  = arg_reps ++ tau_tys
647 648
       ; checkExpectedKind rn_ty
                           (mkTyConApp (sumTyCon arity) arg_tys)
Richard Eisenberg's avatar
Richard Eisenberg committed
649 650
                           (unboxedSumKind arg_reps)
                           exp_kind
651
       }
dreixel's avatar
dreixel committed
652

653
--------- Promoted lists and tuples
654
tc_hs_type mode rn_ty@(HsExplicitListTy _ _k tys) exp_kind
655
  = do { tks <- mapM (tc_infer_lhs_type mode) tys
656
       ; (taus', kind) <- unifyKinds tys tks
657
       ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
658
       ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
659
  where
660 661
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
662

663
tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
664 665 666 667 668 669
  -- 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
670
             tup_k      = mkTyConApp kind_con ks
671
       ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
672 673
  where
    arity = length tys
674 675

--------- Constraint types
676
tc_hs_type mode rn_ty@(HsIParamTy (L _ n) ty) exp_kind
677 678
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; ty' <- tc_lhs_type mode ty liftedTypeKind
679
       ; let n' = mkStrLitTy $ hsIPNameFS n
680
       ; ipClass <- tcLookupClass ipClassName
681
       ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
682 683
           constraintKind exp_kind }

684
tc_hs_type mode rn_ty@(HsEqTy ty1 ty2) exp_kind
685 686
  = do { (ty1', kind1) <- tc_infer_lhs_type mode ty1
       ; (ty2', kind2) <- tc_infer_lhs_type mode ty2
687
       ; ty2'' <- checkExpectedKind (unLoc ty2) ty2' kind2 kind1
688 689
       ; eq_tc <- tcLookupTyCon eqTyConName
       ; let ty' = mkNakedTyConApp eq_tc [kind1, ty1', ty2'']
690
       ; checkExpectedKind rn_ty ty' constraintKind exp_kind }
691 692

--------- Literals
693
tc_hs_type _ rn_ty@(HsTyLit (HsNumTy _ n)) exp_kind
694
  = do { checkWiredInTyCon typeNatKindCon
695
       ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
696

697
tc_hs_type _ rn_ty@(HsTyLit (HsStrTy _ s)) exp_kind
698
  = do { checkWiredInTyCon typeSymbolKindCon
699
       ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
700 701 702 703 704 705 706 707 708 709

--------- 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
710 711
  = do { wc_tv <- tcWildCardOcc wc exp_kind
       ; return (mkTyVarTy wc_tv) }
712 713 714 715 716

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

717
tcWildCardOcc :: HsWildCardInfo GhcRn -> Kind -> TcM TcTyVar
718 719 720 721 722 723 724
tcWildCardOcc wc_info exp_kind
  = do { wc_tv <- tcLookupTyVar (wildCardName wc_info)
          -- The wildcard's kind should be an un-filled-in meta tyvar
       ; let Just wc_kind_var = tcGetTyVar_maybe (tyVarKind wc_tv)
       ; writeMetaTyVar wc_kind_var exp_kind
       ; return wc_tv }

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

732
---------------------------
733
tupKindSort_maybe :: TcKind -> Maybe TupleSort
734
tupKindSort_maybe k
Simon Peyton Jones's avatar
Simon Peyton Jones committed
735
  | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
Ben Gamari's avatar
Ben Gamari committed
736
  | Just k'      <- tcView k            = tupKindSort_maybe k'
737 738
  | isConstraintKind k = Just ConstraintTuple
  | isLiftedTypeKind k = Just BoxedTuple
739 740
  | otherwise          = Nothing

741 742
tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
tc_tuple rn_ty mode tup_sort tys exp_kind
743 744
  = do { arg_kinds <- case tup_sort of
           BoxedTuple      -> return (nOfThem arity liftedTypeKind)
745
           UnboxedTuple    -> mapM (\_ -> newOpenTypeKind) tys
746 747
           ConstraintTuple -> return (nOfThem arity constraintKind)
       ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
748
       ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
dreixel's avatar
dreixel committed
749
  where
750 751
    arity   = length tys

752 753
finish_tuple :: HsType GhcRn
             -> TupleSort
754 755 756 757
             -> [TcType]    -- ^ argument types
             -> [TcKind]    -- ^ of these kinds
             -> TcKind      -- ^ expected kind of the whole tuple
             -> TcM TcType
758
finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
759 760
  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
       ; let arg_tys  = case tup_sort of
761
                   -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
Richard Eisenberg's avatar
Richard Eisenberg committed
762
                 UnboxedTuple    -> tau_reps ++ tau_tys
763 764
                 BoxedTuple      -> tau_tys
                 ConstraintTuple -> tau_tys
765
       ; tycon <- case tup_sort of
766 767 768 769 770 771 772 773
           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)
774
       ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
775
  where
776
    arity = length tau_tys
777
    tau_reps = map getRuntimeRepFromKind tau_kinds
778
    res_kind = case tup_sort of
Richard Eisenberg's avatar
Richard Eisenberg committed
779
                 UnboxedTuple    -> unboxedTupleKind tau_reps
780 781
                 BoxedTuple      -> liftedTypeKind
                 ConstraintTuple -> constraintKind
782

783 784
bigConstraintTuple :: Arity -> MsgDoc
bigConstraintTuple arity
785 786 787
  = hang (text "Constraint tuple arity too large:" <+> int arity
          <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
       2 (text "Instead, use a nested tuple")
788

789
---------------------------
790 791 792 793 794 795
-- | 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.
796
tcInferApps :: TcTyMode
797
            -> Maybe (VarEnv Kind)  -- ^ Possibly, kind info (see above)
798
            -> LHsType GhcRn        -- ^ Function (for printing only)
799 800
            -> TcType               -- ^ Function (could be knot-tied)
            -> TcKind               -- ^ Function kind (zonked)
801
            -> [LHsType GhcRn]      -- ^ Args
802
            -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
Richard Eisenberg's avatar
Richard Eisenberg committed
803 804 805
tcInferApps mode mb_kind_info orig_ty ty ki args
  = do { traceTc "tcInferApps" (ppr orig_ty $$ ppr args $$ ppr ki)
       ; go [] [] orig_subst ty orig_ki_binders orig_inner_ki args 1 }
806
  where
Richard Eisenberg's avatar
Richard Eisenberg committed
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
    orig_subst                       = mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfType ki
    (orig_ki_binders, orig_inner_ki) = tcSplitPiTys ki

    go :: [LHsType GhcRn] -- already type-checked args, in reverse order, for errors
       -> [TcType]        -- already type-checked args, in reverse order
       -> TCvSubst        -- instantiating substitution
       -> TcType          -- function applied to some args, could be knot-tied
       -> [TyBinder]      -- binders in function kind (both vis. and invis.)
       -> TcKind          -- function kind body (not a Pi-type)
       -> [LHsType GhcRn] -- un-type-checked args
       -> Int             -- the # of the next argument
       -> TcM (TcType, [TcType], TcKind)  -- same as overall return type

      -- no user-written args left. We're done!
    go _acc_hs_args acc_args subst fun ki_binders inner_ki [] _
      = return (fun, reverse acc_args, substTy subst $ mkPiTys ki_binders inner_ki)

      -- The function's kind has a binder. Is it visible or invisible?
    go acc_hs_args acc_args subst fun (ki_binder:ki_binders) inner_ki
       all_args@(arg:args) n
      | isInvisibleBinder ki_binder
        -- It's invisible. Instantiate.
      = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
           ; (subst', arg') <- tcInstBinder mb_kind_info subst ki_binder
           ; go acc_hs_args (arg' : acc_args) subst' (mkNakedAppTy fun arg')
                ki_binders inner_ki all_args n }

      | otherwise
        -- It's visible. Check the next user-written argument
      = do { traceTc "tcInferApps (vis)" (ppr ki_binder $$ ppr arg $$ ppr subst)
837
           ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
Richard Eisenberg's avatar
Richard Eisenberg committed
838