TcHsType.lhs 71.7 KB
Newer Older
1
2
%
% (c) The University of Glasgow 2006
3
4
5
6
7
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section[TcMonoType]{Typechecking user-specified @MonoTypes@}

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
8
9
10
11
12
13
14
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

15
module TcHsType (
16
	tcHsSigType, tcHsSigTypeNC, tcHsDeriv, tcHsVectInst, 
17
	tcHsInstHead, 
18
19
	UserTypeCtxt(..), 

20
                -- Type checking type and class decls
21
	kcLookupKind, kcTyClTyVars, tcTyClTyVars,
22
        tcHsConArgType, tcDataKindSig, 
23
        tcClassSigType,
dreixel's avatar
dreixel committed
24

25
26
		-- Kind-checking types
                -- No kind generalisation, no checkValidType
27
28
	KindCheckingStrategy(..), kcStrategy, kcStrategyFamDecl,
        kcHsTyVarBndrs, tcHsTyVarBndrs, 
29
        tcHsLiftedType, tcHsOpenType,
30
31
	tcLHsType, tcCheckLHsType, 
        tcHsContext, tcInferApps, tcHsArgTys,
batterseapower's avatar
batterseapower committed
32

33
        kindGeneralize, checkKind,
34
35
36

		-- Sort-checking kinds
	tcLHsKind, 
37

38
39
		-- Pattern type signatures
	tcHsPatSigType, tcPatSig
40
41
42
43
   ) where

#include "HsVersions.h"

44
#ifdef GHCI 	/* Only if bootstrapped */
45
import {-# SOURCE #-}	TcSplice( tcSpliceType )
46
47
#endif

48
import HsSyn
49
import TcRnMonad
50
import TcEvidence( HsWrapper )
51
52
import TcEnv
import TcMType
53
import TcValidity
54
55
56
import TcUnify
import TcIface
import TcType
57
import Type
58
import TypeRep( Type(..) )  -- For the mkNakedXXX stuff
dreixel's avatar
dreixel committed
59
import Kind
60
import Var
61
import VarSet
62
import TyCon
63
import DataCon
dreixel's avatar
dreixel committed
64
import TysPrim ( liftedTypeKindTyConName, constraintKindTyConName )
65
66
import Class
import Name
67
import NameEnv
68
69
70
import TysWiredIn
import BasicTypes
import SrcLoc
71
import ErrUtils ( isEmptyMessages )
72
import DynFlags ( ExtensionFlag( Opt_DataKinds ), getDynFlags )
73
import Unique
74
import UniqSupply
75
import Outputable
76
import FastString
77
78
import Util

79
import Control.Monad ( unless, when, zipWithM )
80
import PrelNames( ipClassName, funTyConKey )
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
\end{code}


	----------------------------
		General notes
	----------------------------

Generally speaking we now type-check types in three phases

  1.  kcHsType: kind check the HsType
	*includes* performing any TH type splices;
	so it returns a translated, and kind-annotated, type

  2.  dsHsType: convert from HsType to Type:
	perform zonking
	expand type synonyms [mkGenTyApps]
	hoist the foralls [tcHsType]

  3.  checkValidType: check the validity of the resulting type

Often these steps are done one after the other (tcHsSigType).
But in mutually recursive groups of type and class decls we do
	1 kind-check the whole group
	2 build TyCons/Classes in a knot-tied way
	3 check the validity of types in the now-unknotted TyCons/Classes

For example, when we find
	(forall a m. m a -> m a)
we bind a,m to kind varibles and kind-check (m a -> m a).  This makes
a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a) in
an environment that binds a and m suitably.

The kind checker passed to tcHsTyVars needs to look at enough to
establish the kind of the tyvar:
  * For a group of type and class decls, it's just the group, not
	the rest of the program
  * For a tyvar bound in a pattern type signature, its the types
	mentioned in the other type signatures in that bunch of patterns
  * For a tyvar bound in a RULE, it's the type signatures on other
	universally quantified variables in the rule

Note that this may occasionally give surprising results.  For example:

	data T a b = MkT (a b)

Here we deduce			a::*->*,       b::*
But equally valid would be	a::(*->*)-> *, b::*->*


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

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


%************************************************************************
%*									*
162
              Check types AND do validity checking
163
164
165
166
%*									*
%************************************************************************

\begin{code}
167
tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
168
169
170
  -- NB: it's important that the foralls that come from the top-level
  --	 HsForAllTy in hs_ty occur *first* in the returned type.
  --     See Note [Scoped] with TcSigInfo
171
tcHsSigType ctxt hs_ty
172
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
173
174
    tcHsSigTypeNC ctxt hs_ty

175
176
177
178
179
180
tcHsSigTypeNC ctxt (L loc hs_ty)
  = setSrcSpan loc $    -- The "In the type..." context
                        -- comes from the caller; hence "NC"
    do  { kind <- case expectedKindInCtxt ctxt of
                    Nothing -> newMetaKindVar
                    Just k  -> return k
181
182
          -- The kind is checked by checkValidType, and isn't necessarily
          -- of kind * in a Template Haskell quote eg [t| Maybe |]
183

184
          -- Generalise here: see Note [Kind generalisation]
185
        ; ty <- tcCheckHsTypeAndGen hs_ty kind
dreixel's avatar
dreixel committed
186

187
          -- Zonk to expose kind information to checkValidType
188
        ; ty <- zonkSigType ty
189
190
        ; checkValidType ctxt ty
        ; return ty }
dreixel's avatar
dreixel committed
191

192
-----------------
dreixel's avatar
dreixel committed
193
tcHsInstHead :: UserTypeCtxt -> LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
194
-- Like tcHsSigTypeNC, but for an instance head.
195
tcHsInstHead user_ctxt lhs_ty@(L loc hs_ty)
196
  = setSrcSpan loc $    -- The "In the type..." context comes from the caller
197
    do { inst_ty <- tc_inst_head hs_ty
198
       ; kvs     <- zonkTcTypeAndFV inst_ty
199
       ; kvs     <- kindGeneralize kvs
200
       ; inst_ty <- zonkSigType (mkForAllTys kvs inst_ty)
201
202
203
204
205
206
207
208
209
210
211
       ; checkValidInstance user_ctxt lhs_ty inst_ty }

tc_inst_head :: HsType Name -> TcM TcType
tc_inst_head (HsForAllTy _ hs_tvs hs_ctxt hs_ty)
  = tcHsTyVarBndrs hs_tvs $ \ tvs -> 
    do { ctxt <- tcHsContext hs_ctxt
       ; ty   <- tc_lhs_type hs_ty ekConstraint    -- Body for forall has kind Constraint
       ; return (mkSigmaTy tvs ctxt ty) }

tc_inst_head hs_ty
  = tc_hs_type hs_ty ekConstraint
batterseapower's avatar
batterseapower committed
212

213
214
215
216
217
218
219
220
221
-----------------
tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
-- Like tcHsSigTypeNC, but for the ...deriving( ty ) clause
tcHsDeriv hs_ty 
  = do { kind <- newMetaKindVar
       ; ty   <- tcCheckHsTypeAndGen hs_ty kind
                 -- Funny newtype deriving form
                 -- 	forall a. C [a]
                 -- where C has arity 2. Hence any-kinded result
222
       ; ty   <- zonkSigType ty
223
224
225
       ; let (tvs, pred) = splitForAllTys ty
       ; case getClassPredTys_maybe pred of
           Just (cls, tys) -> return (tvs, cls, tys)
226
           Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) }
227
228
229
230
231
232

-- Used for 'VECTORISE [SCALAR] instance' declarations
--
tcHsVectInst :: LHsType Name -> TcM (Class, [Type])
tcHsVectInst ty
  | Just (L _ cls_name, tys) <- splitLHsClassTy_maybe ty
233
234
235
  = do { (cls, cls_kind) <- tcClass cls_name
       ; (arg_tys, _res_kind) <- tcInferApps cls_name cls_kind tys
       ; return (cls, arg_tys) }
236
237
  | otherwise
  = failWithTc $ ptext (sLit "Malformed instance type")
238
239
240
241
242
243
244
245
246
\end{code}

	These functions are used during knot-tying in
	type and class declarations, when we have to
 	separate kind-checking, desugaring, and validity checking


%************************************************************************
%*									*
247
            The main kind checker: no validity checks here
248
249
250
251
252
253
%*									*
%************************************************************************
	
	First a couple of simple wrappers for kcHsType

\begin{code}
254
255
256
257
tcClassSigType :: LHsType Name -> TcM Type
tcClassSigType lhs_ty@(L _ hs_ty)
  = addTypeCtxt lhs_ty $
    do { ty <- tcCheckHsTypeAndGen hs_ty liftedTypeKind
258
       ; zonkSigType ty }
259
260
261
262
263
264
265

tcHsConArgType :: NewOrData ->  LHsType Name -> TcM Type
-- Permit a bang, but discard it
tcHsConArgType NewType  bty = tcHsLiftedType (getBangType bty)
  -- Newtypes can't have bangs, but we don't check that
  -- until checkValidDataCon, so do not want to crash here

266
tcHsConArgType DataType bty = tcHsOpenType (getBangType bty)
267
268
269
270
  -- Can't allow an unlifted type for newtypes, because we're effectively
  -- going to remove the constructor while coercing it to a lifted type.
  -- And newtypes can't be bang'd

271
---------------------------
272
273
274
275
276
277
278
279
280
281
282
tcHsArgTys :: SDoc -> [LHsType Name] -> [Kind] -> TcM [TcType]
tcHsArgTys what tys kinds
  = sequence [ addTypeCtxt ty $
               tc_lhs_type ty (expArgKind what kind n)
             | (ty,kind,n) <- zip3 tys kinds [1..] ]

tc_hs_arg_tys :: SDoc -> [LHsType Name] -> [Kind] -> TcM [TcType]
-- Just like tcHsArgTys but without the addTypeCtxt
tc_hs_arg_tys what tys kinds
  = sequence [ tc_lhs_type ty (expArgKind what kind n)
             | (ty,kind,n) <- zip3 tys kinds [1..] ]
283

dreixel's avatar
dreixel committed
284
---------------------------
285
tcHsOpenType, tcHsLiftedType :: LHsType Name -> TcM TcType
286
287
-- Used for type signatures
-- Do not do validity checking
288
tcHsOpenType ty   = addTypeCtxt ty $ tc_lhs_type ty ekOpen
289
290
291
292
293
294
tcHsLiftedType ty = addTypeCtxt ty $ tc_lhs_type ty ekLifted

-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType Name -> Kind -> TcM Type
tcCheckLHsType hs_ty exp_kind
  = addTypeCtxt hs_ty $ 
295
    tc_lhs_type hs_ty (EK exp_kind expectedKindMsg)
296
297
298
299

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

301
---------------------------
302
303
304
305
306
tcCheckHsTypeAndGen :: HsType Name -> Kind -> TcM Type
-- Input type is HsType, not LhsType; the caller adds the context
-- Typecheck a type signature, and kind-generalise it
-- The result is not necessarily zonked, and has not been checked for validity
tcCheckHsTypeAndGen hs_ty kind
307
  = do { ty  <- tc_hs_type hs_ty (EK kind expectedKindMsg)
308
309
       ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty)
       ; kvs <- zonkTcTypeAndFV ty 
310
       ; kvs <- kindGeneralize kvs
311
       ; return (mkForAllTys kvs ty) }
312
313
\end{code}

314
Like tcExpr, tc_hs_type takes an expected kind which it unifies with
dreixel's avatar
dreixel committed
315
the kind it figures out. When we don't know what kind to expect, we use
316
tc_lhs_type_fresh, to first create a new meta kind variable and use that as
dreixel's avatar
dreixel committed
317
the expected kind.
318
319

\begin{code}
320
321
322
tc_infer_lhs_type :: LHsType Name -> TcM (TcType, TcKind)
tc_infer_lhs_type ty =
  do { kv <- newMetaKindVar
323
     ; r <- tc_lhs_type ty (EK kv expectedKindMsg)
324
325
326
327
     ; return (r, kv) }

tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType
tc_lhs_type (L span ty) exp_kind
328
  = setSrcSpan span $
329
330
331
332
333
334
    do { traceTc "tc_lhs_type:" (ppr ty $$ ppr exp_kind)
       ; tc_hs_type ty exp_kind }

tc_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [TcType]
tc_lhs_types tys_w_kinds = mapM (uncurry tc_lhs_type) tys_w_kinds

335
336
337
338
339
340
341
342
343
344
345
346
------------------------------------------
tc_fun_type :: HsType Name -> LHsType Name -> LHsType Name -> ExpKind -> TcM TcType
-- We need to recognise (->) so that we can construct a FunTy, 
-- *and* we need to do by looking at the Name, not the TyCon
-- (see Note [Zonking inside the knot]).  For example,
-- consider  f :: (->) Int Int  (Trac #7312)
tc_fun_type ty ty1 ty2 exp_kind@(EK _ ctxt)
  = do { ty1' <- tc_lhs_type ty1 (EK openTypeKind ctxt)
       ; ty2' <- tc_lhs_type ty2 (EK openTypeKind ctxt)
       ; checkExpectedKind ty liftedTypeKind exp_kind
       ; return (mkFunTy ty1' ty2') }

347
348
349
350
351
------------------------------------------
tc_hs_type :: HsType Name -> ExpKind -> TcM TcType
tc_hs_type (HsParTy ty)        exp_kind = tc_lhs_type ty exp_kind
tc_hs_type (HsDocTy ty _)      exp_kind = tc_lhs_type ty exp_kind
tc_hs_type (HsQuasiQuoteTy {}) _ = panic "tc_hs_type: qq"	-- Eliminated by renamer
352
353
354
355
356
tc_hs_type ty@(HsBangTy {})    _
    -- 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)
    = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
357
358
359
360
361
362
363
364
365
366
tc_hs_type (HsRecTy _)         _ = panic "tc_hs_type: record" -- Unwrapped by con decls
      -- Record types (which only show up temporarily in constructor 
      -- signatures) should have been removed by now

---------- Functions and applications
tc_hs_type hs_ty@(HsTyVar name) exp_kind
  = do { (ty, k) <- tcTyVar name
       ; checkExpectedKind hs_ty k exp_kind
       ; return ty }

367
368
tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind
  = tc_fun_type ty ty1 ty2 exp_kind
369
370

tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind
371
372
373
  | op `hasKey` funTyConKey
  = tc_fun_type hs_ty ty1 ty2 exp_kind
  | otherwise
374
375
376
377
378
379
  = do { (op', op_kind) <- tcTyVar op
       ; tys' <- tcCheckApps hs_ty l_op op_kind [ty1,ty2] exp_kind
       ; return (mkNakedAppTys op' tys') }
         -- mkNakedAppTys: see Note [Zonking inside the knot]

tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind
380
381
382
383
384
--  | L _ (HsTyVar fun) <- fun_ty
--  , fun `hasKey` funTyConKey
--  , [fty1,fty2] <- arg_tys
--  = tc_fun_type hs_ty fty1 fty2 exp_kind
--  | otherwise
385
  = do { (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty
386
387
388
       ; arg_tys' <- tcCheckApps hs_ty fun_ty fun_kind arg_tys exp_kind
       ; return (mkNakedAppTys fun_ty' arg_tys') }
         -- mkNakedAppTys: see Note [Zonking inside the knot]
Simon Peyton Jones's avatar
Simon Peyton Jones committed
389
390
391
         -- This looks fragile; how do we *know* that fun_ty isn't 
         -- a TyConApp, say (which is never supposed to appear in the
         -- function position of an AppTy)?
392
393
  where
    (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
394
395

--------- Foralls
396
tc_hs_type hs_ty@(HsForAllTy _ hs_tvs context ty) exp_kind
397
398
399
  = tcHsTyVarBndrs hs_tvs $ \ tvs' -> 
    -- Do not kind-generalise here!  See Note [Kind generalisation]
    do { ctxt' <- tcHsContext context
400
401
402
403
       ; ty' <- if null (unLoc context) then  -- Plain forall, no context
                   tc_lhs_type ty exp_kind    -- Why exp_kind?  See Note [Body kind of forall]
                else     
                   -- If there is a context, then this forall is really a
404
                   -- _function_, so the kind of the result really is *
405
406
407
                   -- The body kind (result of the function can be * or #, hence ekOpen
                   do { checkExpectedKind hs_ty liftedTypeKind exp_kind
                      ; tc_lhs_type ty ekOpen }
408
409
410
411
412
413
414
415
416
417
418
419
420
421
       ; return (mkSigmaTy tvs' ctxt' ty') }

--------- Lists, arrays, and tuples
tc_hs_type hs_ty@(HsListTy elt_ty) exp_kind 
  = do { tau_ty <- tc_lhs_type elt_ty ekLifted
       ; checkExpectedKind hs_ty liftedTypeKind exp_kind
       ; checkWiredInTyCon listTyCon
       ; return (mkListTy tau_ty) }

tc_hs_type hs_ty@(HsPArrTy elt_ty) exp_kind
  = do { tau_ty <- tc_lhs_type elt_ty ekLifted
       ; checkExpectedKind hs_ty liftedTypeKind exp_kind
       ; checkWiredInTyCon parrTyCon
       ; return (mkPArrTy tau_ty) }
422

dreixel's avatar
dreixel committed
423
-- See Note [Distinguishing tuple kinds] in HsTypes
424
425
426
427
428
-- See Note [Inferring tuple kinds]
tc_hs_type hs_ty@(HsTupleTy HsBoxedOrConstraintTuple tys) exp_kind@(EK exp_k _ctxt)
     -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
  | isConstraintKind exp_k = tc_tuple hs_ty HsConstraintTuple tys exp_kind
  | isLiftedTypeKind exp_k = tc_tuple hs_ty HsBoxedTuple      tys exp_kind
dreixel's avatar
dreixel committed
429
430
  | otherwise
  = do { k <- newMetaKindVar
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
       ; (msgs, mb_tau_tys) <- tryTc (tc_hs_arg_tys (ptext (sLit "a tuple")) tys (repeat k))
       ; k <- zonkTcKind k
           -- Do the experiment inside a 'tryTc' because errors can be
           -- confusing.  Eg Trac #7410 (Either Int, Int), we do not want to get
           -- an error saying "the second argument of a tuple should have kind *->*"

       ; case mb_tau_tys of
           Just tau_tys 
             | not (isEmptyMessages msgs) -> try_again k
             | isConstraintKind k         -> go_for HsConstraintTuple tau_tys
             | isLiftedTypeKind k         -> go_for HsBoxedTuple      tau_tys
             | otherwise                  -> try_again k
           Nothing                        -> try_again k }
   where
     go_for sort tau_tys = finish_tuple hs_ty sort tau_tys exp_kind

     try_again k
       | isConstraintKind k = tc_tuple hs_ty HsConstraintTuple tys exp_kind
       | otherwise          = tc_tuple hs_ty HsBoxedTuple      tys exp_kind
         -- It's not clear what the kind is, so make best guess and
451
         -- check the arguments again to give good error messages
dreixel's avatar
dreixel committed
452
453
         -- in eg. `(Maybe, Maybe)`

454
455
tc_hs_type hs_ty@(HsTupleTy tup_sort tys) exp_kind
  = tc_tuple hs_ty tup_sort tys exp_kind
dreixel's avatar
dreixel committed
456

457
458
459
460
461
462
463
464
--------- Promoted lists and tuples
tc_hs_type hs_ty@(HsExplicitListTy _k tys) exp_kind
  = do { tks <- mapM tc_infer_lhs_type tys
       ; let taus = map fst tks
       ; kind <- unifyKinds (ptext (sLit "In a promoted list")) tks
       ; checkExpectedKind hs_ty (mkPromotedListTy kind) exp_kind
       ; return (foldr (mk_cons kind) (mk_nil kind) taus) }
  where
465
466
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
467
468
469
470
471
472
473
474
475
476
477
478
479

tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
  = do { tks <- mapM tc_infer_lhs_type tys
       ; let n          = length tys
             kind_con   = promotedTupleTyCon   BoxedTuple n
             ty_con     = promotedTupleDataCon BoxedTuple n
             (taus, ks) = unzip tks
             tup_k      = mkTyConApp kind_con ks
       ; checkExpectedKind hs_ty tup_k exp_kind
       ; return (mkTyConApp ty_con (ks ++ taus)) }

--------- Constraint types
tc_hs_type ipTy@(HsIParamTy n ty) exp_kind
480
  = do { ty' <- tc_lhs_type ty ekLifted
481
       ; checkExpectedKind ipTy constraintKind exp_kind
482
483
484
485
       ; ipClass <- tcLookupClass ipClassName
       ; let n' = mkStrLitTy $ hsIPNameFS n
       ; return (mkClassPred ipClass [n',ty'])
       }
486
487
488
489
490

tc_hs_type ty@(HsEqTy ty1 ty2) exp_kind 
  = do { (ty1', kind1) <- tc_infer_lhs_type ty1
       ; (ty2', kind2) <- tc_infer_lhs_type ty2
       ; checkExpectedKind ty2 kind2
491
              (EK kind1 msg_fn)
492
493
       ; checkExpectedKind ty constraintKind exp_kind
       ; return (mkNakedTyConApp eqTyCon [kind1, ty1', ty2']) }
494
495
496
  where
    msg_fn pkind = ptext (sLit "The left argument of the equality had kind")
                   <+> quotes (pprKind pkind)
497
498
499
500
501

--------- Misc
tc_hs_type (HsKindSig ty sig_k) exp_kind 
  = do { sig_k' <- tcLHsKind sig_k
       ; checkExpectedKind ty sig_k' exp_kind
502
503
504
505
       ; tc_lhs_type ty (EK sig_k' msg_fn) }
  where
    msg_fn pkind = ptext (sLit "The signature specified kind") 
                   <+> quotes (pprKind pkind)
506
507
508
509

tc_hs_type (HsCoreTy ty) exp_kind
  = do { checkExpectedKind ty (typeKind ty) exp_kind
       ; return ty }
dreixel's avatar
dreixel committed
510
511


512
#ifdef GHCI	/* Only if bootstrapped */
513
514
515
-- This looks highly suspect to me
-- It will really only be fixed properly when we do the TH
-- reorganisation so that type splices happen in the renamer
516
tc_hs_type hs_ty@(HsSpliceTy sp fvs _) exp_kind 
517
518
519
  = do { s <- getStage
       ; traceTc "tc_hs_type: splice" (ppr sp $$ ppr s) 
       ; (ty, kind) <- tcSpliceType sp fvs
520
521
522
523
524
525
526
527
528
529
       ; checkExpectedKind hs_ty kind exp_kind
--                     -- See Note [Kind of a type splice]
       ; return ty }
#else
tc_hs_type ty@(HsSpliceTy {}) _exp_kind 
  = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
#endif

tc_hs_type (HsWrapTy {}) _exp_kind 
  = panic "tc_hs_type HsWrapTy"  -- We kind checked something twice
dreixel's avatar
dreixel committed
530

531
532
533
534
535
536
tc_hs_type hs_ty@(HsTyLit (HsNumTy n)) exp_kind 
  = do { checkExpectedKind hs_ty typeNatKind exp_kind
       ; checkWiredInTyCon typeNatKindCon
       ; return (mkNumLitTy n) }

tc_hs_type hs_ty@(HsTyLit (HsStrTy s)) exp_kind 
537
538
  = do { checkExpectedKind hs_ty typeSymbolKind exp_kind
       ; checkWiredInTyCon typeSymbolKindCon
539
       ; return (mkStrLitTy s) }
540

541
542
543
544
545
546
---------------------------
tc_tuple :: HsType Name -> HsTupleSort -> [LHsType Name] -> ExpKind -> TcM TcType
-- Invariant: tup_sort is not HsBoxedOrConstraintTuple
tc_tuple hs_ty tup_sort tys exp_kind
  = do { tau_tys <- tc_hs_arg_tys cxt_doc tys (repeat arg_kind)
       ; finish_tuple hs_ty tup_sort tau_tys exp_kind }
dreixel's avatar
dreixel committed
547
548
549
  where
    arg_kind = case tup_sort of
                 HsBoxedTuple      -> liftedTypeKind
550
                 HsUnboxedTuple    -> openTypeKind
dreixel's avatar
dreixel committed
551
                 HsConstraintTuple -> constraintKind
552
                 _                 -> panic "tc_hs_type arg_kind"
dreixel's avatar
dreixel committed
553
554
555
556
    cxt_doc = case tup_sort of
                 HsBoxedTuple      -> ptext (sLit "a tuple")
                 HsUnboxedTuple    -> ptext (sLit "an unboxed tuple")
                 HsConstraintTuple -> ptext (sLit "a constraint tuple")
557
                 _                 -> panic "tc_hs_type tup_sort"
dreixel's avatar
dreixel committed
558

559
560
561
562
563
564
565
566
567
568
569
570
571
572
finish_tuple :: HsType Name -> HsTupleSort -> [TcType] -> ExpKind -> TcM TcType
finish_tuple hs_ty tup_sort tau_tys exp_kind
  = do { checkExpectedKind hs_ty res_kind exp_kind
       ; checkWiredInTyCon tycon
       ; return (mkTyConApp tycon tau_tys) }
  where
    tycon = tupleTyCon con (length tau_tys)
    con = case tup_sort of
            HsUnboxedTuple    -> UnboxedTuple
            HsBoxedTuple      -> BoxedTuple
            HsConstraintTuple -> ConstraintTuple
            _                 -> panic "tc_hs_type HsTupleTy"

    res_kind = case tup_sort of
573
                 HsUnboxedTuple    -> unliftedTypeKind
574
575
576
                 HsBoxedTuple      -> liftedTypeKind
                 HsConstraintTuple -> constraintKind
                 _                 -> panic "tc_hs_type arg_kind"
577

578
---------------------------
579
tcInferApps :: Outputable a
580
581
       => a 
       -> TcKind			-- Function kind
582
       -> [LHsType Name]		-- Arg types
583
584
585
586
       -> TcM ([TcType], TcKind)	-- Kind-checked args
tcInferApps the_fun fun_kind args
  = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) fun_kind args
       ; args' <- tc_lhs_types args_w_kinds
587
588
       ; return (args', res_kind) }

589
590
591
592
593
594
595
596
597
598
tcCheckApps :: Outputable a 
            => HsType Name     -- The type being checked (for err messages only)
            -> a               -- The function
            -> TcKind -> [LHsType Name]   -- Fun kind and arg types
	    -> ExpKind 	                  -- Expected kind
	    -> TcM [TcType]
tcCheckApps hs_ty the_fun fun_kind args exp_kind
  = do { (arg_tys, res_kind) <- tcInferApps the_fun fun_kind args
       ; checkExpectedKind hs_ty res_kind exp_kind
       ; return arg_tys }
599

600
---------------------------
601
602
603
splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
splitFunKind the_fun fun_kind args
  = go 1 fun_kind args
604
  where
605
606
607
608
609
610
611
612
613
    go _      fk [] = return ([], fk)
    go arg_no fk (arg:args)
       = do { mb_fk <- matchExpectedFunKind fk
            ; case mb_fk of
                 Nothing       -> failWithTc too_many_args 
                 Just (ak,fk') -> do { (aks, rk) <- go (arg_no+1) fk' args
                                     ; let exp_kind = expArgKind (quotes the_fun) ak arg_no
                                     ; return ((arg, exp_kind) : aks, rk) } }
 
614
    too_many_args = quotes the_fun <+>
Ian Lynagh's avatar
Ian Lynagh committed
615
		    ptext (sLit "is applied to too many type arguments")
616

617

618
---------------------------
619
620
tcHsContext :: LHsContext Name -> TcM [PredType]
tcHsContext ctxt = mapM tcHsLPredType (unLoc ctxt)
621

622
623
tcHsLPredType :: LHsType Name -> TcM PredType
tcHsLPredType pred = tc_lhs_type pred ekConstraint
624
625

---------------------------
626
tcTyVar :: Name -> TcM (TcType, TcKind)
dreixel's avatar
dreixel committed
627
628
-- See Note [Type checking recursive type and class declarations]
-- in TcTyClsDecls
629
tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
dreixel's avatar
dreixel committed
630
631
632
633
  = do { traceTc "lk1" (ppr name)
       ; thing <- tcLookup name
       ; traceTc "lk2" (ppr name <+> ppr thing)
       ; case thing of
634
635
636
637
638
639
           ATyVar _ tv 
              | isKindVar tv
              -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr tv)
                             <+> ptext (sLit "used as a type"))
              | otherwise
              -> return (mkTyVarTy tv, tyVarKind tv)
640
641
642
643
644
645
646
647

           AThing kind -> do { tc <- get_loopy_tc name
                             ; inst_tycon (mkNakedTyConApp tc) kind }
                             -- mkNakedTyConApp: see Note [Zonking inside the knot]

           AGlobal (ATyCon tc) -> inst_tycon (mkTyConApp tc) (tyConKind tc)

           AGlobal (ADataCon dc)
648
             | Just tc <- promoteDataCon_maybe dc
649
650
651
             -> do { data_kinds <- xoptM Opt_DataKinds
                   ; unless data_kinds $ promotionErr name NoDataKinds
                   ; inst_tycon (mkTyConApp tc) (tyConKind tc) }
652
653
654
             | otherwise -> failWithTc (ptext (sLit "Data constructor") <+> quotes (ppr dc)
                                        <+> ptext (sLit "comes from an un-promotable type") 
                                        <+> quotes (ppr (dataConTyCon dc)))
655

656
           APromotionErr err -> promotionErr name err
657
658

           _  -> wrongThingErr "type" thing name }
dreixel's avatar
dreixel committed
659
  where
660
661
662
663
664
665
666
667
668
669
670
671
    get_loopy_tc name
      = do { env <- getGblEnv
           ; case lookupNameEnv (tcg_type_env env) name of
                Just (ATyCon tc) -> return tc
                _                -> return (aThingErr "tcTyVar" name) }

    inst_tycon :: ([Type] -> Type) -> Kind -> TcM (Type, Kind)
    -- Instantiate the polymorphic kind
    -- Lazy in the TyCon
    inst_tycon mk_tc_app kind
      | null kvs 
      = return (mk_tc_app [], ki_body)
dreixel's avatar
dreixel committed
672
673
      | otherwise
      = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind)
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
           ; ks <- mapM (const newMetaKindVar) kvs
           ; return (mk_tc_app ks, substKiWith kvs ks ki_body) }
      where 
        (kvs, ki_body) = splitForAllTys kind

tcClass :: Name -> TcM (Class, TcKind)
tcClass cls 	-- Must be a class
  = do { thing <- tcLookup cls
       ; case thing of
           AThing kind -> return (aThingErr "tcClass" cls, kind)
           AGlobal (ATyCon tc)
             | Just cls <- tyConClass_maybe tc 
             -> return (cls, tyConKind tc)
           _ -> wrongThingErr "class" thing cls }


aThingErr :: String -> Name -> b
-- The type checker for types is sometimes called simply to
-- do *kind* checking; and in that case it ignores the type
-- returned. Which is a good thing since it may not be available yet!
aThingErr str x = pprPanic "AThing evaluated unexpectedly" (text str <+> ppr x)
695
696
\end{code}

697
698
699
700
701
Note [Zonking inside the knot]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are checking the argument types of a data constructor.  We
must zonk the types before making the DataCon, because once built we
can't change it.  So we must traverse the type.
702

703
704
705
BUT the parent TyCon is knot-tied, so we can't look at it yet. 

So we must be careful not to use "smart constructors" for types that
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
look at the TyCon or Class involved.  

  * Hence the use of mkNakedXXX functions. These do *not* enforce 
    the invariants (for example that we use (FunTy s t) rather 
    than (TyConApp (->) [s,t])).  

  * Ditto in zonkTcType (which may be applied more than once, eg to
    squeeze out kind meta-variables), we are careful not to look at
    the TyCon.

  * We arrange to call zonkSigType *once* right at the end, and it
    does establish the invariants.  But in exchange we can't look
    at the result (not even its structure) until we have emerged
    from the "knot".

  * TcHsSyn.zonkTcTypeToType also can safely check/establish
    invariants.
723

724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
This is horribly delicate.  I hate it.  A good example of how
delicate it is can be seen in Trac #7903.

\begin{code}
mkNakedTyConApp :: TyCon -> [Type] -> Type
-- Builds a TyConApp 
--   * without being strict in TyCon,
--   * without satisfying the invariants of TyConApp
-- A subsequent zonking will establish the invariants
mkNakedTyConApp tc tys = TyConApp tc tys

mkNakedAppTys :: Type -> [Type] -> Type
mkNakedAppTys ty1                []   = ty1
mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
mkNakedAppTys ty1                tys2 = foldl AppTy ty1 tys2

zonkSigType :: TcType -> TcM TcType
-- Zonk the result of type-checking a user-written type signature
-- It may have kind varaibles in it, but no meta type variables
-- Because of knot-typing (see Note [Zonking inside the knot])
-- it may need to establish the Type invariants; 
-- hence the use of mkTyConApp and mkAppTy
zonkSigType ty
  = go ty
  where
    go (TyConApp tc tys) = do tys' <- mapM go tys
                              return (mkTyConApp tc tys')
                -- Key point: establish Type invariants! 
                -- See Note [Zonking inside the knot] 

    go (LitTy n)         = return (LitTy n)

    go (FunTy arg res)   = do arg' <- go arg
                              res' <- go res
                              return (FunTy arg' res')

    go (AppTy fun arg)   = do fun' <- go fun
                              arg' <- go arg
                              return (mkAppTy fun' arg')
		-- NB the mkAppTy; we might have instantiated a
		-- type variable to a type constructor, so we need
		-- to pull the TyConApp to the top.

	-- The two interesting cases!
    go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
		       | otherwise	 = TyVarTy <$> updateTyVarKindM go tyvar
		-- Ordinary (non Tc) tyvars occur inside quantified types

    go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
                             ; ty' <- go ty
                             ; return (ForAllTy tv' ty') }
\end{code}
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842

Note [Body kind of a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The body of a forall is usually a type, but in principle
there's no reason to prohibit *unlifted* types.
In fact, GHC can itself construct a function with an
unboxed tuple inside a for-all (via CPR analyis; see 
typecheck/should_compile/tc170).

Moreover in instance heads we get forall-types with
kind Constraint.  

Moreover if we have a signature
   f :: Int#
then we represent it as (HsForAll Implicit [] [] Int#).  And this must
be legal!  We can't drop the empty forall until *after* typechecking
the body because of kind polymorphism:
   Typeable :: forall k. k -> Constraint
   data Apply f t = Apply (f t)
   -- Apply :: forall k. (k -> *) -> k -> *
   instance Typeable Apply where ...
Then the dfun has type
   df :: forall k. Typeable ((k->*) -> k -> *) (Apply k)

   f :: Typeable Apply

   f :: forall (t:k->*) (a:k).  t a -> t a

   class C a b where
      op :: a b -> Typeable Apply

   data T a = MkT (Typeable Apply)
            | T2 a
      T :: * -> *
      MkT :: forall k. (Typeable ((k->*) -> k -> *) (Apply k)) -> T a

   f :: (forall (k:BOX). forall (t:: k->*) (a:k). t a -> t a) -> Int
   f :: (forall a. a -> Typeable Apply) -> Int

So we *must* keep the HsForAll on the instance type
   HsForAll Implicit [] [] (Typeable Apply)
so that we do kind generalisation on it.

Really we should check that it's a type of value kind
{*, Constraint, #}, but I'm not doing that yet
Example that should be rejected:  
         f :: (forall (a:*->*). a) Int

Note [Inferring tuple kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Give a tuple type (a,b,c), which the parser labels as HsBoxedOrConstraintTuple,
we try to figure out whether it's a tuple of kind * or Constraint.
  Step 1: look at the expected kind
  Step 2: infer argument kinds

If after Step 2 it's not clear from the arguments that it's
Constraint, then it must be *.  Once having decided that we re-check
the Check the arguments again to give good error messages
in eg. `(Maybe, Maybe)`

Note that we will still fail to infer the correct kind in this case:

  type T a = ((a,a), D a)
  type family D :: Constraint -> Constraint

While kind checking T, we do not yet know the kind of D, so we will default the
kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
843

dreixel's avatar
dreixel committed
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
Note [Desugaring types]
~~~~~~~~~~~~~~~~~~~~~~~
The type desugarer is phase 2 of dealing with HsTypes.  Specifically:

  * It transforms from HsType to Type

  * It zonks any kinds.  The returned type should have no mutable kind
    or type variables (hence returning Type not TcType):
      - any unconstrained kind variables are defaulted to AnyK just 
        as in TcHsSyn. 
      - there are no mutable type variables because we are 
        kind-checking a type
    Reason: the returned type may be put in a TyCon or DataCon where
    it will never subsequently be zonked.

You might worry about nested scopes:
        ..a:kappa in scope..
            let f :: forall b. T '[a,b] -> Int
In this case, f's type could have a mutable kind variable kappa in it;
and we might then default it to AnyK when dealing with f's type
signature.  But we don't expect this to happen because we can't get a
lexically scoped type variable with a mutable kind variable in it.  A
delicate point, this.  If it becomes an issue we might need to
distinguish top-level from nested uses.

Moreover
  * it cannot fail, 
  * it does no unifications
  * it does no validity checking, except for structural matters, such as
873
874
	(a) spurious ! annotations.
	(b) a class used as a type
875

dreixel's avatar
dreixel committed
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
Note [Kind of a type splice]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider these terms, each with TH type splice inside:
     [| e1 :: Maybe $(..blah..) |]
     [| e2 :: $(..blah..) |]
When kind-checking the type signature, we'll kind-check the splice
$(..blah..); we want to give it a kind that can fit in any context,
as if $(..blah..) :: forall k. k.  

In the e1 example, the context of the splice fixes kappa to *.  But
in the e2 example, we'll desugar the type, zonking the kind unification
variables as we go.  When we encournter the unconstrained kappa, we
want to default it to '*', not to AnyK.


891
892
893
894
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

\begin{code}
895
addTypeCtxt :: LHsType Name -> TcM a -> TcM a
896
	-- Wrap a context around only if we want to show that contexts.  
batterseapower's avatar
batterseapower committed
897
	-- Omit invisble ones and ones user's won't grok
898
899
900
901
addTypeCtxt (L _ ty) thing 
  = addErrCtxt doc thing
  where
    doc = ptext (sLit "In the type") <+> quotes (ppr ty)
902
\end{code}
903
904
905
906
907
908
909

%************************************************************************
%*									*
		Type-variable binders
%*									*
%************************************************************************

910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
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
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
Note [Kind-checking strategies]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

There are three main declarations that we have to kind check carefully in the
presence of -XPolyKinds: classes, datatypes, and data/type families. They each
have a different kind-checking strategy (labeled in the parentheses above each
section). This should potentially be cleaned up in the future, but this is how
it stands now (June 2013).

Classes (ParametricKinds):
  - kind-polymorphic by default
  - each un-annotated type variable is given a fresh meta kind variable
  - every explicit kind variable becomes a SigTv during inference
  - no generalisation is done while kind-checking the recursive group

  Taken together, this means that classes cannot participate in polymorphic
  recursion. Thus, the following is not definable:

  class Fugly (a :: k) where
    foo :: forall (b :: k -> *). Fugly b => b a

  But, because explicit kind variables are SigTvs, it is OK for the kind to
  be forced to be the same kind that is used in a separate declaration. See
  test case polykinds/T7020.hs.

Datatypes:
  Here we have two cases, whether or not a Full Kind Signature is provided.
  A Full Kind Signature means that there is a top-level :: in the definition
  of the datatype. For example:

  data T1 :: k -> Bool -> * where ...         -- YES
  data T2 (a :: k) :: Bool -> * where ...     -- YES
  data T3 (a :: k) (b :: Bool) :: * where ... -- YES
  data T4 (a :: k) (b :: Bool) where ...      -- NO

  Kind signatures are not allowed on datatypes declared in the H98 style,
  so those always have no Full Kind Signature.

  Full Kind Signature (FullKindSignature):
    - each un-annotated type variable defaults to *
    - every explicit kind variable becomes a skolem during type inference
    - these kind variables are generalised *before* kind-checking the group

    With these rules, polymorphic recursion is possible. This is essentially
    because of the generalisation step before kind-checking the group -- it
    gives the kind-checker enough flexibility to supply the right kind arguments
    to support polymorphic recursion.

  no Full Kind Signature (ParametricKinds):
    - kind-polymorphic by default
    - each un-annotated type variable is given a fresh meta kind variable
    - every explicit kind variable becomes a SigTv during inference
    - no generalisation is done while kind-checking the recursive group

    Thus, no polymorphic recursion in this case. See also Trac #6093 & #6049.

Type families:
  Here we have three cases: open top-level families, closed top-level families,
  and open associated types. (There are no closed associated types, for good
  reason.)

  Open top-level families (FullKindSignature):
    - All open top-level families are considered to have a Full Kind Signature
    - All arguments and the result default to *
    - All kind variables are skolems
    - All kind variables are generalised before kind-checking the group

    This behaviour supports kind-indexed type and data families, because we
    need to have generalised before kind-checking for this to work. For example:

    type family F (a :: k)
    type instance F Int = Bool
    type instance F Maybe = Char
    type instance F (x :: * -> * -> *) = Double

  Closed top-level families (NonParametricKinds):
    - kind-monomorphic by default
    - each un-annotated type variable is given a fresh meta kind variable
    - every explicit kind variable becomes a skolem during inference
    - all such skolems are generalised before kind-checking; other kind
      variables are not generalised
    - all unconstrained meta kind variables are defaulted to * at the
      end of kind checking

    This behaviour is to allow kind inference to occur in closed families, but
    without becoming too polymorphic. For example:

    type family F a where
      F Int = Bool
      F Bool = Char

    We would want F to have kind * -> * from this definition, although something
    like k1 -> k2 would be perfectly sound. The reason we want this restriction is
    that it is better to have (F Maybe) be a kind error than simply stuck.

    The kind inference gives us also

    type family Not b where
      Not False = True
      Not True  = False

    With an open family, the above would need kind annotations in its header.

    The tricky case is

    type family G a (b :: k) where
      G Int Int    = False
      G Bool Maybe = True

    We want this to work. But, we also want (G Maybe Maybe) to be a kind error
    (in the first argument). So, we need to generalise the skolem "k" but not
    the meta kind variable associated with "a".

  Associated families (FullKindSignature):
    - Kind-monomorphic by default
    - Result kind defaults to *
    - Each type variable is either in the class header or not:
      - Type variables in the class header are given the kind inherited from
        the class header (and checked against an annotation, if any)
      - Un-annotated type variables default to *
    - Each kind variable mentioned in the class header becomes a SigTv during
      kind inference.
    - Each kind variable not mentioned in the class header becomes a skolem during
      kind inference.
    - Only the skolem kind variables are generalised before kind checking.

    Here are some examples:
    
    class Foo1 a b where
      type Bar1 (a :: k) (b :: k)

    The kind of Foo1 will be k -> k -> Constraint. Kind annotations on associated
    type declarations propagate to the header because the type variables in Bar1's
    declaration inherit the (meta) kinds of the class header.

    class Foo2 a where
      type Bar2 a

    The kind of Bar2 will be k -> *.

    class Foo3 a where
      type Bar3 a (b :: k)
      meth :: Bar3 a Maybe -> ()

    The kind of Bar3 will be k1 -> k2 -> *. This only kind-checks because the kind
    of b is generalised before kind-checking.

    class Foo4 a where
      type Bar4 a b

    Here, the kind of Bar4 will be k -> * -> *, because b is not mentioned in the
    class header, so it defaults to *.

1063
\begin{code}
1064
1065
1066
1067
data KindCheckingStrategy   -- See Note [Kind-checking strategies]
  = ParametricKinds
  | NonParametricKinds
  | FullKindSignature
1068
  deriving (Eq)
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080

-- determine the appropriate strategy for a decl
kcStrategy :: TyClDecl Name -> KindCheckingStrategy
kcStrategy d@(ForeignType {}) = pprPanic "kcStrategy" (ppr d)
kcStrategy (FamDecl fam_decl)
  = kcStrategyFamDecl fam_decl
kcStrategy (SynDecl {})       = ParametricKinds
kcStrategy (DataDecl { tcdDataDefn = HsDataDefn { dd_kindSig = m_ksig }})
  | Just _ <- m_ksig            = FullKindSignature
  | otherwise                   = ParametricKinds
kcStrategy (ClassDecl {})     = ParametricKinds

1081
-- if the ClosedTypeFamily has no equations, do the defaulting to *, etc.
1082
kcStrategyFamDecl :: FamilyDecl Name -> KindCheckingStrategy
1083
1084
kcStrategyFamDecl (FamilyDecl { fdInfo = ClosedTypeFamily (_:_) }) = NonParametricKinds
kcStrategyFamDecl _                                                = FullKindSignature
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095

mkKindSigVar :: Name -> TcM KindVar
-- Use the specified name; don't clone it
mkKindSigVar n 
  = do { mb_thing <- tcLookupLcl_maybe n
       ; case mb_thing of
           Just (AThing k)
             | Just kvar <- getTyVar_maybe k
             -> return kvar
           _ -> return $ mkTcTyVar n superKind (SkolemTv False) }

1096
kcScopedKindVars :: [Name] -> TcM a -> TcM a
1097
1098
1099
-- Given some tyvar binders like [a (b :: k -> *) (c :: k)]
-- bind each scoped kind variable (k in this case) to a fresh
-- kind skolem variable
1100
1101
1102
1103
kcScopedKindVars kv_ns thing_inside 
  = do { kvs <- mapM (\n -> newSigTyVar n superKind) kv_ns
                     -- NB: use mutable signature variables
       ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) thing_inside } 
1104

1105
kcHsTyVarBndrs :: KindCheckingStrategy
1106
               -> LHsTyVarBndrs Name 
1107
	       -> TcM (Kind, r)   -- the result kind, possibly with other info
1108
	       -> TcM (Kind, r)
1109
-- Used in getInitialKind
1110
1111
1112
kcHsTyVarBndrs strat (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
  = do { kvs <- if skolem_kvs
                then mapM mkKindSigVar kv_ns
1113
1114
                else mapM (\n -> newSigTyVar n superKind) kv_ns
       ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
1115
    do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs
1116
1117
1118
1119
1120
1121
1122
       ; (res_kind, stuff) <- tcExtendKindEnv nks thing_inside
       ; let full_kind = mkArrowKinds (map snd nks) res_kind
             kvs       = filter (not . isMetaTyVar) $
                         varSetElems $ tyVarsOfType full_kind
             gen_kind  = if generalise
                         then mkForAllTys kvs full_kind
                         else full_kind
1123
       ; return (gen_kind, stuff) } }
1124
  where
1125
1126
1127
1128
1129
1130
    -- See Note [Kind-checking strategies]
    (skolem_kvs, default_to_star, generalise) = case strat of
          ParametricKinds    -> (False, False, False)
          NonParametricKinds -> (True,  False, True)
          FullKindSignature  -> (True,  True,  True)

1131
1132
    kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind)
    kc_hs_tv (UserTyVar n)
1133
      = do { mb_thing <- tcLookupLcl_maybe n
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
           ; kind <- case mb_thing of
               	       Just (AThing k)     -> return k
               	       _ | default_to_star -> return liftedTypeKind
               	         | otherwise       -> newMetaKindVar
           ; return (n, kind) }
    kc_hs_tv (KindedTyVar n k) 
      = do { kind <- tcLHsKind k
               -- In an associated type decl, the type variable may already 
               -- be in scope; in that case we want to make sure its kind
               -- matches the one declared here
           ; mb_thing <- tcLookupLcl_maybe n
           ; case mb_thing of
               Nothing          -> return ()
               Just (AThing ks) -> checkKind kind ks
               Just thing       -> pprPanic "check_in_scope" (ppr thing)
           ; return (n, kind) }
1150

1151
tcHsTyVarBndrs :: LHsTyVarBndrs Name 
1152
	       -> ([TcTyVar] -> TcM r)
1153
	       -> TcM r
1154
1155
1156
-- Bind the kind variables to fresh skolem variables
-- and type variables to skolems, each with a meta-kind variable kind
tcHsTyVarBndrs (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
1157
  = do { kvs <- mapM mkKindSigVar kv_ns
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
       ; tcExtendTyVarEnv kvs $ do 
       { tvs <- mapM tcHsTyVarBndr hs_tvs
       ; traceTc "tcHsTyVarBndrs {" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
                                        , text "Hs type vars:" <+> ppr hs_tvs
                                        , text "Kind vars:" <+> ppr kvs
                                        , text "Type vars:" <+> ppr tvs ])
       ; res <- tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs))
       ; traceTc "tcHsTyVarBndrs }" (vcat [ text "Hs kind vars:" <+> ppr kv_ns
                                        , text "Hs type vars:" <+> ppr hs_tvs
                                        , text "Kind vars:" <+> ppr kvs
                                        , text "Type vars:" <+> ppr tvs ])
       ; return res  } }
1170

1171
tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TcTyVar
1172
-- Return a type variable 
dreixel's avatar
dreixel committed
1173
-- initialised with a kind variable.
1174
1175
-- Typically the Kind inside the HsTyVarBndr will be a tyvar with a mutable kind 
-- in it.
dreixel's avatar
dreixel committed
1176
1177
1178
1179
1180
1181
--
-- If the variable is already in scope return it, instead of introducing a new
-- one. This can occur in 
--   instance C (a,b) where
--     type F (a,b) c = ...
-- Here a,b will be in scope when processing the associated type instance for F.
1182
-- See Note [Associated type tyvar names] in Class
1183
1184
1185
tcHsTyVarBndr (L _ hs_tv)
  = do { let name = hsTyVarName hs_tv
       ; mb_tv <- tcLookupLcl_maybe name
1186
1187
1188
       ; case mb_tv of {
           Just (ATyVar _ tv) -> return tv ;
           _ -> do
1189
1190
1191
1192
       { kind <- case hs_tv of
                   UserTyVar {}       -> newMetaKindVar
                   KindedTyVar _ kind -> tcLHsKind kind
       ; return ( mkTcTyVar name kind (SkolemTv False)) } } }
1193

1194
------------------
1195
1196
kindGeneralize :: TyVarSet -> TcM [KindVar]
kindGeneralize tkvs
1197
  = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
1198
       ; quantifyTyVars gbl_tvs (filterVarSet isKindVar tkvs) }
1199
1200
                -- ToDo: remove the (filter isKindVar)
                -- Any type variables in tkvs will be in scope,
1201
1202
                -- and hence in gbl_tvs, so after removing gbl_tvs
                -- we should only have kind variables left
1203
1204
1205
1206
1207
1208
		--
 		-- BUT there is a smelly case (to be fixed when TH is reorganised)
		--     f t = [| e :: $t |]
                -- When typechecking the body of the bracket, we typecheck $t to a
                -- unification variable 'alpha', with no biding forall.  We don't
                -- want to kind-quantify it!
dreixel's avatar
dreixel committed
1209
1210
\end{code}

1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
Note [Kind generalisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~
We do kind generalisation only at the outer level of a type signature.
For example, consider
  T :: forall k. k -> *
  f :: (forall a. T a -> Int) -> Int
When kind-checking f's type signature we generalise the kind at
the outermost level, thus:
  f1 :: forall k. (forall (a:k). T k a -> Int) -> Int  -- YES!
and *not* at the inner forall:
  f2 :: (forall k. forall (a:k). T k a -> Int) -> Int  -- NO!
Reason: same as for HM inference on value level declarations,
we want to infer the most general type.  The f2 type signature
Gabor Greif's avatar
typos    
Gabor Greif committed
1224
would be *less applicable* than f1, because it requires a more
1225
1226
polymorphic argument.

dreixel's avatar
dreixel committed
1227
1228
Note [Kinds of quantified type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1229
tcTyVarBndrsGen quantifies over a specified list of type variables,
dreixel's avatar
dreixel committed
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
*and* over the kind variables mentioned in the kinds of those tyvars.

Note that we must zonk those kinds (obviously) but less obviously, we
must return type variables whose kinds are zonked too. Example
    (a :: k7)  where  k7 := k9 -> k9
We must return
    [k9, a:k9->k9]
and NOT 
    [k9, a:k7]
Reason: we're going to turn this into a for-all type, 
   forall k9. forall (a:k7). blah
which the type checker will then instantiate, and instantiate does not
look through unification variables!  

1244
Hence using zonked_kinds when forming tvs'.
dreixel's avatar
dreixel committed
1245
1246

\begin{code}
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
--------------------
-- getInitialKind has made a suitably-shaped kind for the type or class
-- Unpack it, and attribute those kinds to the type variables
-- Extend the env with bindings for the tyvars, taken from
-- the kind of the tycon/class.  Give it to the thing inside, and 
-- check the result kind matches
kcLookupKind :: Name -> TcM Kind
kcLookupKind nm 
  = do { tc_ty_thing <- tcLookup nm
       ; case tc_ty_thing of
           AThing k            -> return k
           AGlobal (ATyCon tc) -> return (tyConKind tc)
           _                   -> pprPanic "kcLookupKind" (ppr tc_ty_thing) }

1261
kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> TcM a -> TcM a
1262
-- Used for the type variables of a type or class decl,
1263
-- when doing the initial kind-check.  
1264
kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
1265
  = kcScopedKindVars kvs $
1266
    do 	{ tc_kind <- kcLookupKind name
1267
	; let (arg_ks, _res_k) = splitKindFunTysN (length hs_tvs) tc_kind
1268
1269
1270
                     -- There should be enough arrows, because
                     -- getInitialKinds used the tcdTyVars
        ; name_ks <- zipWithM kc_tv hs_tvs arg_ks
1271
        ; tcExtendKindEnv name_ks thing_inside }
1272
  where
1273
1274
1275
1276
    -- getInitialKind has already gotten the kinds of these type
    -- variables, but tiresomely we need to check them *again* 
    -- to match the kind variables they mention against the ones 
    -- we've freshly brought into scope
1277
    kc_tv :: LHsTyVarBndr Name -> Kind -> TcM (Name, Kind)
1278
1279
1280
1281
1282
1283
    kc_tv (L _ (UserTyVar n)) exp_k 
      = return (n, exp_k)
    kc_tv (L _ (KindedTyVar n hs_k)) exp_k
      = do { k <- tcLHsKind hs_k
           ; checkKind k exp_k
           ; return (n, exp_k) }
1284
1285

-----------------------
1286
tcTyClTyVars :: Name -> LHsTyVarBndrs Name	-- LHS of the type or class decl
dreixel's avatar
dreixel committed
1287
             -> ([TyVar] -> Kind -> TcM a) -> TcM a
1288
1289
-- Used for the type variables of a type or class decl,
-- on the second pass when constructing the final result
1290
1291
1292
-- (tcTyClTyVars T [a,b] thing_inside) 
--   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
--   calls thing_inside with arguments
1293
1294
1295
--      [k1,k2,a,b] (k2 -> *)
--   having also extended the type environment with bindings 
--   for k1,k2,a,b
dreixel's avatar
dreixel committed
1296
1297
1298
--
-- No need to freshen the k's because they are just skolem 
-- constants here, and we are at top level anyway.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1299
1300
1301
1302
tcTyClTyVars tycon (HsQTvs { hsq_kvs = hs_kvs, hsq_tvs = hs_tvs }) thing_inside
  = kcScopedKindVars hs_kvs $ -- Bind scoped kind vars to fresh kind univ vars
                              -- There may be fewer of these than the kvs of
                              -- the type constructor, of course
1303
    do { thing <- tcLookup tycon
1304
1305
1306
       ; let { kind = case thing of
                        AThing kind -> kind
                        _ -> panic "tcTyClTyVars"
dreixel's avatar
dreixel committed
1307
1308
1309
                     -- We only call tcTyClTyVars during typechecking in
                     -- TcTyClDecls, where the local env is extended with
                     -- the generalized_env (mapping Names to AThings).
1310
1311
1312
1313
1314
             ; (kvs, body)  = splitForAllTys kind
             ; (kinds, res) = splitKindFunTysN (length hs_tvs) body }
       ; tvs <- zipWithM tc_hs_tv hs_tvs kinds
       ; tcExtendTyVarEnv tvs (thing_inside (kvs ++ tvs) res) }
  where
1315
1316
1317
1318
    tc_hs_tv (L _ (UserTyVar n))        kind = return (mkTyVar n kind)
    tc_hs_tv (L _ (KindedTyVar n hs_k)) kind = do { tc_kind <- tcLHsKind hs_k
                                                  ; checkKind kind tc_kind
                                                  ; return (mkTyVar n kind) }
1319
1320

-----------------------------------
dreixel's avatar
dreixel committed
1321
tcDataKindSig :: Kind -> TcM [TyVar]
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1322
-- GADT decls can have a (perhaps partial) kind signature
1323
1324
--	e.g.  data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for 
1325
1326
-- the argument kinds, and checks that the result kind is indeed *.
-- We use it also to make up argument type variables for for data instances.
dreixel's avatar
dreixel committed
1327
tcDataKindSig kind
1328
1329
1330
  = do	{ checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
	; span <- getSrcSpanM
	; us   <- newUniqueSupply 
1331
1332
	; let uniqs = uniqsFromSupply us
	; return [ mk_tv span uniq str kind 
1333
		 | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
1334
1335
1336
1337
1338
1339
  where
    (arg_kinds, res_kind) = splitKindFunTys kind
    mk_tv loc uniq str kind = mkTyVar name kind
	where
	   name = mkInternalName uniq occ loc
	   occ  = mkOccName tvName str
1340
1341
	  
    dnames = map ('$' :) names	-- Note [Avoid name clashes for associated data types]
1342

1343
    names :: [String]
1344
1345
1346
1347
    names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 

badKindSig :: Kind -> SDoc
badKindSig kind 
Ian Lynagh's avatar
Ian Lynagh committed
1348
 = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
1349
	2 (ppr kind)
1350
1351
\end{code}

1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
Note [Avoid name clashes for associated data types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider    class C a b where
               data D b :: * -> *
When typechecking the decl for D, we'll invent an extra type variable for D,
to fill out its kind.  We *don't* want this type variable to be 'a', because
in an .hi file we'd get
            class C a b where
               data D b a 
which makes it look as if there are *two* type indices.  But there aren't!
So we use $a instead, which cannot clash with a user-written type variable.
Remember that type variable binders in interface files are just FastStrings,
not proper Names.

(The tidying phase can't help here because we don't tidy TyCons.  Another
alternative would be to record the number of indexing parameters in the 
interface file.)

1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410

%************************************************************************
%*									*
		Scoped type variables
%*									*
%************************************************************************


tcAddScopedTyVars is used for scoped type variables added by pattern
type signatures
	e.g.  \ ((x::a), (y::a)) -> x+y
They never have explicit kinds (because this is source-code only)
They are mutable (because they can get bound to a more specific type).

Usually we kind-infer and expand type splices, and then
tupecheck/desugar the type.  That doesn't work well for scoped type
variables, because they scope left-right in patterns.  (e.g. in the
example above, the 'a' in (y::a) is bound by the 'a' in (x::a).

The current not-very-good plan is to
  * find all the types in the patterns
  * find their free tyvars
  * do kind inference
  * bring the kinded type vars into scope
  * BUT throw away the kind-checked type
  	(we'll kind-check it again when we type-check the pattern)

This is bad because throwing away the kind checked type throws away
its splices.  But too bad for now.  [July 03]

Historical note:
    We no longer specify that these type variables must be univerally 
    quantified (lots of email on the subject).  If you want to put that 
    back in, you need to
	a) Do a checkSigTyVars after thing_inside
	b) More insidiously, don't pass in expected_ty, else
	   we unify with it too early and checkSigTyVars barfs
	   Instead you have to pass in a fresh ty var, and unify
	   it with expected_ty afterwards

\begin{code}
1411
tcHsPatSigType :: UserTypeCtxt
1412
1413
1414
1415
	       -> HsWithBndrs (LHsType Name)  -- The type signature
	      -> TcM ( Type                   -- The signature
                      , [(Name, TcTyVar)] )   -- The new bit of type environment, binding
				              -- the scoped type variables
1416
1417
1418
1419
-- Used for type-checking type signatures in
-- (a) patterns 	  e.g  f (x::Int) = e
-- (b) result signatures  e.g. g x :: Int = e
-- (c) RULE forall bndrs  e.g. forall (x::Int). f x = x
1420

1421
tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs, hswb_tvs = sig_tvs })
1422
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
1423
    do	{ kvs <- mapM new_kv sig_kvs
1424
        ; tvs <- mapM new_tv sig_tvs
1425
1426
        ; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs)
	; sig_ty <- tcExtendTyVarEnv2 ktv_binds $
1427
                    tcHsLiftedType hs_ty
1428
        ; sig_ty <- zonkSigType sig_ty
1429
	; checkValidType ctxt sig_ty 
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
	; return (sig_ty, ktv_binds) }
  where
    new_kv name = new_tkv name superKind
    new_tv name = do { kind <- newMetaKindVar
                     ; new_tkv name kind }

    new_tkv name kind   -- See Note [Pattern signature binders]
      = case ctxt of
          RuleSigCtxt {} -> return (mkTcTyVar name kind (SkolemTv False))
          _              -> newSigTyVar name kind  -- See Note [Unifying SigTvs]
1440
1441

tcPatSig :: UserTypeCtxt
1442
	 -> HsWithBndrs (LHsType Name)
1443
	 -> TcSigmaType
1444
1445
1446
1447
1448
	 -> TcM (TcType,	    -- The type to use for "inside" the signature
		 [(Name, TcTyVar)], -- The new bit of type environment, binding
				    -- the scoped type variables
                 HsWrapper)         -- Coercion due to unification with actual ty
                                    -- Of shape:  res_ty ~ sig_ty
1449
tcPatSig ctxt sig res_ty
1450
  = do	{ (sig_ty, sig_tvs) <- tcHsPatSigType ctxt sig
1451
1452
1453
    	-- sig_tvs are the type variables free in 'sig', 
	-- and not already in scope. These are the ones
	-- that should be brought into scope
1454
1455

	; if null sig_tvs then do {
1456
		-- Just do the subsumption check and return
1457
                  wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
1458
		; return (sig_ty, [], wrap)
1459
        } else do
1460
1461
1462
		-- Type signature binds at least one scoped type variable
	
		-- A pattern binding cannot bind scoped type variables
1463
1464
1465
                -- It is more convenient to make the test here
                -- than in the renamer
	{ let in_pat_bind = case ctxt of
1466
				BindPatSigCtxt -> True
Ian Lynagh's avatar
Ian Lynagh committed
1467
				_              -> False
1468
	; when in_pat_bind (addErr (patBindSigErr sig_tvs))
1469

1470
1471
1472
1473
1474
1475
1476
		-- Check that all newly-in-scope tyvars are in fact
		-- constrained by the pattern.  This catches tiresome
		-- cases like	
		--	type T a = Int
		--	f :: Int -> Int
		-- 	f (x :: T a) = ...
		-- Here 'a' doesn't get a binding.  Sigh
1477
1478
	; let bad_tvs = [ tv | (_, tv) <- sig_tvs
                             , not (tv `elemVarSet` exactTyVarsOfType sig_ty) ]
1479
1480
	; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)

1481
	-- Now do a subsumption check of the pattern signature against res_ty
1482
1483
	; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty

1484
	-- Phew!
1485
        ; return (sig_ty, sig_tvs, wrap)
1486
        } }
1487

1488
patBindSigErr :: [(Name, TcTyVar)] -> SDoc
1489
1490
patBindSigErr sig_tvs 
  = hang (ptext (sLit "You cannot bind scoped type variable") <> plural sig_tvs
1491
          <+> pprQuotedList (map fst sig_tvs))
1492
       2 (ptext (sLit "in a pattern binding signature"))
1493
1494
\end{code}

1495
1496
1497
1498
1499
1500
1501
1502
1503
Note [Pattern signature binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
   data T = forall a. T a (a->Int)
   f (T x (f :: a->Int) = blah)

Here 
 * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk', 
   It must be a skolem so that that it retains its identity, and    
Simon Peyton Jones's avatar
Simon Peyton Jones committed
1504
   TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
1505
1506
1507
1508
1509

 * The type signature pattern (f :: a->Int) binds "a" -> a_sig in the envt

 * Then unificaiton makes a_sig := a_sk

1510
1511
That's why we must make a_sig a MetaTv (albeit a SigTv), 
not a SkolemTv, so that it can unify to a_sk.
1512
1513
1514