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

8
{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
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
        tcLHsKind,
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
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
Gergő Érdi's avatar
Gergő Érdi committed
66
import ConLike
67
import DataCon
68
import TysPrim ( tYPE )
69 70
import Class
import Name
71
import NameEnv
72 73
import NameSet
import VarEnv
74 75 76
import TysWiredIn
import BasicTypes
import SrcLoc
77 78
import Constants ( mAX_CTUPLE_SIZE )
import ErrUtils( MsgDoc )
79
import Unique
80
import Util
81
import UniqSupply
82
import Outputable
83
import FastString
84
import PrelNames hiding ( wildCardName )
85
import qualified GHC.LanguageExtensions as LangExt
86

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

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

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

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

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

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

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

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

149 150 151 152 153 154 155
funsSigCtxt :: [Located Name] -> UserTypeCtxt
-- Returns FunSigCtxt, with no redundant-context-reporting,
-- form a list of located names
funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 False
funsSigCtxt []              = panic "funSigCtxt"

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

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

175 176 177 178 179 180
tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType Name -> TcM Type
-- This one is used when we have a LHsSigWcType, but in
-- a place where wildards aren't allowed. The renamer has
-- alrady checked this, so we can simply ignore it.
tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)

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

tcClassSigType :: [Located Name] -> LHsSigType Name -> TcM Type
-- 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) $
194 195
    do { ty <- tc_hs_sig_type sig_ty liftedTypeKind
       ; kindGeneralizeType ty }
196 197 198 199 200 201

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

       ; ty <- tc_hs_sig_type sig_ty kind
209

210
          -- Generalise here: see Note [Kind generalisation]
211 212 213 214 215
       ; do_kind_gen <- decideKindGeneralisationPlan ty
       ; ty <- if do_kind_gen
               then kindGeneralizeType ty
               else zonkTcType ty

216 217 218 219
       ; checkValidType ctxt ty
       ; return ty }

tc_hs_sig_type :: LHsSigType Name -> Kind -> TcM Type
220
-- Does not do validity checking or zonking
221
tc_hs_sig_type (HsIB { hsib_body = hs_ty
222 223 224 225
                     , hsib_vars = sig_vars }) kind
  = do { (tkvs, ty) <- solveEqualities $
                       tcImplicitTKBndrsType sig_vars $
                       tc_lhs_type typeLevelMode hs_ty kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
226
       ; return (mkSpecForAllTys tkvs ty) }
batterseapower's avatar
batterseapower committed
227

228
-----------------
229
tcHsDeriv :: LHsSigType Name -> TcM ([TyVar], Class, [Type], [Kind])
230
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
231
-- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
232 233
-- E.g.    class C (a::*) (b::k->k)
--         data T a b = ... deriving( C Int )
234
--    returns ([k], C, [k, Int], [k->k])
235
tcHsDeriv hs_ty
236
  = do { cls_kind <- newMetaKindVar
237 238 239 240
                    -- 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
241
               tc_hs_sig_type hs_ty cls_kind
242
       ; ty <- kindGeneralizeType ty  -- also zonks
243
       ; cls_kind <- zonkTcType cls_kind
244
       ; let (tvs, pred) = splitForAllTys ty
245
       ; let (args, _) = splitFunTys cls_kind
246
       ; case getClassPredTys_maybe pred of
247
           Just (cls, tys) -> return (tvs, cls, tys, args)
248
           Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
249

250 251 252 253
tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
                -> LHsSigType Name
                -> TcM ([TyVar], ThetaType, Class, [Type])
-- Like tcHsSigType, but for a class instance declaration
254 255 256
tcHsClsInstType user_ctxt hs_inst_ty
  = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
    do { inst_ty <- tc_hs_sig_type hs_inst_ty constraintKind
257 258 259
       ; inst_ty <- kindGeneralizeType inst_ty
       ; checkValidInstance user_ctxt hs_inst_ty inst_ty }

260
-- Used for 'VECTORISE [SCALAR] instance' declarations
261
tcHsVectInst :: LHsSigType Name -> TcM (Class, [Type])
262
tcHsVectInst ty
263
  | Just (L _ cls_name, tys) <- hsTyGetAppHead_maybe (hsSigType ty)
264
    -- Ignoring the binders looks pretty dodgy to me
265
  = do { (cls, cls_kind) <- tcClass cls_name
266 267 268 269 270 271
       ; (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) }
272
  | otherwise
273
  = failWithTc $ text "Malformed instance type"
274

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
275 276 277 278
----------------------------------------------
-- | Type-check a visible type application
tcHsTypeApp :: LHsWcType Name -> Kind -> TcM Type
tcHsTypeApp wc_ty kind
279 280 281 282
  | HsWC { hswc_wcs = sig_wcs, hswc_body = hs_ty } <- wc_ty
  = do { ty <- solveEqualities $
               tcWildCardBindersX newWildTyVar sig_wcs $ \ _ ->
               tcCheckLHsType hs_ty kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
283 284 285 286 287 288 289
       ; 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
290 291 292
{-
************************************************************************
*                                                                      *
293
            The main kind checker: no validity checks here
294 295
%*                                                                      *
%************************************************************************
296 297

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

dreixel's avatar
dreixel committed
300
---------------------------
301 302
tcHsOpenType, tcHsLiftedType,
  tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType Name -> TcM TcType
303 304
-- Used for type signatures
-- Do not do validity checking
305 306 307
tcHsOpenType ty   = addTypeCtxt ty $ tcHsOpenTypeNC ty
tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty

308
tcHsOpenTypeNC   ty = do { ek <- newOpenTypeKind
309 310
                         ; tc_lhs_type typeLevelMode ty ek }
tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
311 312 313 314

-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType Name -> Kind -> TcM Type
tcCheckLHsType hs_ty exp_kind
315
  = addTypeCtxt hs_ty $
316
    tc_lhs_type typeLevelMode hs_ty exp_kind
317 318 319

tcLHsType :: LHsType Name -> TcM (TcType, TcKind)
-- Called from outside: set the context
320
tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
dreixel's avatar
dreixel committed
321

322
---------------------------
323
-- | Should we generalise the kind of this type signature?
324 325 326 327
-- We *should* generalise if the type is mentions no scoped type variables
-- or if NoMonoLocalBinds is set. Otherwise, nope.
decideKindGeneralisationPlan :: Type -> TcM Bool
decideKindGeneralisationPlan ty
328
  = do { mono_locals <- xoptM LangExt.MonoLocalBinds
329 330 331 332 333 334 335 336 337
       ; in_scope <- getInLocalScope
       ; let fvs        = tyCoVarsOfTypeList ty
             should_gen = not mono_locals || all (not . in_scope . getName) fvs
       ; traceTc "decideKindGeneralisationPlan"
           (vcat [ text "type:" <+> ppr ty
                 , text "ftvs:" <+> ppr fvs
                 , text "should gen?" <+> ppr should_gen ])
       ; return should_gen }

Austin Seipp's avatar
Austin Seipp committed
338
{-
339 340 341 342 343 344 345 346 347 348 349 350
************************************************************************
*                                                                      *
      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
351
-}
352

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
353 354 355 356 357
-- | 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
358 359 360 361 362 363 364 365 366 367 368 369 370
  = 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
371 372 373
instance Outputable TcTyMode where
  ppr = ppr . mode_level

374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418
{-
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.
-}
419

420
------------------------------------------
421 422 423 424 425 426
-- | Check and desugar a type, returning the core type and its
-- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
-- level.
tc_infer_lhs_type :: TcTyMode -> LHsType Name -> TcM (TcType, TcKind)
tc_infer_lhs_type mode (L span ty)
  = setSrcSpan span $
427 428
    do { (ty', kind) <- tc_infer_hs_type mode ty
       ; return (ty', kind) }
429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455

-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
tc_infer_hs_type :: TcTyMode -> HsType Name -> TcM (TcType, TcKind)
tc_infer_hs_type mode (HsTyVar (L _ tv)) = tcTyVar mode tv
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') }
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) }

456
------------------------------------------
457 458
tc_lhs_type :: TcTyMode -> LHsType Name -> TcKind -> TcM TcType
tc_lhs_type mode (L span ty) exp_kind
459
  = setSrcSpan span $
460 461
    do { ty' <- tc_hs_type mode ty exp_kind
       ; return ty' }
462

463
------------------------------------------
464
tc_fun_type :: TcTyMode -> LHsType Name -> LHsType Name -> TcKind -> TcM TcType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
465 466
tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
  TypeLevel ->
467 468 469 470
    do { arg_k <- newOpenTypeKind
       ; res_k <- newOpenTypeKind
       ; ty1' <- tc_lhs_type mode ty1 arg_k
       ; ty2' <- tc_lhs_type mode ty2 res_k
471
       ; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
472 473 474 475
  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 }
476

477
------------------------------------------
478 479 480 481 482
-- See also Note [Bidirectional type checking]
tc_hs_type :: TcTyMode -> HsType Name -> TcKind -> TcM TcType
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 {}) _
483 484 485
    -- 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)
486
    = failWithTc (text "Unexpected strictness annotation:" <+> ppr ty)
487
tc_hs_type _ ty@(HsRecTy _)      _
488
      -- Record types (which only show up temporarily in constructor
489
      -- signatures) should have been removed by now
490
    = failWithTc (text "Record syntax is illegal here:" <+> ppr ty)
491

492 493 494 495 496 497 498 499 500 501 502 503
-- 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

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

508 509 510
---------- Functions and applications
tc_hs_type mode (HsFunTy ty1 ty2) exp_kind
  = tc_fun_type mode ty1 ty2 exp_kind
511

512
tc_hs_type mode (HsOpTy ty1 (L _ op) ty2) exp_kind
513
  | op `hasKey` funTyConKey
514
  = tc_fun_type mode ty1 ty2 exp_kind
515 516

--------- Foralls
517
tc_hs_type mode (HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kind
518
  = fmap fst $
519
    tcExplicitTKBndrs hs_tvs $ \ tvs' ->
520
    -- Do not kind-generalise here!  See Note [Kind generalisation]
521
    -- Why exp_kind?  See Note [Body kind of HsForAllTy]
522 523
    do { ty' <- tc_lhs_type mode ty exp_kind
       ; let bound_vars = allBoundVariables ty'
Simon Peyton Jones's avatar
Simon Peyton Jones committed
524
             bndrs      = mkTyVarBinders Specified tvs'
525
       ; return (mkForAllTys bndrs ty', bound_vars) }
526

527
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
528 529 530 531
  | null (unLoc ctxt)
  = tc_lhs_type mode ty exp_kind

  | otherwise
532
  = do { ctxt' <- tc_hs_context mode ctxt
533 534 535 536

         -- See Note [Body kind of a HsQualTy]
       ; ty' <- if isConstraintKind exp_kind
                then tc_lhs_type mode ty constraintKind
537 538 539
                else do { ek <- newOpenTypeKind
                                -- The body kind (result of the function)
                                -- can be * or #, hence newOpenTypeKind
540 541 542 543
                        ; ty <- tc_lhs_type mode ty ek
                        ; checkExpectedKind ty liftedTypeKind exp_kind }

       ; return (mkPhiTy ctxt' ty') }
544 545 546 547

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

551 552 553
tc_hs_type mode (HsPArrTy elt_ty) exp_kind
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
554
       ; checkWiredInTyCon parrTyCon
555
       ; checkExpectedKind (mkPArrTy tau_ty) liftedTypeKind exp_kind }
556

dreixel's avatar
dreixel committed
557
-- See Note [Distinguishing tuple kinds] in HsTypes
558
-- See Note [Inferring tuple kinds]
559
tc_hs_type mode (HsTupleTy HsBoxedOrConstraintTuple hs_tys) exp_kind
560
     -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
561
  | Just tup_sort <- tupKindSort_maybe exp_kind
562
  = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
563
    tc_tuple mode tup_sort hs_tys exp_kind
dreixel's avatar
dreixel committed
564
  | otherwise
Austin Seipp's avatar
Austin Seipp committed
565
  = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
566 567
       ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
       ; kinds <- mapM zonkTcType kinds
568 569 570 571 572 573
           -- 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)
574 575 576
               = case [ (k,s) | k <- kinds
                              , Just s <- [tupKindSort_maybe k] ] of
                    ((k,s) : _) -> (k,s)
577
                    [] -> (liftedTypeKind, BoxedTuple)
578 579
         -- In the [] case, it's not clear what the kind is, so guess *

580 581 582
       ; tys' <- sequence [ setSrcSpan loc $
                            checkExpectedKind ty kind arg_kind
                          | ((L loc _),ty,kind) <- zip3 hs_tys tys kinds ]
583

584
       ; finish_tuple tup_sort tys' (map (const arg_kind) tys') exp_kind }
585

dreixel's avatar
dreixel committed
586

587 588
tc_hs_type mode (HsTupleTy hs_tup_sort tys) exp_kind
  = tc_tuple mode tup_sort tys exp_kind
589 590 591 592 593 594 595
  where
    tup_sort = case hs_tup_sort of  -- Fourth case dealt with above
                  HsUnboxedTuple    -> UnboxedTuple
                  HsBoxedTuple      -> BoxedTuple
                  HsConstraintTuple -> ConstraintTuple
                  _                 -> panic "tc_hs_type HsTupleTy"

596 597
tc_hs_type mode (HsSumTy hs_tys) exp_kind
  = do { let arity = length hs_tys
598 599
       ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
       ; tau_tys   <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
600 601 602
       ; let arg_tys = map (getRuntimeRepFromKind "tc_hs_type HsSumTy") arg_kinds ++ tau_tys
       ; checkExpectedKind (mkTyConApp (sumTyCon arity) arg_tys) (tYPE unboxedSumRepDataConTy) exp_kind
       }
dreixel's avatar
dreixel committed
603

604
--------- Promoted lists and tuples
605 606 607 608 609
tc_hs_type mode (HsExplicitListTy _k tys) exp_kind
  = 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 }
610
  where
611 612
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
613

614
tc_hs_type mode (HsExplicitTupleTy _ tys) exp_kind
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
615 616 617 618 619 620
  -- 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
621
             tup_k      = mkTyConApp kind_con ks
622
       ; checkExpectedKind (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
623 624
  where
    arity = length tys
625 626

--------- Constraint types
627 628 629
tc_hs_type mode (HsIParamTy n ty) exp_kind
  = do { MASSERT( isTypeLevel (mode_level mode) )
       ; ty' <- tc_lhs_type mode ty liftedTypeKind
630
       ; let n' = mkStrLitTy $ hsIPNameFS n
631
       ; ipClass <- tcLookupClass ipClassName
632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660
       ; 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
661 662
  = do { wc_tv <- tcWildCardOcc wc exp_kind
       ; return (mkTyVarTy wc_tv) }
663 664 665 666 667

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

668 669 670 671 672 673 674 675
tcWildCardOcc :: HsWildCardInfo Name -> Kind -> TcM TcTyVar
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 }

676 677 678 679 680 681
---------------------------
-- | Call 'tc_infer_hs_type' and check its result against an expected kind.
tc_infer_hs_type_ek :: TcTyMode -> HsType Name -> TcKind -> TcM TcType
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
682

683
---------------------------
684
tupKindSort_maybe :: TcKind -> Maybe TupleSort
685
tupKindSort_maybe k
Simon Peyton Jones's avatar
Simon Peyton Jones committed
686 687
  | Just (k', _) <- splitCastTy_maybe k = tupKindSort_maybe k'
  | Just k'      <- coreView k          = tupKindSort_maybe k'
688 689
  | isConstraintKind k = Just ConstraintTuple
  | isLiftedTypeKind k = Just BoxedTuple
690 691
  | otherwise          = Nothing

692 693 694 695
tc_tuple :: TcTyMode -> TupleSort -> [LHsType Name] -> TcKind -> TcM TcType
tc_tuple mode tup_sort tys exp_kind
  = do { arg_kinds <- case tup_sort of
           BoxedTuple      -> return (nOfThem arity liftedTypeKind)
696
           UnboxedTuple    -> mapM (\_ -> newOpenTypeKind) tys
697 698 699
           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
700
  where
701 702 703 704 705 706 707 708 709 710
    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
711 712
                   -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
                 UnboxedTuple    -> map (getRuntimeRepFromKind "finish_tuple") tau_kinds
713 714 715
                                    ++ tau_tys
                 BoxedTuple      -> tau_tys
                 ConstraintTuple -> tau_tys
716
       ; tycon <- case tup_sort of
717 718 719 720 721 722 723 724
           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)
725
       ; checkExpectedKind (mkTyConApp tycon arg_tys) res_kind exp_kind }
726
  where
727
    arity = length tau_tys
728
    res_kind = case tup_sort of
729 730 731
                 UnboxedTuple
                   | arity == 0  -> tYPE voidRepDataConTy
                   | otherwise   -> unboxedTupleKind
732 733
                 BoxedTuple      -> liftedTypeKind
                 ConstraintTuple -> constraintKind
734

735 736
bigConstraintTuple :: Arity -> MsgDoc
bigConstraintTuple arity
737 738 739
  = hang (text "Constraint tuple arity too large:" <+> int arity
          <+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
       2 (text "Instead, use a nested tuple")
740

741
---------------------------
742 743 744
-- | 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.
745 746
-- Never calls 'matchExpectedFunKind'; when the kind runs out of binders,
-- this stops processing.
747 748 749 750
-- 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
751 752 753 754
-- 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@.)
755 756
tcInferArgs :: Outputable fun
            => fun                      -- ^ the function
757
            -> [TyConBinder]            -- ^ function kind's binders
758 759
            -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
            -> [LHsType Name]           -- ^ args
760 761 762
            -> TcM (TCvSubst, [TyBinder], [TcType], [LHsType Name], Int)
               -- ^ (instantiating subst, un-insted leftover binders,
               --   typechecked args, untypechecked args, n)
763 764 765
tcInferArgs fun tc_binders mb_kind_info args
  = do { let binders = tyConBindersTyBinders tc_binders  -- UGH!
       ; (subst, leftover_binders, args', leftovers, n)
766
           <- tc_infer_args typeLevelMode fun binders mb_kind_info args 1
767
        -- now, we need to instantiate any remaining invisible arguments
768
       ; let (invis_bndrs, other_binders) = break isVisibleBinder leftover_binders
769 770 771 772
       ; (subst', invis_args)
           <- tcInstBindersX subst mb_kind_info invis_bndrs
       ; return ( subst'
                , other_binders
Simon Peyton Jones's avatar
Simon Peyton Jones committed
773
                , args' `chkAppend` invis_args
774 775 776 777 778 779 780
                , 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
781
              -> [TyBinder]               -- ^ function kind's binders (zonked)
782 783 784
              -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
              -> [LHsType Name]           -- ^ args
              -> Int                      -- ^ number to start arg counter at
785 786
              -> TcM (TCvSubst, [TyBinder], [TcType], [LHsType Name], Int)
tc_infer_args mode orig_ty binders mb_kind_info orig_args n0
Simon Peyton Jones's avatar
Simon Peyton Jones committed
787
  = go emptyTCvSubst binders orig_args n0 []
788
  where
789 790
    go subst binders []   n acc
      = return ( subst, binders, reverse acc, [], n )
791 792 793 794
    -- when we call this when checking type family patterns, we really
    -- do want to instantiate all invisible arguments. During other
    -- typechecking, we don't.

795 796 797 798 799
    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) }
800

801 802
      | otherwise
      = do { traceTc "tc_infer_args (vis)" (ppr binder $$ ppr arg)
803
           ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
804 805 806
                     tc_lhs_type mode arg (substTyUnchecked subst $
                                           tyBinderType binder)
           ; let subst' = extendTvSubstBinder subst binder arg'
807
           ; go subst' binders args (n+1) (arg' : acc) }
808

809 810
    go subst [] all_args n acc
      = return (subst, [], reverse acc, all_args, n)
811

812
-- | Applies a type to a list of arguments.
813 814 815 816
-- 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.
817
tcInferApps :: Outputable fun
818 819 820 821 822 823
            => TcTyMode
            -> fun                  -- ^ Function (for printing only)
            -> TcType               -- ^ Function (could be knot-tied)
            -> TcKind               -- ^ Function kind (zonked)
            -> [LHsType Name]       -- ^ Args
            -> TcM (TcType, TcKind) -- ^ (f args, result kind)
824
tcInferApps mode orig_ty ty ki args = go ty ki args 1
825
  where
826 827
    go fun fun_kind []   _ = return (fun, fun_kind)
    go fun fun_kind args n
828 829 830 831 832
      | let (binders, res_kind) = splitPiTys fun_kind
      , not (null binders)
      = do { (subst, leftover_binders, args', leftover_args, n')
                <- tc_infer_args mode orig_ty binders Nothing args n
           ; let fun_kind' = substTyUnchecked subst $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
833
                             mkPiTys leftover_binders res_kind
834
           ; go (mkNakedAppTys fun args') fun_kind' leftover_args n' }
835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855

    go fun fun_kind all_args@(arg:args) n
      = do { (co, arg_k, res_k) <- matchExpectedFunKind (length all_args)
                                                        fun fun_kind
           ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
                     tc_lhs_type mode arg arg_k
           ; go (mkNakedAppTy (fun `mkNakedCastTy` co) arg')
                res_k args (n+1) }

--------------------------
checkExpectedKind :: TcType               -- the type whose kind we're checking
                  -> TcKind               -- the known kind of that type, k
                  -> TcKind               -- the expected kind, exp_kind
                  -> TcM TcType    -- a possibly-inst'ed, casted type :: exp_kind
-- Instantiate a kind (if necessary) and then call unifyType
--      (checkExpectedKind ty act_kind exp_kind)
-- checks that the actual kind act_kind is compatible
--      with the expected kind exp_kind
checkExpectedKind ty act_kind exp_kind
 = do { (ty', act_kind') <- instantiate ty act_kind exp_kind
      ; let origin = TypeEqOrigin { uo_actual   = act_kind'
856
                                  , uo_expected = exp_kind
857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891
                                  , uo_thing    = Just $ mkTypeErrorThing ty'
                                  }
      ; co_k <- uType origin KindLevel act_kind' exp_kind
      ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
                                          , ppr exp_kind
                                          , ppr co_k ])
      ; let result_ty = ty' `mkNakedCastTy` co_k
      ; return result_ty }
  where
    -- we need to make sure that both kinds have the same number of implicit
    -- foralls out front. If the actual kind has more, instantiate accordingly.
    -- Otherwise, just pass the type & kind through -- the errors are caught
    -- in unifyType.
    instantiate :: TcType    -- the type
                -> TcKind    -- of this kind
                -> TcKind   -- but expected to be of this one
                -> TcM ( TcType   -- the inst'ed type
                       , TcKind ) -- its new kind
    instantiate ty act_ki exp_ki
      = let (exp_bndrs, _) = splitPiTysInvisible exp_ki in
        instantiateTyN (length exp_bndrs) ty act_ki

-- | Instantiate a type to have at most @n@ invisible arguments.
instantiateTyN :: Int    -- ^ @n@
               -> TcType -- ^ the type
               -> TcKind -- ^ its kind
               -> TcM (TcType, TcKind)   -- ^ The inst'ed type with kind
instantiateTyN n ty ki
  = let (bndrs, inner_ki)            = splitPiTysInvisible ki
        num_to_inst                  = length bndrs - n
           -- NB: splitAt is forgiving with invalid numbers
        (inst_bndrs, leftover_bndrs) = splitAt num_to_inst bndrs
    in
    if num_to_inst <= 0 then return (ty, ki) else
    do { (subst, inst_args) <- tcInstBinders inst_bndrs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
892
       ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
893 894
             ki'        = substTy subst rebuilt_ki
       ; return (mkNakedAppTys ty inst_args, ki') }
895

896
---------------------------
897
tcHsContext :: LHsContext Name -> TcM [PredType]
898
tcHsContext = tc_hs_context typeLevelMode
899

900
tcLHsPredType :: LHsType Name -> TcM PredType
901 902 903 904 905 906 907
tcLHsPredType = tc_lhs_pred typeLevelMode

tc_hs_context :: TcTyMode -> LHsContext Name -> TcM [PredType]
tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)

tc_lhs_pred :: TcTyMode -> LHsType Name -> TcM PredType
tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
908 909

---------------------------
910
tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
dreixel's avatar
dreixel committed
911 912
-- See Note [Type checking recursive type and class declarations]
-- in TcTyClsDecls
913
tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
dreixel's avatar
dreixel committed
914 915 916
  = do { traceTc "lk1" (ppr name)
       ; thing <- tcLookup name
       ; case thing of
917 918
           ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)