HsType.hs 178 KB
Newer Older
1

Alan Zimmerman's avatar
Alan Zimmerman committed
2
3
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
4
5
6
7
8
9
10
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE ViewPatterns        #-}

{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

Austin Seipp's avatar
Austin Seipp committed
11
12
13
14
15
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

-}
16

Sylvain Henry's avatar
Sylvain Henry committed
17
18
-- | Typechecking user-specified @MonoTypes@
module GHC.Tc.Gen.HsType (
19
        -- Type signatures
20
        kcClassSigType, tcClassSigType,
21
        tcHsSigType, tcHsSigWcType,
22
        tcHsPartialSigType,
23
        tcStandaloneKindSig,
24
        funsSigCtxt, addSigCtxt, pprSigCtxt,
25
26

        tcHsClsInstType,
Ryan Scott's avatar
Ryan Scott committed
27
        tcHsDeriv, tcDerivStrategy,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
28
        tcHsTypeApp,
29
        UserTypeCtxt(..),
30
31
32
33
        bindImplicitTKBndrs_Tv, bindImplicitTKBndrs_Skol,
            bindImplicitTKBndrs_Q_Tv, bindImplicitTKBndrs_Q_Skol,
        bindExplicitTKBndrs_Tv, bindExplicitTKBndrs_Skol,
            bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol,
34
35
36
37
38
39

        bindOuterFamEqnTKBndrs, bindOuterFamEqnTKBndrs_Q_Tv,
        tcOuterTKBndrs, scopedSortOuter,
        bindOuterSigTKBndrs_Tv,
        tcExplicitTKBndrs,
        bindNamedWildCardBinders,
40

Simon Peyton Jones's avatar
Simon Peyton Jones committed
41
42
        -- Type checking type and class decls, and instances thereof
        bindTyClTyVars, tcFamTyPats,
43
        etaExpandAlgTyCon, tcbVisibilities,
dreixel's avatar
dreixel committed
44

45
          -- tyvars
46
        zonkAndScopedSort,
47

48
49
        -- Kind-checking types
        -- No kind generalisation, no checkValidType
50
51
        InitialKindStrategy(..),
        SAKS_or_CUSK(..),
52
        ContextKind(..),
53
        kcDeclHeader,
54
55
        tcHsLiftedType,   tcHsOpenType,
        tcHsLiftedTypeNC, tcHsOpenTypeNC,
Alan Zimmerman's avatar
Alan Zimmerman committed
56
        tcInferLHsType, tcInferLHsTypeKind, tcInferLHsTypeUnsaturated,
57
        tcCheckLHsType,
58
        tcHsContext, tcLHsPredType,
batterseapower's avatar
batterseapower committed
59

60
        kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
61

62
        -- Sort-checking kinds
63
        tcLHsKindSig, checkDataKindSig, DataSort(..),
64
        checkClassKindSig,
65

Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
66
67
68
        -- Multiplicity
        tcMult,

69
        -- Pattern type signatures
70
        tcHsPatSigType,
71
        HoleMode(..),
Tobias Dammers's avatar
Tobias Dammers committed
72
73
74

        -- Error messages
        funAppCtxt, addTyConFlavCtxt
75
76
   ) where

77
import GHC.Prelude
78

Sylvain Henry's avatar
Sylvain Henry committed
79
import GHC.Hs
80
import GHC.Rename.Utils
81
import GHC.Tc.Errors.Types
Sylvain Henry's avatar
Sylvain Henry committed
82
83
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Origin
Sylvain Henry's avatar
Sylvain Henry committed
84
import GHC.Core.Predicate
Sylvain Henry's avatar
Sylvain Henry committed
85
86
87
88
89
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.TcMType
import GHC.Tc.Validity
import GHC.Tc.Utils.Unify
90
import GHC.IfaceToCore
Sylvain Henry's avatar
Sylvain Henry committed
91
92
import GHC.Tc.Solver
import GHC.Tc.Utils.Zonk
Sylvain Henry's avatar
Sylvain Henry committed
93
94
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
Sylvain Henry's avatar
Sylvain Henry committed
95
import GHC.Tc.Utils.TcType
96
97
import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBindersN,
                                  tcInstInvisibleTyBinder )
Sylvain Henry's avatar
Sylvain Henry committed
98
import GHC.Core.Type
Sylvain Henry's avatar
Sylvain Henry committed
99
import GHC.Builtin.Types.Prim
100
import GHC.Types.Error
101
import GHC.Types.Name.Env
Sylvain Henry's avatar
Sylvain Henry committed
102
103
104
import GHC.Types.Name.Reader( lookupLocalRdrOcc )
import GHC.Types.Var
import GHC.Types.Var.Set
Sylvain Henry's avatar
Sylvain Henry committed
105
106
107
108
import GHC.Core.TyCon
import GHC.Core.ConLike
import GHC.Core.DataCon
import GHC.Core.Class
Sylvain Henry's avatar
Sylvain Henry committed
109
110
111
import GHC.Types.Name
-- import GHC.Types.Name.Set
import GHC.Types.Var.Env
Sylvain Henry's avatar
Sylvain Henry committed
112
import GHC.Builtin.Types
Sylvain Henry's avatar
Sylvain Henry committed
113
114
115
import GHC.Types.Basic
import GHC.Types.SrcLoc
import GHC.Types.Unique
116
import GHC.Types.Unique.FM
Sylvain Henry's avatar
Sylvain Henry committed
117
import GHC.Types.Unique.Set
118
import GHC.Utils.Misc
Sylvain Henry's avatar
Sylvain Henry committed
119
import GHC.Types.Unique.Supply
120
import GHC.Utils.Outputable
121
import GHC.Utils.Panic
122
import GHC.Utils.Panic.Plain
123
import GHC.Data.FastString
Sylvain Henry's avatar
Sylvain Henry committed
124
import GHC.Builtin.Names hiding ( wildCardName )
Sylvain Henry's avatar
Sylvain Henry committed
125
import GHC.Driver.Session
126
import qualified GHC.LanguageExtensions as LangExt
127

128
import GHC.Data.Maybe
Simon Peyton Jones's avatar
Simon Peyton Jones committed
129
import GHC.Data.Bag( unitBag )
130
import Data.List ( find )
131
import Control.Monad
132

Austin Seipp's avatar
Austin Seipp committed
133
{-
134
135
136
        ----------------------------
                General notes
        ----------------------------
137

138
139
140
141
142
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.
143

144
145
During type-checking, we perform as little validity checking as possible.
Generally, after type-checking, you will want to do validity checking, say
Sylvain Henry's avatar
Sylvain Henry committed
146
with GHC.Tc.Validity.checkValidType.
147
148
149

Validity checking
~~~~~~~~~~~~~~~~~
150
Some of the validity check could in principle be done by the kind checker,
151
152
153
154
but not all:

- During desugaring, we normalise by expanding type synonyms.  Only
  after this step can we check things like type-synonym saturation
155
156
  e.g.  type T k = k Int
        type S a = a
157
158
159
160
161
162
  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

163
- Ambiguity checks involve functional dependencies
164
165
166
167
168

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

169
170
%************************************************************************
%*                                                                      *
171
              Check types AND do validity checking
Austin Seipp's avatar
Austin Seipp committed
172
173
*                                                                      *
************************************************************************
Simon Peyton Jones's avatar
Simon Peyton Jones committed
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194

Note [Keeping implicitly quantified variables in order]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the user implicitly quantifies over variables (say, in a type
signature), we need to come up with some ordering on these variables.
This is done by bumping the TcLevel, bringing the tyvars into scope,
and then type-checking the thing_inside. The constraints are all
wrapped in an implication, which is then solved. Finally, we can
zonk all the binders and then order them with scopedSort.

It's critical to solve before zonking and ordering in order to uncover
any unifications. You might worry that this eager solving could cause
trouble elsewhere. I don't think it will. Because it will solve only
in an increased TcLevel, it can't unify anything that was mentioned
elsewhere. Additionally, we require that the order of implicitly
quantified variables is manifest by the scope of these variables, so
we're not going to learn more information later that will help order
these variables.

Note [Recipe for checking a signature]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
195
Kind-checking a user-written signature requires several steps:
Simon Peyton Jones's avatar
Simon Peyton Jones committed
196

197
198
199
200
201
202
203
204
 0. Bump the TcLevel
 1.   Bind any lexically-scoped type variables.
 2.   Generate constraints.
 3. Solve constraints.
 4. Sort any implicitly-bound variables into dependency order
 5. Promote tyvars and/or kind-generalize.
 6. Zonk.
 7. Check validity.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
205

206
207
Very similar steps also apply when kind-checking a type or class
declaration.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
208

209
210
The general pattern looks something like this.  (But NB every
specific instance varies in one way or another!)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
211

212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
    do { (tclvl, wanted, (spec_tkvs, ty))
              <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
                 bindImplicitTKBndrs_Skol sig_vars              $
                 <kind-check the type>

       ; spec_tkvs <- zonkAndScopedSort spec_tkvs

       ; reportUnsolvedEqualities skol_info spec_tkvs tclvl wanted

       ; let ty1 = mkSpecForAllTys spec_tkvs ty
       ; kvs <- kindGeneralizeAll ty1

       ; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1)

       ; checkValidType final_ty

This pattern is repeated many times in GHC.Tc.Gen.HsType,
GHC.Tc.Gen.Sig, and GHC.Tc.TyCl, with variations.  In more detail:

* pushLevelAndSolveEqualitiesX (Step 0, step 3) bumps the TcLevel,
  calls the thing inside to generate constraints, solves those
  constraints as much as possible, returning the residual unsolved
  constraints in 'wanted'.

* bindImplicitTKBndrs_Skol (Step 1) binds the user-specified type
  variables E.g.  when kind-checking f :: forall a. F a -> a we must
  bring 'a' into scope before kind-checking (F a -> a)

* zonkAndScopedSort (Step 4) puts those user-specified variables in
  the dependency order.  (For "implicit" variables the order is no
  user-specified.  E.g.  forall (a::k1) (b::k2). blah k1 and k2 are
  implicitly brought into scope.

* reportUnsolvedEqualities (Step 3 continued) reports any unsolved
  equalities, carefully wrapping them in an implication that binds the
  skolems.  We can't do that in pushLevelAndSolveEqualitiesX because
  that function doesn't have access to the skolems.

* kindGeneralize (Step 5). See Note [Kind generalisation]

* The final zonkTcTypeToType must happen after promoting/generalizing,
  because promoting and generalizing fill in metavariables.


Doing Step 3 (constraint solving) eagerly (rather than building an
implication constraint and solving later) is necessary for several
reasons:

* Exactly as for Solver.simplifyInfer: when generalising, we solve all
  the constraints we can so that we don't have to quantify over them
  or, since we don't quantify over constraints in kinds, float them
  and inhibit generalisation.

* Most signatures also bring implicitly quantified variables into
  scope, and solving is necessary to get these in the right order
  (Step 4) see Note [Keeping implicitly quantified variables in
  order]).

Note [Kind generalisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Step 5 of Note [Recipe for checking a signature], namely
kind-generalisation, is done by
    kindGeneraliseAll
    kindGeneraliseSome
    kindGeneraliseNone

Here, we have to deal with the fact that metatyvars generated in the
type will have a bumped TcLevel, because explicit foralls raise the
TcLevel. To avoid these variables from ever being visible in the
surrounding context, we must obey the following dictum:
Simon Peyton Jones's avatar
Simon Peyton Jones committed
282
283
284
285

  Every metavariable in a type must either be
    (A) generalized, or
    (B) promoted, or        See Note [Promotion in signatures]
286
287
288
289
290
291
292
293
294
295
296
297
298
    (C) a cause to error    See Note [Naughty quantification candidates]
                            in GHC.Tc.Utils.TcMType

There are three steps (look at kindGeneraliseSome):

1. candidateQTyVarsOfType finds the free variables of the type or kind,
   to generalise

2. filterConstrainedCandidates filters out candidates that appear
   in the unsolved 'wanteds', and promotes the ones that get filtered out
   thereby.

3. quantifyTyVars quantifies the remaining type variables
Simon Peyton Jones's avatar
Simon Peyton Jones committed
299
300
301
302

The kindGeneralize functions do not require pre-zonking; they zonk as they
go.

303
304
305
kindGeneraliseAll specialises for the case where step (2) is vacuous.
kindGeneraliseNone specialises for the case where we do no quantification,
but we must still promote.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
306

307
308
309
310
If you are actually doing kind-generalization, you need to bump the
level before generating constraints, as we will only generalize
variables with a TcLevel higher than the ambient one.
Hence the "pushLevel" in pushLevelAndSolveEqualities.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
311
312
313
314
315
316

Note [Promotion in signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If an unsolved metavariable in a signature is not generalized
(because we're not generalizing the construct -- e.g., pattern
sig -- or because the metavars are constrained -- see kindGeneralizeSome)
317
we need to promote to maintain (WantedTvInv) of Note [TcLevel invariants]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing
and the reinstantiating with a fresh metavariable at the current level.
So in some sense, we generalize *all* variables, but then re-instantiate
some of them.

Here is an example of why we must promote:
  foo (x :: forall a. a -> Proxy b) = ...

In the pattern signature, `b` is unbound, and will thus be brought into
scope. We do not know its kind: it will be assigned kappa[2]. Note that
kappa is at TcLevel 2, because it is invented under a forall. (A priori,
the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel
than the surrounding context.) This kappa cannot be solved for while checking
the pattern signature (which is not kind-generalized). When we are checking
the *body* of foo, though, we need to unify the type of x with the argument
type of bar. At this point, the ambient TcLevel is 1, and spotting a
matavariable with level 2 would violate the (WantedTvInv) invariant of
335
Note [TcLevel invariants]. So, instead of kind-generalizing,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
336
337
we promote the metavariable to level 1. This is all done in kindGeneralizeNone.

Austin Seipp's avatar
Austin Seipp committed
338
-}
339

Alan Zimmerman's avatar
Alan Zimmerman committed
340
funsSigCtxt :: [LocatedN Name] -> UserTypeCtxt
341
342
-- Returns FunSigCtxt, with no redundant-context-reporting,
-- form a list of located names
343
funsSigCtxt (L _ name1 : _) = FunSigCtxt name1 NoRRC
344
345
funsSigCtxt []              = panic "funSigCtxt"

Alan Zimmerman's avatar
Alan Zimmerman committed
346
addSigCtxt :: Outputable hs_ty => UserTypeCtxt -> LocatedA hs_ty -> TcM a -> TcM a
347
addSigCtxt ctxt hs_ty thing_inside
Alan Zimmerman's avatar
Alan Zimmerman committed
348
  = setSrcSpan (getLocA hs_ty) $
349
    addErrCtxt (pprSigCtxt ctxt hs_ty) $
350
351
    thing_inside

Alan Zimmerman's avatar
Alan Zimmerman committed
352
pprSigCtxt :: Outputable hs_ty => UserTypeCtxt -> LocatedA hs_ty -> SDoc
353
354
355
356
357
358
359
360
361
362
363
364
365
-- (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)

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

Alan Zimmerman's avatar
Alan Zimmerman committed
372
kcClassSigType :: [LocatedN Name] -> LHsSigType GhcRn -> TcM ()
373
-- This is a special form of tcClassSigType that is used during the
374
-- kind-checking phase to infer the kind of class variables. Cf. tc_lhs_sig_type.
375
376
377
378
379
380
381
382
383
384
-- Importantly, this does *not* kind-generalize. Consider
--   class SC f where
--     meth :: forall a (x :: f a). Proxy x -> ()
-- When instantiating Proxy with kappa, we must unify kappa := f a. But we're
-- still working out the kind of f, and thus f a will have a coercion in it.
-- Coercions block unification (Note [Equalities with incompatible kinds] in
-- TcCanonical) and so we fail to unify. If we try to kind-generalize, we'll
-- end up promoting kappa to the top level (because kind-generalization is
-- normally done right before adding a binding to the context), and then we
-- can't set kappa := f a, because a is local.
385
386
387
388
kcClassSigType names
    sig_ty@(L _ (HsSig { sig_bndrs = hs_outer_bndrs, sig_body = hs_ty }))
  = addSigCtxt (funsSigCtxt names) sig_ty $
    do { _ <- bindOuterSigTKBndrs_Tv hs_outer_bndrs    $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
389
              tcLHsType hs_ty liftedTypeKind
390
       ; return () }
391

Alan Zimmerman's avatar
Alan Zimmerman committed
392
tcClassSigType :: [LocatedN Name] -> LHsSigType GhcRn -> TcM Type
393
-- Does not do validity checking
394
395
396
tcClassSigType names sig_ty
  = addSigCtxt sig_ctxt sig_ty $
    do { (implic, ty) <- tc_lhs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
397
398
       ; emitImplication implic
       ; return ty }
399
400
401
       -- 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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
402
       --
403
404
405
406
407
408
409
410
411
412
413
414
       -- No need to fail here if the type has an error:
       --   If we're in the kind-checking phase, the solveEqualities
       --     in kcTyClGroup catches the error
       --   If we're in the type-checking phase, the solveEqualities
       --     in tcClassDecl1 gets it
       -- Failing fast here degrades the error message in, e.g., tcfail135:
       --   class Foo f where
       --     baa :: f a -> f
       -- If we fail fast, we're told that f has kind `k1` when we wanted `*`.
       -- It should be that f has kind `k2 -> *`, but we never get a chance
       -- to run the solver where the kind of f is touchable. This is
       -- painfully delicate.
415
416
417
  where
    sig_ctxt = funsSigCtxt names
    skol_info = SigTypeSkol sig_ctxt
418

419
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
420
-- Does validity checking
421
-- See Note [Recipe for checking a signature]
422
tcHsSigType ctxt sig_ty
423
  = addSigCtxt ctxt sig_ty $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
424
    do { traceTc "tcHsSigType {" (ppr sig_ty)
425

426
          -- Generalise here: see Note [Kind generalisation]
427
       ; (implic, ty) <- tc_lhs_sig_type skol_info sig_ty  (expectedKindInCtxt ctxt)
428

429
       -- Float out constraints, failing fast if not possible
Simon Peyton Jones's avatar
Simon Peyton Jones committed
430
       -- See Note [Failure in local type signatures] in GHC.Tc.Solver
431
432
       ; traceTc "tcHsSigType 2" (ppr implic)
       ; simplifyAndEmitFlatConstraints (mkImplicWC (unitBag implic))
433

Simon Peyton Jones's avatar
Simon Peyton Jones committed
434
       ; ty <- zonkTcType ty
435
       ; checkValidType ctxt ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
436
       ; traceTc "end tcHsSigType }" (ppr ty)
437
       ; return ty }
438
439
  where
    skol_info = SigTypeSkol ctxt
440

441
tc_lhs_sig_type :: SkolemInfo -> LHsSigType GhcRn
Simon Peyton Jones's avatar
Simon Peyton Jones committed
442
               -> ContextKind -> TcM (Implication, TcType)
443
444
445
-- Kind-checks/desugars an 'LHsSigType',
--   solve equalities,
--   and then kind-generalizes.
446
-- This will never emit constraints, as it uses solveEqualities internally.
447
-- No validity checking or zonking
Simon Peyton Jones's avatar
Simon Peyton Jones committed
448
-- Returns also an implication for the unsolved constraints
449
450
tc_lhs_sig_type skol_info full_hs_ty@(L loc (HsSig { sig_bndrs = hs_outer_bndrs
                                                   , sig_body = hs_ty })) ctxt_kind
Alan Zimmerman's avatar
Alan Zimmerman committed
451
  = setSrcSpanA loc $
452
    do { (tc_lvl, wanted, (exp_kind, (outer_bndrs, ty)))
453
              <- pushLevelAndSolveEqualitiesX "tc_lhs_sig_type" $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
454
                 -- See Note [Failure in local type signatures]
455
456
457
458
459
460
461
462
463
464
                 do { exp_kind <- newExpectedKind ctxt_kind
                          -- See Note [Escaping kind in type signatures]
                    ; stuff <- tcOuterTKBndrs skol_info hs_outer_bndrs $
                               tcLHsType hs_ty exp_kind
                    ; return (exp_kind, stuff) }

       -- Default any unconstrained variables free in the kind
       -- See Note [Escaping kind in type signatures]
       ; exp_kind_dvs <- candidateQTyVarsOfType exp_kind
       ; doNotQuantifyTyVars exp_kind_dvs (mk_doc exp_kind)
465

466
467
468
469
       ; traceTc "tc_lhs_sig_type" (ppr hs_outer_bndrs $$ ppr outer_bndrs)
       ; (outer_tv_bndrs :: [InvisTVBinder]) <- scopedSortOuter outer_bndrs

       ; let ty1 = mkInvisForAllTys outer_tv_bndrs ty
470

471
       ; kvs <- kindGeneralizeSome wanted ty1
472

Simon Peyton Jones's avatar
Simon Peyton Jones committed
473
474
       -- Build an implication for any as-yet-unsolved kind equalities
       -- See Note [Skolem escape in type signatures]
475
       ; implic <- buildTvImplication skol_info kvs tc_lvl wanted
Simon Peyton Jones's avatar
Simon Peyton Jones committed
476
477

       ; return (implic, mkInfForAllTys kvs ty1) }
478
479
480
481
482
483
  where
    mk_doc exp_kind tidy_env
      = do { (tidy_env2, exp_kind) <- zonkTidyTcType tidy_env exp_kind
           ; return (tidy_env2, hang (text "The kind" <+> ppr exp_kind)
                                   2 (text "of type signature:" <+> ppr full_hs_ty)) }

Simon Peyton Jones's avatar
Simon Peyton Jones committed
484

485
486

{- Note [Escaping kind in type signatures]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
487
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
Consider kind-checking the signature for `foo` (#19495):
  type family T (r :: RuntimeRep) :: TYPE r

  foo :: forall (r :: RuntimeRep). T r
  foo = ...

We kind-check the type with expected kind `TYPE delta` (see newExpectedKind),
where `delta :: RuntimeRep` is as-yet unknown. (We can't use `TYPE LiftedRep`
because we allow signatures like `foo :: Int#`.)

Suppose we are at level L currently.  We do this
  * pushLevelAndSolveEqualitiesX: moves to level L+1
  * newExpectedKind: allocates delta{L+1}
  * tcOuterTKBndrs: pushes the level again to L+2, binds skolem r{L+2}
  * kind-check the body (T r) :: TYPE delta{L+1}

Then
* We can't unify delta{L+1} with r{L+2}.
  And rightly so: skolem would escape.

* If delta{L+1} is unified with some-kind{L}, that is fine.
  This can happen
      \(x::a) -> let y :: a; y = x in ...(x :: Int#)...
  Here (x :: a :: TYPE gamma) is in the environment when we check
  the signature y::a.  We unify delta := gamma, and all is well.

* If delta{L+1} is unconstrained, we /must not/ quantify over it!
  E.g. Consider f :: Any   where Any :: forall k. k
  We kind-check this with expected kind TYPE kappa. We get
      Any @(TYPE kappa) :: TYPE kappa
  We don't want to generalise to     forall k. Any @k
  because that is ill-kinded: the kind of the body of the forall,
  (Any @k :: k) mentions the bound variable k.

  Instead we want to default it to LiftedRep.

  An alternative would be to promote it, similar to the monomorphism
  restriction, but the MR is pretty confusing.  Defaulting seems better

How does that defaulting happen?  Well, since we /currently/ default
RuntimeRep variables during generalisation, it'll happen in
kindGeneralize. But in principle we might allow generalisation over
RuntimeRep variables in future.  Moreover, what if we had
   kappa{L+1} := F alpha{L+1}
where F :: Type -> RuntimeRep.   Now it's alpha that is free in the kind
and it /won't/ be defaulted.

So we use doNotQuantifyTyVars to either default the free vars of
exp_kind (if possible), or error (if not).

Note [Skolem escape in type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Simon Peyton Jones's avatar
Simon Peyton Jones committed
540
541
tcHsSigType is tricky.  Consider (T11142)
  foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
Brian Wignall's avatar
Brian Wignall committed
542
This is ill-kinded because of a nested skolem-escape.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
543
544

That will show up as an un-solvable constraint in the implication
545
returned by buildTvImplication in tc_lhs_sig_type.  See Note [Skolem
Simon Peyton Jones's avatar
Simon Peyton Jones committed
546
547
548
escape prevention] in GHC.Tc.Utils.TcType for why it is unsolvable
(the unification variable for b's kind is untouchable).

549
Then, in GHC.Tc.Solver.simplifyAndEmitFlatConstraints (called from tcHsSigType)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
550
551
552
553
we'll try to float out the constraint, be unable to do so, and fail.
See GHC.Tc.Solver Note [Failure in local type signatures] for more
detail on this.

554
The separation between tcHsSigType and tc_lhs_sig_type is because
Simon Peyton Jones's avatar
Simon Peyton Jones committed
555
556
557
558
559
tcClassSigType wants to use the latter, but *not* fail fast, because
there are skolems from the class decl which are in scope; but it's fine
not to because tcClassDecl1 has a solveEqualities wrapped around all
the tcClassSigType calls.

560
561
562
That's why tcHsSigType does simplifyAndEmitFlatConstraints (which
fails fast) but tcClassSigType just does emitImplication (which does
not).  Ugh.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
563
564
565
566
567
568
569
570

c.f. see also Note [Skolem escape and forall-types]. The difference
is that we don't need to simplify at a forall type, only at the
top level of a signature.
-}

-- Does validity checking and zonking.
tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind)
571
572
573
tcStandaloneKindSig (L _ (StandaloneKindSig _ (L _ name) ksig))
  = addSigCtxt ctxt ksig $
    do { kind <- tc_top_lhs_type KindLevel ctxt ksig
Simon Peyton Jones's avatar
Simon Peyton Jones committed
574
575
       ; checkValidType ctxt kind
       ; return (name, kind) }
576
577
  where
   ctxt = StandaloneKindSigCtxt name
Simon Peyton Jones's avatar
Simon Peyton Jones committed
578

579
580
581
tcTopLHsType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
tcTopLHsType ctxt lsig_ty
  = tc_top_lhs_type TypeLevel ctxt lsig_ty
582

583
584
tc_top_lhs_type :: TypeOrKind -> UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
-- tc_top_lhs_type is used for kind-checking top-level LHsSigTypes where
585
586
587
588
--   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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
589
-- Used for both types and kinds
590
591
tc_top_lhs_type tyki ctxt (L loc sig_ty@(HsSig { sig_bndrs = hs_outer_bndrs
                                               , sig_body = body }))
Alan Zimmerman's avatar
Alan Zimmerman committed
592
  = setSrcSpanA loc $
593
594
595
596
597
598
599
600
601
602
603
604
    do { traceTc "tc_top_lhs_type {" (ppr sig_ty)
       ; (tclvl, wanted, (outer_bndrs, ty))
              <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type"    $
                 tcOuterTKBndrs skol_info hs_outer_bndrs $
                 do { kind <- newExpectedKind (expectedKindInCtxt ctxt)
                    ; tc_lhs_type (mkMode tyki) body kind }

       ; outer_tv_bndrs <- scopedSortOuter outer_bndrs
       ; let ty1 = mkInvisForAllTys outer_tv_bndrs ty

       ; kvs <- kindGeneralizeAll ty1  -- "All" because it's a top-level type
       ; reportUnsolvedEqualities skol_info kvs tclvl wanted
605

606
607
       ; ze       <- mkEmptyZonkEnv NoFlexi
       ; final_ty <- zonkTcTypeToTypeX ze (mkInfForAllTys kvs ty1)
608
609
610
611
       ; traceTc "tc_top_lhs_type }" (vcat [ppr sig_ty, ppr final_ty])
       ; return final_ty }
  where
    skol_info = SigTypeSkol ctxt
612

613
-----------------
614
tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
615
-- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause
616
-- Returns the C, [ty1, ty2, and the kinds of C's remaining arguments
617
618
-- E.g.    class C (a::*) (b::k->k)
--         data T a b = ... deriving( C Int )
619
--    returns ([k], C, [k, Int], [k->k])
620
-- Return values are fully zonked
621
tcHsDeriv hs_ty
622
623
  = do { ty <- checkNoErrs $  -- Avoid redundant error report
                              -- with "illegal deriving", below
624
               tcTopLHsType DerivClauseCtxt hs_ty
625
       ; let (tvs, pred)    = splitForAllTyCoVars ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
626
             (kind_args, _) = splitFunTys (tcTypeKind pred)
627
       ; case getClassPredTys_maybe pred of
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
628
           Just (cls, tys) -> return (tvs, cls, tys, map scaledThing kind_args)
629
630
           Nothing -> failWithTc $ TcRnUnknownMessage $ mkPlainError noHints $
             (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
631

632
633
634
635
636
637
638
639
640
641
-- | Typecheck a deriving strategy. For most deriving strategies, this is a
-- no-op, but for the @via@ strategy, this requires typechecking the @via@ type.
tcDerivStrategy ::
     Maybe (LDerivStrategy GhcRn)
     -- ^ The deriving strategy
  -> TcM (Maybe (LDerivStrategy GhcTc), [TyVar])
     -- ^ The typechecked deriving strategy and the tyvars that it binds
     -- (if using 'ViaStrategy').
tcDerivStrategy mb_lds
  = case mb_lds of
Ryan Scott's avatar
Ryan Scott committed
642
      Nothing -> boring_case Nothing
643
      Just (L loc ds) ->
644
645
        setSrcSpan loc $ do
          (ds', tvs) <- tc_deriv_strategy ds
646
          pure (Just (L loc ds'), tvs)
Ryan Scott's avatar
Ryan Scott committed
647
648
  where
    tc_deriv_strategy :: DerivStrategy GhcRn
649
                      -> TcM (DerivStrategy GhcTc, [TyVar])
Alan Zimmerman's avatar
Alan Zimmerman committed
650
651
652
653
654
655
    tc_deriv_strategy (StockStrategy    _)
                                     = boring_case (StockStrategy noExtField)
    tc_deriv_strategy (AnyclassStrategy _)
                                     = boring_case (AnyclassStrategy noExtField)
    tc_deriv_strategy (NewtypeStrategy  _)
                                     = boring_case (NewtypeStrategy noExtField)
Ryan Scott's avatar
Ryan Scott committed
656
    tc_deriv_strategy (ViaStrategy ty) = do
657
      ty' <- checkNoErrs $ tcTopLHsType DerivClauseCtxt ty
658
      let (via_tvs, via_pred) = splitForAllTyCoVars ty'
659
660
661
662
      pure (ViaStrategy via_pred, via_tvs)

    boring_case :: ds -> TcM (ds, [TyVar])
    boring_case ds = pure (ds, [])
Ryan Scott's avatar
Ryan Scott committed
663

664
tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
665
                -> LHsSigType GhcRn
666
                -> TcM Type
667
-- Like tcHsSigType, but for a class instance declaration
668
tcHsClsInstType user_ctxt hs_inst_ty
Alan Zimmerman's avatar
Alan Zimmerman committed
669
  = setSrcSpan (getLocA hs_inst_ty) $
670
671
672
673
674
    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 $
675
                    tcTopLHsType user_ctxt hs_inst_ty
676
677
       ; checkValidInstance user_ctxt hs_inst_ty inst_ty
       ; return inst_ty }
678

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
679
680
----------------------------------------------
-- | Type-check a visible type application
681
tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
Sylvain Henry's avatar
Sylvain Henry committed
682
-- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
683
tcHsTypeApp wc_ty kind
684
  | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
685
686
687
  = do { mode <- mkHoleMode TypeLevel HM_VTA
                 -- HM_VTA: See Note [Wildcards in visible type application]
       ; ty <- addTypeCtxt hs_ty                  $
688
               solveEqualities "tcHsTypeApp" $
689
690
               -- We are looking at a user-written type, very like a
               -- signature so we want to solve its equalities right now
691
               bindNamedWildCardBinders sig_wcs $ \ _ ->
Simon Peyton Jones's avatar
Simon Peyton Jones committed
692
693
               tc_lhs_type mode hs_ty kind

694
695
696
697
698
699
700
       -- We do not kind-generalize type applications: we just
       -- instantiate with exactly what the user says.
       -- See Note [No generalization in type application]
       -- We still must call kindGeneralizeNone, though, according
       -- to Note [Recipe for checking a signature]
       ; kindGeneralizeNone ty
       ; ty <- zonkTcType ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
701
702
703
       ; checkValidType TypeAppCtxt ty
       ; return ty }

My Nguyen's avatar
My Nguyen committed
704
705
{- Note [Wildcards in visible type application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
706
707
A HsWildCardBndrs's hswc_ext now only includes /named/ wildcards, so
any unnamed wildcards stay unchanged in hswc_body.  When called in
Richard Eisenberg's avatar
Richard Eisenberg committed
708
tcHsTypeApp, tcCheckLHsType will call emitAnonTypeHole
709
710
711
712
713
714
715
on these anonymous wildcards. However, this would trigger
error/warning when an anonymous 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
716
application] and Note [The wildcard story for types] in GHC.Hs.Type
717
718

Ugh!
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734

Note [No generalization in type application]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We do not kind-generalize type applications. Imagine

  id @(Proxy Nothing)

If we kind-generalized, we would get

  id @(forall {k}. Proxy @(Maybe k) (Nothing @k))

which is very sneakily impredicative instantiation.

There is also the possibility of mentioning a wildcard
(`id @(Proxy _)`), which definitely should not be kind-generalized.

My Nguyen's avatar
My Nguyen committed
735
736
-}

Simon Peyton Jones's avatar
Simon Peyton Jones committed
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
tcFamTyPats :: TyCon
            -> HsTyPats GhcRn                -- Patterns
            -> TcM (TcType, TcKind)          -- (lhs_type, lhs_kind)
-- Check the LHS of a type/data family instance
-- e.g.   type instance F ty1 .. tyn = ...
-- Used for both type and data families
tcFamTyPats fam_tc hs_pats
  = do { traceTc "tcFamTyPats {" $
         vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ]

       ; mode <- mkHoleMode TypeLevel HM_FamPat
                 -- HM_FamPat: See Note [Wildcards in family instances] in
                 -- GHC.Rename.Module
       ; let fun_ty = mkTyConApp fam_tc []
       ; (fam_app, res_kind) <- tcInferTyApps mode lhs_fun fun_ty hs_pats

753
754
755
       -- Hack alert: see Note [tcFamTyPats: zonking the result kind]
       ; res_kind <- zonkTcType res_kind

Simon Peyton Jones's avatar
Simon Peyton Jones committed
756
757
758
759
760
761
762
       ; traceTc "End tcFamTyPats }" $
         vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ]

       ; return (fam_app, res_kind) }
  where
    fam_name  = tyConName fam_tc
    fam_arity = tyConArity fam_tc
Alan Zimmerman's avatar
Alan Zimmerman committed
763
    lhs_fun   = noLocA (HsTyVar noAnn NotPromoted (noLocA fam_name))
Simon Peyton Jones's avatar
Simon Peyton Jones committed
764

765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
{- Note [tcFamTyPats: zonking the result kind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#19250)
    F :: forall k. k -> k
    type instance F (x :: Constraint) = ()

The tricky point is this:
  is that () an empty type tuple (() :: Type), or
  an empty constraint tuple (() :: Constraint)?
We work this out in a hacky way, by looking at the expected kind:
see Note [Inferring tuple kinds].

In this case, we kind-check the RHS using the kind gotten from the LHS:
see the call to tcCheckLHsType in tcTyFamInstEqnGuts in GHC.Tc.Tycl.

But we want the kind from the LHS to be /zonked/, so that when
kind-checking the RHS (tcCheckLHsType) we can "see" what we learned
from kind-checking the LHS (tcFamTyPats).  In our example above, the
type of the LHS is just `kappa` (by instantiating the forall k), but
then we learn (from x::Constraint) that kappa ~ Constraint.  We want
that info when kind-checking the RHS.

Easy solution: just zonk that return kind.  Of course this won't help
if there is lots of type-family reduction to do, but it works fine in
common cases.
-}


Austin Seipp's avatar
Austin Seipp committed
793
794
795
{-
************************************************************************
*                                                                      *
796
            The main kind checker: no validity checks here
Richard Eisenberg's avatar
Richard Eisenberg committed
797
798
*                                                                      *
************************************************************************
Austin Seipp's avatar
Austin Seipp committed
799
-}
800

dreixel's avatar
dreixel committed
801
---------------------------
802
tcHsOpenType, tcHsLiftedType,
803
  tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
804
805
-- Used for type signatures
-- Do not do validity checking
806
807
tcHsOpenType   hs_ty = addTypeCtxt hs_ty $ tcHsOpenTypeNC hs_ty
tcHsLiftedType hs_ty = addTypeCtxt hs_ty $ tcHsLiftedTypeNC hs_ty
808

809
810
tcHsOpenTypeNC   hs_ty = do { ek <- newOpenTypeKind; tcLHsType hs_ty ek }
tcHsLiftedTypeNC hs_ty = tcLHsType hs_ty liftedTypeKind
811
812

-- Like tcHsType, but takes an expected kind
813
tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
814
tcCheckLHsType hs_ty exp_kind
815
  = addTypeCtxt hs_ty $
816
    do { ek <- newExpectedKind exp_kind
Simon Peyton Jones's avatar
Simon Peyton Jones committed
817
       ; tcLHsType hs_ty ek }
818

Simon Peyton Jones's avatar
Simon Peyton Jones committed
819
820
tcInferLHsType :: LHsType GhcRn -> TcM TcType
tcInferLHsType hs_ty
821
  = do { (ty,_kind) <- tcInferLHsTypeKind hs_ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
822
       ; return ty }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
823

824
825
826
827
828
tcInferLHsTypeKind :: LHsType GhcRn -> TcM (TcType, TcKind)
-- Called from outside: set the context
-- Eagerly instantiate any trailing invisible binders
tcInferLHsTypeKind lhs_ty@(L loc hs_ty)
  = addTypeCtxt lhs_ty $
Alan Zimmerman's avatar
Alan Zimmerman committed
829
    setSrcSpanA loc    $  -- Cover the tcInstInvisibleTyBinders
830
    do { (res_ty, res_kind) <- tc_infer_hs_type typeLevelMode hs_ty
831
832
833
       ; tcInstInvisibleTyBinders res_ty res_kind }
  -- See Note [Do not always instantiate eagerly in types]

Simon Peyton Jones's avatar
Simon Peyton Jones committed
834
835
836
-- Used to check the argument of GHCi :kind
-- Allow and report wildcards, e.g. :kind T _
-- Do not saturate family applications: see Note [Dealing with :kind]
837
-- Does not instantiate eagerly; See Note [Do not always instantiate eagerly in types]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
838
839
tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcInferLHsTypeUnsaturated hs_ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
840
  = addTypeCtxt hs_ty $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
841
842
843
844
845
846
847
848
849
    do { mode <- mkHoleMode TypeLevel HM_Sig  -- Allow and report holes
       ; case splitHsAppTys (unLoc hs_ty) of
           Just (hs_fun_ty, hs_args)
              -> do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
                    ; tcInferTyApps_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]
           Nothing -> tc_infer_lhs_type mode hs_ty }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
850
851
852
853
854
855
856
857
858
859

{- 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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
860
binders (see tcInferTyApps), and we want to do so for nested application
861
even in GHCi.  Consider for example (#16287)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
862
863
864
865
866
867
  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.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
868
So tcInferLHsTypeUnsaturated does a little special case for top level
Simon Peyton Jones's avatar
Simon Peyton Jones committed
869
870
applications.  Actually the common case is a bare variable, as above.

871
872
873
874
875
876
877
878
879
880
881
882
883
Note [Do not always instantiate eagerly in types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Terms are eagerly instantiated. This means that if you say

  x = id

then `id` gets instantiated to have type alpha -> alpha. The variable
alpha is then unconstrained and regeneralized. But we cannot do this
in types, as we have no type-level lambda. So, when we are sure
that we will not want to regeneralize later -- because we are done
checking a type, for example -- we can instantiate. But we do not
instantiate at variables, nor do we in tcInferLHsTypeUnsaturated,
which is used by :kind in GHCi.
Richard Eisenberg's avatar
Richard Eisenberg committed
884

885
886
887
888
889
890
891
892
893
894
895
896
************************************************************************
*                                                                      *
      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
897
-}
898

Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
899
tcMult :: HsArrow GhcRn -> TcM Mult
900
tcMult hc = tc_mult typeLevelMode hc
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
901

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
902
903
904
905
-- | 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
906
--
Simon Peyton Jones's avatar
Simon Peyton Jones committed
907
908
909
910
911
-- To find out where the mode is used, search for 'mode_tyki'
--
-- This data type is purely local, not exported from this module
data TcTyMode
  = TcTyMode { mode_tyki :: TypeOrKind
912
             , mode_holes :: HoleInfo   }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
913

914
915
916
-- See Note [Levels for wildcards]
-- Nothing <=> no wildcards expected
type HoleInfo = Maybe (TcLevel, HoleMode)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
917
918
919
920
921
922
923
924

-- HoleMode says how to treat the occurrences
-- of anonymous wildcards; see tcAnonWildCardOcc
data HoleMode = HM_Sig      -- Partial type signatures: f :: _ -> Int
              | HM_FamPat   -- Family instances: F _ Int = Bool
              | HM_VTA      -- Visible type and kind application:
                            --   f @(Maybe _)
                            --   Maybe @(_ -> _)
925
926
927
              | HM_TyAppPat -- Visible type applications in patterns:
                            --   foo (Con @_ @t x) = ...
                            --   case x of Con @_ @t v -> ...
Simon Peyton Jones's avatar
Simon Peyton Jones committed
928
929
930
931

mkMode :: TypeOrKind -> TcTyMode
mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing }

932
933
934
935
936
typeLevelMode, kindLevelMode :: TcTyMode
-- These modes expect no wildcards (holes) in the type
kindLevelMode = mkMode KindLevel
typeLevelMode = mkMode TypeLevel

Simon Peyton Jones's avatar
Simon Peyton Jones committed
937
938
939
940
941
mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode
mkHoleMode tyki hm
  = do { lvl <- getTcLevel
       ; return (TcTyMode { mode_tyki  = tyki
                          , mode_holes = Just (lvl,hm) }) }
942

Simon Peyton Jones's avatar
Simon Peyton Jones committed
943
instance Outputable HoleMode where
944
945
946
947
  ppr HM_Sig      = text "HM_Sig"
  ppr HM_FamPat   = text "HM_FamPat"
  ppr HM_VTA      = text "HM_VTA"
  ppr HM_TyAppPat = text "HM_TyAppPat"
948

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
949
instance Outputable TcTyMode where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
950
951
952
  ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm })
    = text "TcTyMode" <+> braces (sep [ ppr tyki <> comma
                                      , ppr hm ])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
953

954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
{-
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
972
again. This is done in calls to tcInstInvisibleTyBinders.
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997

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

999
-}
1000

1001
------------------------------------------
1002
1003
1004
-- | Check and desugar a type, returning the core type and its
-- possibly-polymorphic kind. Much like 'tcInferRho' at the expression
-- level.
1005
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
1006
tc_infer_lhs_type mode (L span ty)
Alan Zimmerman's avatar
Alan Zimmerman committed
1007
  = setSrcSpanA span $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1008
    tc_infer_hs_type mode ty
1009

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1010
1011
1012
1013
1014
1015
1016
1017
---------------------------
-- | 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 }

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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1022
1023
tc_infer_hs_type mode (HsParTy _ t)
  = tc_infer_lhs_type mode t
1024

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1025
1026
tc_infer_hs_type mode ty
  | Just (hs_fun_ty, hs_args) <- splitHsAppTys ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1027
1028
  = do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
       ; tcInferTyApps mode hs_fun_ty fun_ty hs_args }
1029

1030
tc_infer_hs_type mode (HsKindSig _ ty sig)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1031
1032
  = do { let mode' = mode { mode_tyki = KindLevel }
       ; sig' <- tc_lhs_kind_sig mode' KindSigCtxt sig
1033
                 -- We must typecheck the kind signature, and solve all
1034
1035
                 -- its equalities etc; from this point on we may do
                 -- things like instantiate its foralls, so it needs
1036
                 -- to be fully determined (#14904)
1037
       ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
1038
1039
       ; ty' <- tc_lhs_type mode ty sig'
       ; return (ty', sig') }
1040

1041
-- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSpliceType' to communicate
1042
1043
1044
1045
1046
-- 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].
1047
tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
1048
  = tc_infer_hs_type mode ty
1049

1050
tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
1051

1052
1053
-- See Note [Typechecking HsCoreTys]
tc_infer_hs_type _ (XHsType ty)
1054
  = do env <- getLclEnv
1055
1056
1057
       -- Raw uniques since we go from NameEnv to TvSubstEnv.
       let subst_prs :: [(Unique, TcTyVar)]
           subst_prs = [ (getUnique nm, tv)
1058
                       | ATyVar nm tv <- nonDetNameEnvElts (tcl_env env) ]
1059
1060
           subst = mkTvSubst
                     (mkInScopeSet $ mkVarSet $ map snd subst_prs)
1061
                     (listToUFM_Directly $ map (liftSnd mkTyVarTy) subst_prs)
1062
1063
           ty' = substTy subst ty
       return (ty', tcTypeKind ty')
My Nguyen's avatar
My Nguyen committed
1064
1065
1066
1067
1068
1069
1070

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)

1071
1072
1073
1074
1075
tc_infer_hs_type mode other_ty
  = do { kv <- newMetaKindVar
       ; ty' <- tc_hs_type mode other_ty kv
       ; return (ty', kv) }

1076
{-
1077
1078
1079
1080
Note [Typechecking HsCoreTys]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
HsCoreTy is an escape hatch that allows embedding Core Types in HsTypes.
As such, there's not much to be done in order to typecheck an HsCoreTy,
1081
1082
1083
since it's already been typechecked to some extent. There is one thing that
we must do, however: we must substitute the type variables from the tcl_env.
To see why, consider GeneralizedNewtypeDeriving, which is one of the main
1084
clients of HsCoreTy (example adapted from #14579):
1085
1086
1087
1088
1089
1090

  newtype T a = MkT a deriving newtype Eq

This will produce an InstInfo GhcPs that looks roughly like this:

  instance forall a_1. Eq a_1 => Eq (T a_1) where
1091
    (==) = coerce @(  a_1 ->   a_1 -> Bool) -- The type within @(...) is an HsCoreTy
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
                  @(T a_1 -> T a_1 -> Bool) -- So is this
                  (==)

This is then fed into the renamer. Since all of the type variables in this
InstInfo use Exact RdrNames, the resulting InstInfo GhcRn looks basically
identical. Things get more interesting when the InstInfo is fed into the
typechecker, however. GHC will first generate fresh skolems to instantiate
the instance-bound type variables with. In the example above, we might generate
the skolem a_2 and use that to instantiate a_1, which extends the local type
environment (tcl_env) with [a_1 :-> a_2]. This gives us:

  instance forall a_2. Eq a_2 => Eq (T a_2) where ...

To ensure that the body of this instance is well scoped, every occurrence of
the `a` type variable should refer to a_2, the new skolem. However, the
1107
HsCoreTys mention a_1, not a_2. Luckily, the tcl_env provides exactly the
1108
substitution we need ([a_1 :-> a_2]) to fix up the scoping. We apply this
1109
substitution to each HsCoreTy and all is well:
1110
1111
1112
1113
1114
1115
1116

  instance forall a_2. Eq a_2 => Eq (T a_2) where
    (==) = coerce @(  a_2 ->   a_2 -> Bool)
                  @(T a_2 -> T a_2 -> Bool)
                  (==)
-}

1117
------------------------------------------
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1118
1119
tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType
tcLHsType hs_ty exp_kind
1120
  = tc_lhs_type typeLevelMode hs_ty exp_kind
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1121

1122
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
1123
tc_lhs_type mode (L span ty) exp_kind
Alan Zimmerman's avatar
Alan Zimmerman committed
1124
  = setSrcSpanA span $
1125
    tc_hs_type mode ty exp_kind
1126

1127
tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
1128
1129
-- See Note [Bidirectional type checking]

1130
1131
1132
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 _) _
1133
1134
    -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
    -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of