TcHsType.hs 121 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
        -- Sort-checking kinds
Simon Peyton Jones's avatar
Simon Peyton Jones committed
52
        tcLHsKindSig, badKindSig,
53

54 55 56
        -- Zonking and promoting
        zonkPromoteType,

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

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

#include "HsVersions.h"

66 67
import GhcPrelude

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

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

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

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

126 127 128
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.
129 130 131

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

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

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

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

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

158 159 160 161 162 163
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"

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

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

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

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

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

200
tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
201
-- Does not do validity checking
202
tcClassSigType skol_info names sig_ty
203
  = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
204 205 206 207
    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
208

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

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

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

227 228
tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
               -> ContextKind -> TcM Type
229 230 231
-- Kind-checks/desugars an 'LHsSigType',
--   solve equalities,
--   and then kind-generalizes.
Richard Eisenberg's avatar
Richard Eisenberg committed
232
-- This will never emit constraints, as it uses solveEqualities interally.
233
-- No validity checking or zonking
234 235 236 237 238 239 240 241 242 243 244 245 246
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
247
       ; kvs <- kindGeneralizeLocal wanted ty1
248 249 250
       ; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
                                  tc_lvl wanted

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

255
       ; return (mkInvForAllTys kvs ty1) }
256

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

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"
283

284
-----------------
Ryan Scott's avatar
Ryan Scott committed
285
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
286
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
287
-- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
288 289
-- E.g.    class C (a::*) (b::k->k)
--         data T a b = ... deriving( C Int )
290
--    returns ([k], C, [k, Int], [k->k])
291
-- Return values are fully zonked
292
tcHsDeriv hs_ty
293 294 295 296
  = 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
297
             (kind_args, _) = splitFunTys (tcTypeKind pred)
298
       ; case getClassPredTys_maybe pred of
299
           Just (cls, tys) -> return (tvs, (cls, tys, kind_args))
300
           Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
301

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

346
tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
347
                -> LHsSigType GhcRn
348
                -> TcM Type
349
-- Like tcHsSigType, but for a class instance declaration
350 351
tcHsClsInstType user_ctxt hs_inst_ty
  = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
352 353 354 355 356 357 358 359
    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 }
360

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
361 362
----------------------------------------------
-- | Type-check a visible type application
363
tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
364
-- See Note [Recipe for checking a signature] in TcHsType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
365
tcHsTypeApp wc_ty kind
366
  | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
367
  = do { ty <- solveLocalEqualities "tcHsTypeApp" $
368 369
               -- 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
370 371 372
               unsetWOptM Opt_WarnPartialTypeSignatures $
               setXOptM LangExt.PartialTypeSignatures $
               -- See Note [Wildcards in visible type application]
373
               tcWildCardBinders sig_wcs $ \ _ ->
374
               tcCheckLHsType hs_ty kind
375 376 377 378 379 380
       -- 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.
381
       ; ty <- zonkPromoteType ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
382 383
       ; checkValidType TypeAppCtxt ty
       ; return ty }
384
tcHsTypeApp (XHsWildCardBndrs _) _ = panic "tcHsTypeApp"
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
385

My Nguyen's avatar
My Nguyen committed
386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401
{- 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
402 403 404
{-
************************************************************************
*                                                                      *
405
            The main kind checker: no validity checks here
Richard Eisenberg's avatar
Richard Eisenberg committed
406 407
*                                                                      *
************************************************************************
Austin Seipp's avatar
Austin Seipp committed
408
-}
409

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

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

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

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

Richard Eisenberg's avatar
Richard Eisenberg committed
432 433 434
-- 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
435 436 437 438 439 440 441 442 443 444 445 446 447
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
448
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470
    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
471

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

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

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

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

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

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

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

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

552
-}
553

554
------------------------------------------
555 556 557
-- | Check and desugar a type, returning the core type and its
-- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
-- level.
558
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
559 560
tc_infer_lhs_type mode (L span ty)
  = setSrcSpan span $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
561
    tc_infer_hs_type mode ty
562

Simon Peyton Jones's avatar
Simon Peyton Jones committed
563 564 565 566 567 568 569 570
---------------------------
-- | 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 }

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
578 579 580 581
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 }
582

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

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

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

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)

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

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

623
tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
624 625
-- See Note [Bidirectional type checking]

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

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

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

659
---------- Functions and applications
660
tc_hs_type mode (HsFunTy _ ty1 ty2) exp_kind
661
  = tc_fun_type mode ty1 ty2 exp_kind
662

663
tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
664
  | op `hasKey` funTyConKey
665
  = tc_fun_type mode ty1 ty2 exp_kind
666 667

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

       ; emitResidualTvConstraint skol_info m_telescope tvs' tclvl wanted

685
       ; return (mkForAllTys bndrs ty') }
686

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

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
700 701 702 703 704
       ; 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 }
705 706

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

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

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

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

dreixel's avatar
dreixel committed
741

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

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

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

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
793
tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
794 795
  -- 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
796
  = checkExpectedKind rn_ty liftedTypeKind liftedTypeKind exp_kind
797

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

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

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
817 818 819 820 821 822 823 824 825
------------------------------------------
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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
826
       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkVisFunTy ty1' ty2')
Simon Peyton Jones's avatar
Simon Peyton Jones committed
827 828 829 830
                           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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
831
       ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkVisFunTy ty1' ty2')
Simon Peyton Jones's avatar
Simon Peyton Jones committed
832
                           liftedTypeKind exp_kind }
833

Simon Peyton Jones's avatar
Simon Peyton Jones committed
834 835 836
---------------------------
tcWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
tcWildCardOcc wc exp_kind
My Nguyen's avatar
My Nguyen committed
837
  = do { wc_tv <- newWildTyVar
838
          -- The wildcard's kind should be an un-filled-in meta tyvar
My Nguyen's avatar
My Nguyen committed
839 840 841 842 843 844 845 846
       ; 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
847
       ; checkExpectedKind wc (mkTyVarTy wc_tv)
848
                           (tyVarKind wc_tv) exp_kind }
849

My Nguyen's avatar
My Nguyen committed
850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872
{- 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
873 874 875 876 877 878

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

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

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