TcHsType.hs 126 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 #-}
10
{-# LANGUAGE TypeFamilies #-}
Ian Lynagh's avatar
Ian Lynagh committed
11

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

        tcHsClsInstType,
Ryan Scott's avatar
Ryan Scott committed
20
        tcHsDeriv, tcDerivStrategy,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
21
        tcHsTypeApp,
22
        UserTypeCtxt(..),
23 24 25 26 27
        bindImplicitTKBndrs_Tv, bindImplicitTKBndrs_Skol,
            bindImplicitTKBndrs_Q_Tv, bindImplicitTKBndrs_Q_Skol,
        bindExplicitTKBndrs_Tv, bindExplicitTKBndrs_Skol,
            bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol,
        ContextKind(..),
28

29
                -- Type checking type and class decls
30 31
        kcLookupTcTyCon, bindTyClTyVars,
        etaExpandAlgTyCon, tcbVisibilities,
dreixel's avatar
dreixel committed
32

33
          -- tyvars
34
        zonkAndScopedSort,
35

36 37
        -- Kind-checking types
        -- No kind generalisation, no checkValidType
38
        kcLHsQTyVars,
39 40 41
        tcWildCardBinders,
        tcHsLiftedType,   tcHsOpenType,
        tcHsLiftedTypeNC, tcHsOpenTypeNC,
Richard Eisenberg's avatar
Richard Eisenberg committed
42
        tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
43
        tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
44
        failIfEmitsConstraints,
45
        solveEqualities, -- useful re-export
batterseapower's avatar
batterseapower committed
46

47 48
        typeLevelMode, kindLevelMode,

Simon Peyton Jones's avatar
Simon Peyton Jones committed
49
        kindGeneralize, checkExpectedKind_pp,
50 51
        reportFloatingKvs,

52
        -- Sort-checking kinds
Simon Peyton Jones's avatar
Simon Peyton Jones committed
53
        tcLHsKindSig, badKindSig,
54

55 56 57
        -- Zonking and promoting
        zonkPromoteType,

58
        -- Pattern type signatures
Tobias Dammers's avatar
Tobias Dammers committed
59 60 61 62
        tcHsPatSigType, tcPatSig,

        -- Error messages
        funAppCtxt, addTyConFlavCtxt
63 64 65 66
   ) where

#include "HsVersions.h"

67 68
import GhcPrelude

69
import HsSyn
70
import TcRnMonad
71
import TcEvidence
72 73
import TcEnv
import TcMType
74
import TcValidity
75 76
import TcUnify
import TcIface
77
import TcSimplify
78
import TcHsSyn
Simon Peyton Jones's avatar
Simon Peyton Jones committed
79
import TyCoRep  ( Type(..) )
80
import TcErrors ( reportAllUnsolved )
81
import TcType
Simon Peyton Jones's avatar
Simon Peyton Jones committed
82
import Inst   ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
83
import TyCoRep( TyCoBinder(..), tyCoBinderArgFlag )  -- Used in etaExpandAlgTyCon
84
import Type
My Nguyen's avatar
My Nguyen committed
85
import TysPrim
86
import Coercion
87
import RdrName( lookupLocalRdrOcc )
88
import Var
89
import VarSet
90
import TyCon
cactus's avatar
cactus committed
91
import ConLike
92
import DataCon
93 94
import Class
import Name
95 96
import NameSet
import VarEnv
97 98 99
import TysWiredIn
import BasicTypes
import SrcLoc
100 101
import Constants ( mAX_CTUPLE_SIZE )
import ErrUtils( MsgDoc )
102
import Unique
103
import UniqSet
104
import Util
105
import UniqSupply
106
import Outputable
107
import FastString
108
import PrelNames hiding ( wildCardName )
My Nguyen's avatar
My Nguyen committed
109
import DynFlags ( WarningFlag (Opt_WarnPartialTypeSignatures) )
110
import qualified GHC.LanguageExtensions as LangExt
111

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
112
import Maybes
113
import Data.List ( find )
114
import Control.Monad
115

Austin Seipp's avatar
Austin Seipp committed
116
{-
117 118 119
        ----------------------------
                General notes
        ----------------------------
120

121 122 123 124 125
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.
126

127 128 129
During type-checking, we perform as little validity checking as possible.
Generally, after type-checking, you will want to do validity checking, say
with TcValidity.checkValidType.
130 131 132

Validity checking
~~~~~~~~~~~~~~~~~
133
Some of the validity check could in principle be done by the kind checker,
134 135 136 137
but not all:

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
138 139
  e.g.  type T k = k Int
        type S a = a
140 141 142 143 144 145
  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

146
- Ambiguity checks involve functional dependencies
147 148 149 150 151

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).

152 153
%************************************************************************
%*                                                                      *
154
              Check types AND do validity checking
Austin Seipp's avatar
Austin Seipp committed
155 156 157
*                                                                      *
************************************************************************
-}
158

159 160 161 162 163 164
funsSigCtxt :: [Located Name] -> UserTypeCtxt
-- Returns FunSigCtxt, with no redundant-context-reporting,
-- form a list of located names
funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
funsSigCtxt []              = panic "funSigCtxt"

165
addSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> TcM a -> TcM a
166 167 168
addSigCtxt ctxt hs_ty thing_inside
  = setSrcSpan (getLoc hs_ty) $
    addErrCtxt (pprSigCtxt ctxt hs_ty) $
169 170
    thing_inside

171
pprSigCtxt :: UserTypeCtxt -> LHsType GhcRn -> SDoc
172 173 174 175 176 177 178 179 180 181 182 183 184
-- (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)

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

191 192
kcHsSigType :: [Located Name] -> LHsSigType GhcRn -> TcM ()
kcHsSigType names (HsIB { hsib_body = hs_ty
193
                                  , hsib_ext = sig_vars })
194
  = addSigCtxt (funsSigCtxt names) hs_ty $
195
    discardResult $
196
    bindImplicitTKBndrs_Skol sig_vars $
197
    tc_lhs_type typeLevelMode hs_ty liftedTypeKind
198 199

kcHsSigType _ (XHsImplicitBndrs _) = panic "kcHsSigType"
200

201
tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
202
-- Does not do validity checking
203
tcClassSigType skol_info names sig_ty
204
  = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
205 206 207 208
    tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
       -- Do not zonk-to-Type, nor perform a validity check
       -- We are in a knot with the class and associated types
       -- Zonking and validity checking is done by tcClassDecl
209

210
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
211
-- Does validity checking
212
-- See Note [Recipe for checking a signature]
213 214
tcHsSigType ctxt sig_ty
  = addSigCtxt ctxt (hsSigType sig_ty) $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
215
    do { traceTc "tcHsSigType {" (ppr sig_ty)
216

217
          -- Generalise here: see Note [Kind generalisation]
218 219
       ; ty <- tc_hs_sig_type skol_info sig_ty
                                      (expectedKindInCtxt ctxt)
220
       ; ty <- zonkTcType ty
221

222
       ; checkValidType ctxt ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
223
       ; traceTc "end tcHsSigType }" (ppr ty)
224
       ; return ty }
225 226
  where
    skol_info = SigTypeSkol ctxt
227

228 229
tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
               -> ContextKind -> TcM Type
230 231 232
-- Kind-checks/desugars an 'LHsSigType',
--   solve equalities,
--   and then kind-generalizes.
Richard Eisenberg's avatar
Richard Eisenberg committed
233
-- This will never emit constraints, as it uses solveEqualities interally.
234
-- No validity checking or zonking
235 236 237 238 239 240 241 242 243 244 245 246 247 248
tc_hs_sig_type skol_info hs_sig_type ctxt_kind
  | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
  = do { (tc_lvl, (wanted, (spec_tkvs, ty)))
              <- pushTcLevelM                           $
                 solveLocalEqualitiesX "tc_hs_sig_type" $
                 bindImplicitTKBndrs_Skol sig_vars      $
                 do { kind <- newExpectedKind ctxt_kind

                    ; tc_lhs_type typeLevelMode hs_ty kind }
       -- Any remaining variables (unsolved in the solveLocalEqualities)
       -- should be in the global tyvars, and therefore won't be quantified

       ; spec_tkvs <- zonkAndScopedSort spec_tkvs
       ; let ty1 = mkSpecForAllTys spec_tkvs ty
249
       ; kvs <- kindGeneralizeLocal wanted ty1
250 251 252
       ; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
                                  tc_lvl wanted

253 254 255 256
       -- See Note [Fail fast if there are insoluble kind equalities]
       --     in TcSimplify
       ; when (insolubleWC wanted) failM

257
       ; return (mkInvForAllTys kvs ty1) }
258

Simon Peyton Jones's avatar
Simon Peyton Jones committed
259
tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284

tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
-- tcTopLHsType is used for kind-checking top-level HsType where
--   we want to fully solve /all/ equalities, and report errors
-- Does zonking, but not validity checking because it's used
--   for things (like deriving and instances) that aren't
--   ordinary types
tcTopLHsType hs_sig_type ctxt_kind
  | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
  = do { traceTc "tcTopLHsType {" (ppr hs_ty)
       ; (spec_tkvs, ty)
              <- pushTcLevelM_                     $
                 solveEqualities                   $
                 bindImplicitTKBndrs_Skol sig_vars $
                 do { kind <- newExpectedKind ctxt_kind
                    ; tc_lhs_type typeLevelMode hs_ty kind }

       ; spec_tkvs <- zonkAndScopedSort spec_tkvs
       ; let ty1 = mkSpecForAllTys spec_tkvs ty
       ; kvs <- kindGeneralize ty1
       ; final_ty <- zonkTcTypeToType (mkInvForAllTys kvs ty1)
       ; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty])
       ; return final_ty}

tcTopLHsType (XHsImplicitBndrs _) _ = panic "tcTopLHsType"
285

286
-----------------
Ryan Scott's avatar
Ryan Scott committed
287
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
288
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
289
-- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
290 291
-- E.g.    class C (a::*) (b::k->k)
--         data T a b = ... deriving( C Int )
292
--    returns ([k], C, [k, Int], [k->k])
293
-- Return values are fully zonked
294
tcHsDeriv hs_ty
295 296 297 298
  = do { ty <- checkNoErrs $  -- Avoid redundant error report
                              -- with "illegal deriving", below
               tcTopLHsType hs_ty AnyKind
       ; let (tvs, pred)    = splitForAllTys ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
299
             (kind_args, _) = splitFunTys (tcTypeKind pred)
300
       ; case getClassPredTys_maybe pred of
301
           Just (cls, tys) -> return (tvs, (cls, tys, kind_args))
302
           Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
303

Ryan Scott's avatar
Ryan Scott committed
304 305 306 307 308 309 310 311 312 313 314 315 316
-- | 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.
317
     Maybe (DerivStrategy GhcRn) -- ^ The deriving strategy
Ryan Scott's avatar
Ryan Scott committed
318 319 320 321 322 323
  -> 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.
324
tcDerivStrategy mds thing_inside
Ryan Scott's avatar
Ryan Scott committed
325 326 327 328 329 330 331 332 333 334 335 336
  = 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
      ty' <- checkNoErrs $
337
             tcTopLHsType ty AnyKind
Ryan Scott's avatar
Ryan Scott committed
338 339 340 341 342 343 344 345 346 347
      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)

348
tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
349
                -> LHsSigType GhcRn
350
                -> TcM Type
351
-- Like tcHsSigType, but for a class instance declaration
352 353
tcHsClsInstType user_ctxt hs_inst_ty
  = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
354 355 356 357 358 359 360 361
    do { -- Fail eagerly if tcTopLHsType fails.  We are at top level so
         -- these constraints will never be solved later. And failing
         -- eagerly avoids follow-on errors when checkValidInstance
         -- sees an unsolved coercion hole
         inst_ty <- checkNoErrs $
                    tcTopLHsType hs_inst_ty (TheKind constraintKind)
       ; checkValidInstance user_ctxt hs_inst_ty inst_ty
       ; return inst_ty }
362

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
363 364
----------------------------------------------
-- | Type-check a visible type application
365
tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
366
-- See Note [Recipe for checking a signature] in TcHsType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
367
tcHsTypeApp wc_ty kind
368
  | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
369
  = do { ty <- solveLocalEqualities "tcHsTypeApp" $
370 371
               -- We are looking at a user-written type, very like a
               -- signature so we want to solve its equalities right now
My Nguyen's avatar
My Nguyen committed
372 373 374
               unsetWOptM Opt_WarnPartialTypeSignatures $
               setXOptM LangExt.PartialTypeSignatures $
               -- See Note [Wildcards in visible type application]
375
               tcWildCardBinders sig_wcs $ \ _ ->
376
               tcCheckLHsType hs_ty kind
377 378 379 380 381 382
       -- We must promote here. Ex:
       --   f :: forall a. a
       --   g = f @(forall b. Proxy b -> ()) @Int ...
       -- After when processing the @Int, we'll have to check its kind
       -- against the as-yet-unknown kind of b. This check causes an assertion
       -- failure if we don't promote.
383
       ; ty <- zonkPromoteType ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
384 385
       ; checkValidType TypeAppCtxt ty
       ; return ty }
386
tcHsTypeApp (XHsWildCardBndrs _) _ = panic "tcHsTypeApp"
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
387

My Nguyen's avatar
My Nguyen committed
388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403
{- Note [Wildcards in visible type application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

A HsWildCardBndrs's hswc_ext now only includes named wildcards, so any unnamed
wildcards stay unchanged in hswc_body and when called in tcHsTypeApp, tcCheckLHsType
will call emitWildCardHoleConstraints on them. However, this would trigger
error/warning when an unnamed wildcard is passed in as a visible type argument,
which we do not want because users should be able to write @_ to skip a instantiating
a type variable variable without fuss. The solution is to switch the
PartialTypeSignatures flags here to let the typechecker know that it's checking
a '@_' and do not emit hole constraints on it.
See related Note [Wildcards in visible kind application]
and Note [The wildcard story for types] in HsTypes.hs

-}

Austin Seipp's avatar
Austin Seipp committed
404 405 406
{-
************************************************************************
*                                                                      *
407
            The main kind checker: no validity checks here
Richard Eisenberg's avatar
Richard Eisenberg committed
408 409
*                                                                      *
************************************************************************
Austin Seipp's avatar
Austin Seipp committed
410
-}
411

dreixel's avatar
dreixel committed
412
---------------------------
413
tcHsOpenType, tcHsLiftedType,
414
  tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
415 416
-- Used for type signatures
-- Do not do validity checking
417 418 419
tcHsOpenType ty   = addTypeCtxt ty $ tcHsOpenTypeNC ty
tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty

420
tcHsOpenTypeNC   ty = do { ek <- newOpenTypeKind
421 422
                         ; tc_lhs_type typeLevelMode ty ek }
tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
423 424

-- Like tcHsType, but takes an expected kind
425
tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
426
tcCheckLHsType hs_ty exp_kind
427
  = addTypeCtxt hs_ty $
428
    tc_lhs_type typeLevelMode hs_ty exp_kind
429

430
tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
431
-- Called from outside: set the context
432
tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
dreixel's avatar
dreixel committed
433

Richard Eisenberg's avatar
Richard Eisenberg committed
434 435 436
-- 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)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
437 438 439 440 441 442 443 444 445 446 447 448 449
tcLHsTypeUnsaturated hs_ty
  | Just (hs_fun_ty, hs_args) <- splitHsAppTys (unLoc hs_ty)
  = addTypeCtxt hs_ty $
    do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
       ; tcInferApps_nosat mode hs_fun_ty fun_ty hs_args }
         -- Notice the 'nosat'; do not instantiate trailing
         -- invisible arguments of a type family.
         -- See Note [Dealing with :kind]

  | otherwise
  = addTypeCtxt hs_ty $
    tc_infer_lhs_type mode hs_ty

Richard Eisenberg's avatar
Richard Eisenberg committed
450
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472
    mode = typeLevelMode

{- Note [Dealing with :kind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this GHCi command
  ghci> type family F :: Either j k
  ghci> :kind F
  F :: forall {j,k}. Either j k

We will only get the 'forall' if we /refrain/ from saturating those
invisible binders. But generally we /do/ saturate those invisible
binders (see tcInferApps), and we want to do so for nested application
even in GHCi.  Consider for example (Trac #16287)
  ghci> type family F :: k
  ghci> data T :: (forall k. k) -> Type
  ghci> :kind T F
We want to reject this. It's just at the very top level that we want
to switch off saturation.

So tcLHsTypeUnsaturated does a little special case for top level
applications.  Actually the common case is a bare variable, as above.

Richard Eisenberg's avatar
Richard Eisenberg committed
473

474 475 476 477 478 479 480 481 482 483 484 485
************************************************************************
*                                                                      *
      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
486
-}
487

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
488 489 490 491
-- | 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.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
492 493 494
--
-- To find out where the mode is used, search for 'mode_level'
data TcTyMode = TcTyMode { mode_level :: TypeOrKind }
495 496

typeLevelMode :: TcTyMode
Simon Peyton Jones's avatar
Simon Peyton Jones committed
497
typeLevelMode = TcTyMode { mode_level = TypeLevel }
498 499

kindLevelMode :: TcTyMode
Simon Peyton Jones's avatar
Simon Peyton Jones committed
500
kindLevelMode = TcTyMode { mode_level = KindLevel }
501 502 503 504 505

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

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
506 507 508
instance Outputable TcTyMode where
  ppr = ppr . mode_level

509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526
{-
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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
527
again. This is done in calls to tcInstInvisibleTyBinders.
528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552

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.
553

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 $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
563
    tc_infer_hs_type mode ty
564

Simon Peyton Jones's avatar
Simon Peyton Jones committed
565 566 567 568 569 570 571 572
---------------------------
-- | Call 'tc_infer_hs_type' and check its result against an expected kind.
tc_infer_hs_type_ek :: HasDebugCallStack => TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
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 }

---------------------------
573 574
-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
575
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
576

Simon Peyton Jones's avatar
Simon Peyton Jones committed
577 578
tc_infer_hs_type mode (HsParTy _ t)
  = tc_infer_lhs_type mode t
579

Simon Peyton Jones's avatar
Simon Peyton Jones committed
580 581 582 583
tc_infer_hs_type mode ty
  | Just (hs_fun_ty, hs_args) <- splitHsAppTys ty
  = do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
       ; tcInferApps mode hs_fun_ty fun_ty hs_args }
584

585
tc_infer_hs_type mode (HsKindSig _ ty sig)
586
  = do { sig' <- tcLHsKindSig KindSigCtxt sig
587
                 -- We must typecheck the kind signature, and solve all
588 589
                 -- 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
590
                 -- to be fully determined (Trac #14904)
591
       ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
592 593
       ; ty' <- tc_lhs_type mode ty sig'
       ; return (ty', sig') }
594

595 596 597 598 599 600
-- 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].
601
tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
602
  = tc_infer_hs_type mode ty
603

604
tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
605
tc_infer_hs_type _    (XHsType (NHsCoreTy ty))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
606
  = return (ty, tcTypeKind ty)
My Nguyen's avatar
My Nguyen committed
607 608 609 610 611 612 613

tc_infer_hs_type _ (HsExplicitListTy _ _ tys)
  | null tys  -- this is so that we can use visible kind application with '[]
              -- e.g ... '[] @Bool
  = return (mkTyConTy promotedNilDataCon,
            mkSpecForAllTys [alphaTyVar] $ mkListTy alphaTy)

614 615 616 617 618
tc_infer_hs_type mode other_ty
  = do { kv <- newMetaKindVar
       ; ty' <- tc_hs_type mode other_ty kv
       ; return (ty', kv) }

619
------------------------------------------
620
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
621
tc_lhs_type mode (L span ty) exp_kind
622
  = setSrcSpan span $
623
    tc_hs_type mode ty exp_kind
624 625

------------------------------------------
626
tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
627 628
-- See Note [Bidirectional type checking]

629 630 631
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 _) _
632 633
    -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
    -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
634 635 636 637 638 639 640 641 642
    -- 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" }
643
tc_hs_type _ ty@(HsRecTy {})      _
644
      -- Record types (which only show up temporarily in constructor
645
      -- signatures) should have been removed by now
646
    = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
647

648 649 650 651 652
-- 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].
653
tc_hs_type mode (HsSpliceTy _ (HsSpliced _ mod_finalizers (HsSplicedTy ty)))
654 655 656 657
           exp_kind
  = do addModFinalizersWithLclEnv mod_finalizers
       tc_hs_type mode ty exp_kind

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

662
---------- Functions and applications
663
tc_hs_type mode (HsFunTy _ ty1 ty2) exp_kind
664
  = tc_fun_type mode ty1 ty2 exp_kind
665

666
tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
667
  | op `hasKey` funTyConKey
668
  = tc_fun_type mode ty1 ty2 exp_kind
669 670

--------- Foralls
671
tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
672 673 674 675
  = do { (tclvl, wanted, (tvs', ty'))
            <- pushLevelAndCaptureConstraints $
               bindExplicitTKBndrs_Skol hs_tvs $
               tc_lhs_type mode ty exp_kind
676
    -- Do not kind-generalise here!  See Note [Kind generalisation]
677
    -- Why exp_kind?  See Note [Body kind of HsForAllTy]
678 679 680 681 682 683
       ; let bndrs       = mkTyVarBinders Specified tvs'
             skol_info   = ForAllSkol (ppr forall)
             m_telescope = Just (sep (map ppr hs_tvs))

       ; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted

684
       ; return (mkForAllTys bndrs ty') }
685

Simon Peyton Jones's avatar
Simon Peyton Jones committed
686
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
687
  | null (unLoc ctxt)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
688
  = tc_lhs_type mode rn_ty exp_kind
689

Simon Peyton Jones's avatar
Simon Peyton Jones committed
690 691
  -- See Note [Body kind of a HsQualTy]
  | tcIsConstraintKind exp_kind
692
  = do { ctxt' <- tc_hs_context mode ctxt
Simon Peyton Jones's avatar
Simon Peyton Jones committed
693 694
       ; ty'   <- tc_lhs_type mode rn_ty constraintKind
       ; return (mkPhiTy ctxt' ty') }
695

Simon Peyton Jones's avatar
Simon Peyton Jones committed
696 697
  | otherwise
  = do { ctxt' <- tc_hs_context mode ctxt
698

Simon Peyton Jones's avatar
Simon Peyton Jones committed
699 700 701 702 703
       ; ek <- newOpenTypeKind  -- The body kind (result of the function) can
                                -- be TYPE r, for any r, hence newOpenTypeKind
       ; ty' <- tc_lhs_type mode rn_ty ek
       ; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
                           liftedTypeKind exp_kind }
704 705

--------- Lists, arrays, and tuples
706
tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
707
  = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
708
       ; checkWiredInTyCon listTyCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
709
       ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
710

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

734
       ; tys' <- sequence [ setSrcSpan loc $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
735
                            checkExpectedKind hs_ty ty kind arg_kind
736
                          | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
737

Simon Peyton Jones's avatar
Simon Peyton Jones committed
738
       ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
739

dreixel's avatar
dreixel committed
740

741
tc_hs_type mode rn_ty@(HsTupleTy _ hs_tup_sort tys) exp_kind
742
  = tc_tuple rn_ty mode tup_sort tys exp_kind
743 744 745 746 747 748 749
  where
    tup_sort = case hs_tup_sort of  -- Fourth case dealt with above
                  HsUnboxedTuple    -> UnboxedTuple
                  HsBoxedTuple      -> BoxedTuple
                  HsConstraintTuple -> ConstraintTuple
                  _                 -> panic "tc_hs_type HsTupleTy"

750
tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
751
  = do { let arity = length hs_tys
752 753
       ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
       ; tau_tys   <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
754
       ; let arg_reps = map kindRep arg_kinds
Richard Eisenberg's avatar
Richard Eisenberg committed
755
             arg_tys  = arg_reps ++ tau_tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
756 757 758
             sum_ty   = mkTyConApp (sumTyCon arity) arg_tys
             sum_kind = unboxedSumKind arg_reps
       ; checkExpectedKind rn_ty sum_ty sum_kind exp_kind
759
       }
dreixel's avatar
dreixel committed
760

761
--------- Promoted lists and tuples
762
tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
763
  = do { tks <- mapM (tc_infer_lhs_type mode) tys
764
       ; (taus', kind) <- unifyKinds tys tks
765
       ; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
Simon Peyton Jones's avatar
Simon Peyton Jones committed
766
       ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
767
  where
768 769
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
770

771
tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
772 773 774 775 776 777
  -- 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
778
             tup_k      = mkTyConApp kind_con ks
Simon Peyton Jones's avatar
Simon Peyton Jones committed
779
       ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
780 781
  where
    arity = length tys
782 783

--------- Constraint types
784
tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
785 786
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; ty' <- tc_lhs_type mode ty liftedTypeKind
787
       ; let n' = mkStrLitTy $ hsIPNameFS n
788
       ; ipClass <- tcLookupClass ipClassName
Simon Peyton Jones's avatar
Simon Peyton Jones committed
789 790
       ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
                           constraintKind exp_kind }
791

Simon Peyton Jones's avatar
Simon Peyton Jones committed
792
tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
793 794
  -- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't have to
  -- handle it in 'coreView' and 'tcView'.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
795
  = checkExpectedKind rn_ty liftedTypeKind liftedTypeKind exp_kind
796

797
--------- Literals
Simon Peyton Jones's avatar
Simon Peyton Jones committed
798
tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
799
  = do { checkWiredInTyCon typeNatKindCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
800
       ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
801

Simon Peyton Jones's avatar
Simon Peyton Jones committed
802
tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
803
  = do { checkWiredInTyCon typeSymbolKindCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
804
       ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
805 806 807

--------- Potentially kind-polymorphic types: call the "up" checker
-- See Note [Future-proofing the type checker]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
808 809 810 811 812
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@(HsAppKindTy{})         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
813
tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
Simon Peyton Jones's avatar
Simon Peyton Jones committed
814
tc_hs_type _    wc@(HsWildCardTy _)        ek = tcWildCardOcc wc ek
815

Simon Peyton Jones's avatar
Simon Peyton Jones committed
816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831
------------------------------------------
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
            -> TcM TcType
tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
  TypeLevel ->
    do { arg_k <- newOpenTypeKind
       ; res_k <- newOpenTypeKind
       ; ty1' <- tc_lhs_type mode ty1 arg_k
       ; ty2' <- tc_lhs_type mode ty2 res_k
       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
                           liftedTypeKind exp_kind }
  KindLevel ->  -- no representation polymorphism in kinds. yet.
    do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
       ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
                           liftedTypeKind exp_kind }
832

Simon Peyton Jones's avatar
Simon Peyton Jones committed
833 834 835
---------------------------
tcWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
tcWildCardOcc wc exp_kind
My Nguyen's avatar
My Nguyen committed
836
  = do { wc_tv <- newWildTyVar
837
          -- The wildcard's kind should be an un-filled-in meta tyvar
My Nguyen's avatar
My Nguyen committed
838 839 840 841 842 843 844 845
       ; loc <- getSrcSpanM
       ; uniq <- newUnique
       ; let name = mkInternalName uniq (mkTyVarOcc "_") loc
       ; part_tysig <- xoptM LangExt.PartialTypeSignatures
       ; warning <- woptM Opt_WarnPartialTypeSignatures
       -- See Note [Wildcards in visible kind application]
       ; unless (part_tysig && not warning)
             (emitWildCardHoleConstraints [(name,wc_tv)])
Simon Peyton Jones's avatar
Simon Peyton Jones committed
846
       ; checkExpectedKind wc (mkTyVarTy wc_tv)
847
                           (tyVarKind wc_tv) exp_kind }
848

My Nguyen's avatar
My Nguyen committed
849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871
{- Note [Wildcards in visible kind application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are cases where users might want to pass in a wildcard as a visible kind
argument, for instance:

data T :: forall k1 k2. k1 → k2 → Type where
  MkT :: T a b
x :: T @_ @Nat False n
x = MkT

So we should allow '@_' without emitting any hole constraints, and
regardless of whether PartialTypeSignatures is enabled or not. But how would
the typechecker know which '_' is being used in VKA and which is not when it
calls emitWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs,
but instead give every unnamed wildcard a fresh wild tyvar in tcWildCardOcc.
And whenever we see a '@', we automatically turn on PartialTypeSignatures and
turn off hole constraint warnings, and never call emitWildCardHoleConstraints
under these conditions.
See related Note [Wildcards in visible type application] here and
Note [The wildcard story for types] in HsTypes.hs

-}
Simon Peyton Jones's avatar
Simon Peyton Jones committed
872 873 874 875 876 877

{- *********************************************************************
*                                                                      *
                Tuples
*                                                                      *
********************************************************************* -}
thomasw's avatar
thomasw committed
878

879
---------------------------
880
tupKindSort_maybe :: TcKind -> Maybe TupleSort
881
tupKindSort_maybe k
Simon Peyton Jones's avatar
Simon Peyton Jones committed
882
  | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
Ben Gamari's avatar
Ben Gamari committed
883
  | Just k'      <- tcView k            = tupKindSort_maybe k'
884 885 886
  | tcIsConstraintKind k = Just ConstraintTuple
  | tcIsLiftedTypeKind k   = Just BoxedTuple
  | otherwise            = Nothing
887

888 889
tc_tuple :: HsType GhcRn -> TcTyMode -> TupleSort -> [LHsType GhcRn] -> TcKind -> TcM TcType
tc_tuple rn_ty mode tup_sort tys exp_kind
890 891
  = do { arg_kinds <- case tup_sort of
           BoxedTuple      -> return (nOfThem arity liftedTypeKind)
892
           UnboxedTuple    -> mapM (\_ -> newOpenTypeKind) tys
893 894
           ConstraintTuple -> return (nOfThem arity constraintKind)
       ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
Simon Peyton Jones's avatar
Simon Peyton Jones committed
895
       ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
dreixel's avatar
dreixel committed
896
  where
897 898
    arity   = length tys

899 900
finish_tuple :: HsType GhcRn
             -> TupleSort
901 902 903 904
             -> [TcType]    -- ^ argument types
             -> [TcKind]    -- ^ of these kinds
             -> TcKind      -- ^ expected kind of the whole tuple
             -> TcM TcType
Simon Peyton Jones's avatar
Simon Peyton Jones committed
905
finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
906 907
  = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
       ; let arg_tys  = case tup_sort of
908
                   -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon