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

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 35
        tcHsContext, tcLHsPredType, tcInferApps, tcInferArgs,
        solveEqualities, -- useful re-export
batterseapower's avatar
batterseapower committed
36

37
        kindGeneralize,
38

39
        -- Sort-checking kinds
40
        tcLHsKindSig,
41

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

#include "HsVersions.h"

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

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

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

95 96 97 98 99
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.
100

101 102 103 104 105 106 107
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.
108

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

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

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

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

148 149 150 151 152 153
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"

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

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

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

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

188
tcClassSigType :: [Located Name] -> LHsSigType GhcRn -> TcM Type
189 190 191 192
-- 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
193
    tc_hs_sig_type_and_gen sig_ty liftedTypeKind
194

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

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

212 213 214
       ; checkValidType ctxt ty
       ; return ty }

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

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

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

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

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

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

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

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

317
tcHsOpenTypeNC   ty = do { ek <- newOpenTypeKind
318 319
                         ; tc_lhs_type typeLevelMode ty ek }
tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
320 321

-- Like tcHsType, but takes an expected kind
322
tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM Type
323
tcCheckLHsType hs_ty exp_kind
324
  = addTypeCtxt hs_ty $
325
    tc_lhs_type typeLevelMode hs_ty exp_kind
326

327
tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
328
-- Called from outside: set the context
329
tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
dreixel's avatar
dreixel committed
330

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

344 345 346 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
{- 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!

372 373 374 375 376 377 378 379 380 381 382 383
************************************************************************
*                                                                      *
      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
384
-}
385

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
386 387 388 389 390
-- | 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
391 392 393 394 395 396 397 398 399 400 401 402 403
  = 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
404 405 406
instance Outputable TcTyMode where
  ppr = ppr . mode_level

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 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
{-
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.
-}
452

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

-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
465
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
Alan Zimmerman's avatar
Alan Zimmerman committed
466
tc_infer_hs_type mode (HsTyVar _ (L _ tv)) = tcTyVar mode tv
467 468 469 470 471 472 473 474 475 476 477 478 479 480 481
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') }
482 483 484 485 486 487 488 489
-- 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
490 491 492 493 494 495 496
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) }

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

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

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

534 535 536 537 538 539 540 541 542 543 544 545
-- 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

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

550 551 552
---------- Functions and applications
tc_hs_type mode (HsFunTy ty1 ty2) exp_kind
  = tc_fun_type mode ty1 ty2 exp_kind
553

554
tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
555
  | op `hasKey` funTyConKey
556
  = tc_fun_type mode ty1 ty2 exp_kind
557 558

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

569
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
570 571 572 573
  | null (unLoc ctxt)
  = tc_lhs_type mode ty exp_kind

  | otherwise
574
  = do { ctxt' <- tc_hs_context mode ctxt
575 576 577 578

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

       ; return (mkPhiTy ctxt' ty') }
586 587 588 589

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

593 594 595
tc_hs_type mode (HsPArrTy elt_ty) exp_kind
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
596
       ; checkWiredInTyCon parrTyCon
597
       ; checkExpectedKind (mkPArrTy tau_ty) liftedTypeKind exp_kind }
598

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

622 623 624
       ; tys' <- sequence [ setSrcSpan loc $
                            checkExpectedKind ty kind arg_kind
                          | ((L loc _),ty,kind) <- zip3 hs_tys tys kinds ]
625

626
       ; finish_tuple tup_sort tys' (map (const arg_kind) tys') exp_kind }
627

dreixel's avatar
dreixel committed
628

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

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

649
--------- Promoted lists and tuples
Alan Zimmerman's avatar
Alan Zimmerman committed
650
tc_hs_type mode (HsExplicitListTy _ _k tys) exp_kind
651 652 653 654
  = 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 }
655
  where
656 657
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
658

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

--------- Constraint types
672
tc_hs_type mode (HsIParamTy (L _ n) ty) exp_kind
673 674
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; ty' <- tc_lhs_type mode ty liftedTypeKind
675
       ; let n' = mkStrLitTy $ hsIPNameFS n
676
       ; ipClass <- tcLookupClass ipClassName
677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705
       ; 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
706 707
  = do { wc_tv <- tcWildCardOcc wc exp_kind
       ; return (mkTyVarTy wc_tv) }
708 709 710 711 712

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

713
tcWildCardOcc :: HsWildCardInfo GhcRn -> Kind -> TcM TcTyVar
714 715 716 717 718 719 720
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 }

721 722
---------------------------
-- | Call 'tc_infer_hs_type' and check its result against an expected kind.
723
tc_infer_hs_type_ek :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
724 725 726
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
727

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

737
tc_tuple :: TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
738 739 740
tc_tuple mode tup_sort tys exp_kind
  = do { arg_kinds <- case tup_sort of
           BoxedTuple      -> return (nOfThem arity liftedTypeKind)
741
           UnboxedTuple    -> mapM (\_ -> newOpenTypeKind) tys
742 743 744
           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
745
  where
746 747 748 749 750 751 752 753 754 755
    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
756
                   -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
Richard Eisenberg's avatar
Richard Eisenberg committed
757
                 UnboxedTuple    -> tau_reps ++ tau_tys
758 759
                 BoxedTuple      -> tau_tys
                 ConstraintTuple -> tau_tys
760
       ; tycon <- case tup_sort of
761 762 763 764 765 766 767 768
           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)
769
       ; checkExpectedKind (mkTyConApp tycon arg_tys) res_kind exp_kind }
770
  where
771
    arity = length tau_tys
Richard Eisenberg's avatar
Richard Eisenberg committed
772
    tau_reps = map (getRuntimeRepFromKind "finish_tuple") tau_kinds
773
    res_kind = case tup_sort of
Richard Eisenberg's avatar
Richard Eisenberg committed
774
                 UnboxedTuple    -> unboxedTupleKind tau_reps
775 776
                 BoxedTuple      -> liftedTypeKind
                 ConstraintTuple -> constraintKind
777

778 779
bigConstraintTuple :: Arity -> MsgDoc
bigConstraintTuple arity
780 781 782
  = hang (text "Constraint tuple arity too large:" <+> int arity
          <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
       2 (text "Instead, use a nested tuple")
783

784
---------------------------
785 786 787
-- | 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.
788 789
-- Never calls 'matchExpectedFunKind'; when the kind runs out of binders,
-- this stops processing.
790 791 792 793
-- 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
794 795 796 797
-- the visible ones. Used only when typechecking type/data family patterns
-- (where we need to instantiate all remaining invisible parameters; for
-- example, consider @type family F :: k where F = Int; F = Maybe@. We
-- need to instantiate the @k@.)
798 799
tcInferArgs :: Outputable fun
            => fun                      -- ^ the function
800
            -> [TyConBinder]            -- ^ function kind's binders
801
            -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
802 803
            -> [LHsType GhcRn]          -- ^ args
            -> TcM (TCvSubst, [TyBinder], [TcType], [LHsType GhcRn], Int)
804 805
               -- ^ (instantiating subst, un-insted leftover binders,
               --   typechecked args, untypechecked args, n)
806 807 808
tcInferArgs fun tc_binders mb_kind_info args
  = do { let binders = tyConBindersTyBinders tc_binders  -- UGH!
       ; (subst, leftover_binders, args', leftovers, n)
809
           <- tc_infer_args typeLevelMode fun binders mb_kind_info args 1
810
        -- now, we need to instantiate any remaining invisible arguments
811
       ; let (invis_bndrs, other_binders) = break isVisibleBinder leftover_binders
812 813 814 815
       ; (subst', invis_args)
           <- tcInstBindersX subst mb_kind_info invis_bndrs
       ; return ( subst'
                , other_binders
Simon Peyton Jones's avatar
Simon Peyton Jones committed
816
                , args' `chkAppend` invis_args
817 818 819 820 821 822 823
                , 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
824
              -> [TyBinder]               -- ^ function kind's binders (zonked)
825
              -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
826
              -> [LHsType GhcRn]          -- ^ args
827
              -> Int                      -- ^ number to start arg counter at
828
              -> TcM (TCvSubst, [TyBinder], [TcType], [LHsType GhcRn], Int)
829
tc_infer_args mode orig_ty binders mb_kind_info orig_args n0
Simon Peyton Jones's avatar
Simon Peyton Jones committed
830
  = go emptyTCvSubst binders orig_args n0 []
831
  where
832 833
    go subst binders []   n acc
      = return ( subst, binders, reverse acc, [], n )
834 835 836 837
    -- when we call this when checking type family patterns, we really
    -- do want to instantiate all invisible arguments. During other
    -- typechecking, we don't.

838 839 840 841 842
    go subst (binder:binders) all_args@(arg:args) n acc
      | isInvisibleBinder binder
      = do { traceTc "tc_infer_args (invis)" (ppr binder)
           ; (subst', arg') <- tcInstBinderX mb_kind_info subst binder
           ; go subst' binders all_args n (arg' : acc) }
843

844 845
      | otherwise
      = do { traceTc "tc_infer_args (vis)" (ppr binder $$ ppr arg)
846
           ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
847 848 849
                     tc_lhs_type mode arg (substTyUnchecked subst $
                                           tyBinderType binder)
           ; let subst' = extendTvSubstBinder subst binder arg'
850
           ; go subst' binders args (n+1) (arg' : acc) }
851

852 853
    go subst [] all_args n acc
      = return (subst, [], reverse acc, all_args, n)
854

855
-- | Applies a type to a list of arguments.
856 857 858 859
-- Always consumes all the arguments, using 'matchExpectedFunKind' as
-- necessary. If you wish to apply a type to a list of HsTypes, this is
-- your function.
-- Used for type-checking types only.
860
tcInferApps :: Outputable fun
861 862 863 864
            => TcTyMode
            -> fun                  -- ^ Function (for printing only)
            -> TcType               -- ^ Function (could be knot-tied)
            -> TcKind               -- ^ Function kind (zonked)
865
            -> [LHsType GhcRn]      -- ^ Args
866
            -> TcM (TcType, TcKind) -- ^ (f args, result kind)
867
tcInferApps mode orig_ty ty ki args = go ty ki args 1
868
  where
869 870
    go fun fun_kind []   _ = return (fun, fun_kind)
    go fun fun_kind args n
871 872 873 874