TcHsType.lhs 62.9 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 21
                -- Type checking type and class decls
	kcTyClTyVars, tcTyClTyVars,
22
        tcHsConArgType, tcDataKindSig, 
23
        tcClassSigType, 
dreixel's avatar
dreixel committed
24

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

32
        kindGeneralize, checkKind,
33 34 35

		-- Sort-checking kinds
	tcLHsKind, 
36

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

#include "HsVersions.h"

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

47
import HsSyn
48
import TcHsSyn ( zonkTcTypeToType, emptyZonkEnv )
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
dreixel's avatar
dreixel committed
58
import Kind
59
import TypeRep( mkNakedTyConApp )
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 188 189 190
          -- Zonk to expose kind information to checkValidType
        ; ty <- zonkTcType ty
        ; 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 199
       ; kvs     <- zonkTcTypeAndFV inst_ty
       ; kvs     <- kindGeneralize kvs []
200 201 202 203 204 205 206 207 208 209 210 211
       ; inst_ty <- zonkTcType (mkForAllTys kvs inst_ty)
       ; 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 222 223 224 225
-----------------
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
       ; ty   <- zonkTcType ty
       ; 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 258 259 260 261 262 263 264 265
tcClassSigType :: LHsType Name -> TcM Type
tcClassSigType lhs_ty@(L _ hs_ty)
  = addTypeCtxt lhs_ty $
    do { ty <- tcCheckHsTypeAndGen hs_ty liftedTypeKind
       ; zonkTcTypeToType emptyZonkEnv ty }

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 310 311
       ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty)
       ; traceTc "tcCheckHsTypeAndGen" (ppr ty)
       ; kvs <- zonkTcTypeAndFV ty 
       ; kvs <- kindGeneralize kvs []
312
       ; return (mkForAllTys kvs ty) }
313 314
\end{code}

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

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

tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType
tc_lhs_type (L span ty) exp_kind
329
  = setSrcSpan span $
330 331 332 333 334 335
    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

336 337 338 339 340 341 342 343 344 345 346 347
------------------------------------------
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') }

348 349 350 351 352
------------------------------------------
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
353 354 355 356 357
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)
358 359 360 361 362 363 364 365 366 367
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 }

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

tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind
372 373 374
  | op `hasKey` funTyConKey
  = tc_fun_type hs_ty ty1 ty2 exp_kind
  | otherwise
375 376 377 378 379 380
  = 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
381 382 383 384 385 386
  | L _ (HsTyVar fun) <- fun_ty
  , fun `hasKey` funTyConKey
  , [fty1,fty2] <- arg_tys
  = tc_fun_type hs_ty fty1 fty2 exp_kind
  | otherwise
  = do { (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty
387 388 389
       ; 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
390 391 392
         -- 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)?
393 394
  where
    (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
395 396

--------- Foralls
397
tc_hs_type hs_ty@(HsForAllTy _ hs_tvs context ty) exp_kind
398 399 400
  = tcHsTyVarBndrs hs_tvs $ \ tvs' -> 
    -- Do not kind-generalise here!  See Note [Kind generalisation]
    do { ctxt' <- tcHsContext context
401 402 403 404
       ; 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
405
                   -- _function_, so the kind of the result really is *
406 407 408
                   -- The body kind (result of the function can be * or #, hence ekOpen
                   do { checkExpectedKind hs_ty liftedTypeKind exp_kind
                      ; tc_lhs_type ty ekOpen }
409 410 411 412 413 414 415 416 417 418 419 420 421 422
       ; 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) }
423

dreixel's avatar
dreixel committed
424
-- See Note [Distinguishing tuple kinds] in HsTypes
425 426 427 428 429
-- 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
430 431
  | otherwise
  = do { k <- newMetaKindVar
432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
       ; (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
452
         -- check the arguments again to give good error messages
dreixel's avatar
dreixel committed
453 454
         -- in eg. `(Maybe, Maybe)`

455 456
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
457

458 459 460 461 462 463 464 465
--------- 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
466 467
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
468 469 470 471 472 473 474 475 476 477 478 479 480

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
481
  = do { ty' <- tc_lhs_type ty ekLifted
482
       ; checkExpectedKind ipTy constraintKind exp_kind
483 484 485 486
       ; ipClass <- tcLookupClass ipClassName
       ; let n' = mkStrLitTy $ hsIPNameFS n
       ; return (mkClassPred ipClass [n',ty'])
       }
487 488 489 490 491

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
492
              (EK kind1 msg_fn)
493 494
       ; checkExpectedKind ty constraintKind exp_kind
       ; return (mkNakedTyConApp eqTyCon [kind1, ty1', ty2']) }
495 496 497
  where
    msg_fn pkind = ptext (sLit "The left argument of the equality had kind")
                   <+> quotes (pprKind pkind)
498 499 500 501 502

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

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


513
#ifdef GHCI	/* Only if bootstrapped */
514 515 516
-- 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
517
tc_hs_type hs_ty@(HsSpliceTy sp fvs _) exp_kind 
518 519 520
  = do { s <- getStage
       ; traceTc "tc_hs_type: splice" (ppr sp $$ ppr s) 
       ; (ty, kind) <- tcSpliceType sp fvs
521 522 523 524 525 526 527 528 529 530
       ; 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
531

532 533 534 535 536 537
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 
538 539
  = do { checkExpectedKind hs_ty typeSymbolKind exp_kind
       ; checkWiredInTyCon typeSymbolKindCon
540
       ; return (mkStrLitTy s) }
541

542 543 544 545 546 547
---------------------------
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
548 549 550
  where
    arg_kind = case tup_sort of
                 HsBoxedTuple      -> liftedTypeKind
551
                 HsUnboxedTuple    -> openTypeKind
dreixel's avatar
dreixel committed
552
                 HsConstraintTuple -> constraintKind
553
                 _                 -> panic "tc_hs_type arg_kind"
dreixel's avatar
dreixel committed
554 555 556 557
    cxt_doc = case tup_sort of
                 HsBoxedTuple      -> ptext (sLit "a tuple")
                 HsUnboxedTuple    -> ptext (sLit "an unboxed tuple")
                 HsConstraintTuple -> ptext (sLit "a constraint tuple")
558
                 _                 -> panic "tc_hs_type tup_sort"
dreixel's avatar
dreixel committed
559

560 561 562 563 564 565 566 567 568 569 570 571 572 573
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
574
                 HsUnboxedTuple    -> unliftedTypeKind
575 576 577
                 HsBoxedTuple      -> liftedTypeKind
                 HsConstraintTuple -> constraintKind
                 _                 -> panic "tc_hs_type arg_kind"
578

579
---------------------------
580
tcInferApps :: Outputable a
581 582
       => a 
       -> TcKind			-- Function kind
583
       -> [LHsType Name]		-- Arg types
584 585 586 587
       -> 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
588 589
       ; return (args', res_kind) }

590 591 592 593 594 595 596 597 598 599
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 }
600

601
---------------------------
602 603 604
splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
splitFunKind the_fun fun_kind args
  = go 1 fun_kind args
605
  where
606 607 608 609 610 611 612 613 614
    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) } }
 
615
    too_many_args = quotes the_fun <+>
Ian Lynagh's avatar
Ian Lynagh committed
616
		    ptext (sLit "is applied to too many type arguments")
617

618

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

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

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

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

657
           APromotionErr err -> promotionErr name err
658 659

           _  -> wrongThingErr "type" thing name }
dreixel's avatar
dreixel committed
660
  where
661 662 663 664 665 666 667 668 669 670 671 672
    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
673 674
      | otherwise
      = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind)
675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695
           ; 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)
696 697
\end{code}

698 699 700 701 702
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.
703

704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 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 776 777
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
look at the TyCon or Class involved.  Hence the use of mkNakedXXX
functions.

This is sadly delicate.

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`.
778

dreixel's avatar
dreixel committed
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
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
808 809
	(a) spurious ! annotations.
	(b) a class used as a type
810

dreixel's avatar
dreixel committed
811 812 813 814 815 816 817 818 819 820 821 822 823 824 825
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.


826 827 828 829
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

\begin{code}
830
addTypeCtxt :: LHsType Name -> TcM a -> TcM a
831
	-- Wrap a context around only if we want to show that contexts.  
batterseapower's avatar
batterseapower committed
832
	-- Omit invisble ones and ones user's won't grok
833 834 835 836
addTypeCtxt (L _ ty) thing 
  = addErrCtxt doc thing
  where
    doc = ptext (sLit "In the type") <+> quotes (ppr ty)
837
\end{code}
838 839 840 841 842 843 844

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

dreixel's avatar
dreixel committed
845 846 847 848 849 850 851 852 853 854 855 856 857 858
Note [Kind-checking kind-polymorphic types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider:
  f :: forall (f::k -> *) a. f a -> Int

Here, the [LHsTyVarBndr Name] of the forall type will be [f,a], where
  a is a  UserTyVar   -> type variable without kind annotation
  f is a  KindedTyVar -> type variable with kind annotation

If were were to allow binding sites for kind variables, thus
  f :: forall @k (f :: k -> *) a. f a -> Int
then we'd also need
  k is a   UserKiVar   -> kind variable (they don't need annotation,
                          since we only have BOX for a super kind)
859 860

\begin{code}
861
kcScopedKindVars :: [Name] -> TcM a -> TcM a
862 863 864
-- 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
865 866 867 868
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 } 
869

870 871
kcHsTyVarBndrs :: Bool    -- True <=> full kind signature provided
                          -- Default UserTyVar to *
872
                          -- and use KindVars not meta kind vars
873 874 875
               -> LHsTyVarBndrs Name 
	       -> ([TcKind] -> TcM r)
	       -> TcM r
876
-- Used in getInitialKind
877 878 879 880 881
kcHsTyVarBndrs full_kind_sig (HsQTvs { hsq_kvs = kv_ns, hsq_tvs = hs_tvs }) thing_inside
  = do { kvs <- if full_kind_sig 
                then return (map mkKindSigVar kv_ns)
                else mapM (\n -> newSigTyVar n superKind) kv_ns
       ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
882
    do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs
883
       ; tcExtendKindEnv nks (thing_inside (map snd nks)) } }
884 885 886 887 888
  where
    kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind)
    kc_hs_tv (UserTyVar n)     
      = do { mb_thing <- tcLookupLcl_maybe n
           ; kind <- case mb_thing of
889 890 891
               	       Just (AThing k)   -> return k
               	       _ | full_kind_sig -> return liftedTypeKind
               	         | otherwise     -> newMetaKindVar
892 893 894
           ; return (n, kind) }
    kc_hs_tv (KindedTyVar n k) 
      = do { kind <- tcLHsKind k
895 896 897 898 899 900 901 902
               -- 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)
903
           ; return (n, kind) }
904

905
tcHsTyVarBndrs :: LHsTyVarBndrs Name 
906
	       -> ([TcTyVar] -> TcM r)
907
	       -> TcM r
908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923
-- 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
  = do { let kvs = map mkKindSigVar kv_ns
       ; 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  } }
924

925
tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TcTyVar
926
-- Return a type variable 
dreixel's avatar
dreixel committed
927 928 929 930 931 932 933 934 935 936
-- initialised with a kind variable.
-- Typically the Kind inside the KindedTyVar will be a tyvar with a mutable kind 
-- in it. We aren't yet sure whether the binder is a *type* variable or a *kind*
-- variable. See Note [Kind-checking kind-polymorphic types]
--
-- 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.
937
-- See Note [Associated type tyvar names] in Class
938 939 940 941 942 943 944
tcHsTyVarBndr (L _ hs_tv)
  = do { let name = hsTyVarName hs_tv
       ; mb_tv <- tcLookupLcl_maybe name
       ; case mb_tv of {
           Just (ATyVar _ tv) -> return tv ;
           _ -> do
       { kind <- case hs_tv of
945
                   UserTyVar {}       -> newMetaKindVar
946
                   KindedTyVar _ kind -> tcLHsKind kind
947
       ; return (mkTcTyVar name kind (SkolemTv False)) } } }
948 949

------------------
950 951 952 953
kindGeneralize :: TyVarSet -> [Name] -> TcM [KindVar]
kindGeneralize tkvs _names_to_avoid
  = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
       ; tkvs    <- zonkTyVarsAndFV tkvs
954
       ; let kvs_to_quantify = filter isKindVar (varSetElems (tkvs `minusVarSet` gbl_tvs))
955 956
                -- ToDo: remove the (filter isKindVar)
                -- Any type variables in tkvs will be in scope,
957 958
                -- and hence in gbl_tvs, so after removing gbl_tvs
                -- we should only have kind variables left
959 960 961 962 963 964
		--
 		-- 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!
965

966
       ; traceTc "kindGeneralise" (vcat [ppr kvs_to_quantify])
967
       ; ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify $$ ppr tkvs)
968
             -- This assertion is obviosly true because of the filter isKindVar
969 970
             -- but we'll remove that when reorganising TH, and then the assertion
             -- will mean something
971 972 973 974 975

             -- If we tidied the kind variables, which should all be mutable,
             -- this 'zonkQuantifiedTyVars' update the original TyVar to point to
             -- the tided and skolemised one
         zonkQuantifiedTyVars kvs_to_quantify }
dreixel's avatar
dreixel committed
976 977
\end{code}

978 979 980 981 982 983 984 985 986 987 988 989 990
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
991
would be *less applicable* than f1, because it requires a more
992 993
polymorphic argument.

dreixel's avatar
dreixel committed
994 995
Note [Kinds of quantified type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
996
tcTyVarBndrsGen quantifies over a specified list of type variables,
dreixel's avatar
dreixel committed
997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010
*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!  

1011
Hence using zonked_kinds when forming tvs'.
dreixel's avatar
dreixel committed
1012 1013

\begin{code}
1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027
--------------------
-- 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) }

1028
kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> TcM a -> TcM a
1029
-- Used for the type variables of a type or class decl,
1030
-- when doing the initial kind-check.  
1031
kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
1032
  = kcScopedKindVars kvs $
1033
    do 	{ tc_kind <- kcLookupKind name
1034
	; let (arg_ks, _res_k) = splitKindFunTysN (length hs_tvs) tc_kind
1035 1036 1037
                     -- There should be enough arrows, because
                     -- getInitialKinds used the tcdTyVars
        ; name_ks <- zipWithM kc_tv hs_tvs arg_ks
1038
        ; tcExtendKindEnv name_ks thing_inside }
1039
  where
1040 1041 1042 1043
    -- 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
1044
    kc_tv :: LHsTyVarBndr Name -> Kind -> TcM (Name, Kind)
1045
    kc_tv (L _ (UserTyVar n)) exp_k 
1046
      = return (n, exp_k)
1047
    kc_tv (L _ (KindedTyVar n hs_k)) exp_k
1048
      = do { k <- tcLHsKind hs_k
1049
           ; checkKind k exp_k
1050
           ; return (n, exp_k) }
1051 1052

-----------------------
1053
tcTyClTyVars :: Name -> LHsTyVarBndrs Name	-- LHS of the type or class decl
dreixel's avatar
dreixel committed
1054
             -> ([TyVar] -> Kind -> TcM a) -> TcM a
1055 1056
-- Used for the type variables of a type or class decl,
-- on the second pass when constructing the final result
1057 1058 1059
-- (tcTyClTyVars T [a,b] thing_inside) 
--   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
--   calls thing_inside with arguments
1060 1061 1062
--      [k1,k2,a,b] (k2 -> *)
--   having also extended the type environment with bindings 
--   for k1,k2,a,b
dreixel's avatar
dreixel committed
1063 1064 1065
--
-- 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
1066 1067 1068 1069
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
1070
    do { thing <- tcLookup tycon
1071 1072 1073
       ; let { kind = case thing of
                        AThing kind -> kind
                        _ -> panic "tcTyClTyVars"
dreixel's avatar
dreixel committed
1074 1075 1076
                     -- We only call tcTyClTyVars during typechecking in
                     -- TcTyClDecls, where the local env is extended with
                     -- the generalized_env (mapping Names to AThings).
1077 1078 1079 1080 1081 1082 1083
             ; (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
    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
1084
                                                  ; checkKind kind tc_kind
1085
                                                  ; return (mkTyVar n kind) }
1086 1087

-----------------------------------
dreixel's avatar
dreixel committed
1088
tcDataKindSig :: Kind -> TcM [TyVar]
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1089
-- GADT decls can have a (perhaps partial) kind signature
1090 1091
--	e.g.  data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for 
1092 1093
-- 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
1094
tcDataKindSig kind
1095 1096 1097
  = do	{ checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
	; span <- getSrcSpanM
	; us   <- newUniqueSupply 
1098 1099
	; let uniqs = uniqsFromSupply us
	; return [ mk_tv span uniq str kind 
1100
		 | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
1101 1102 1103 1104 1105 1106
  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
1107 1108
	  
    dnames = map ('$' :) names	-- Note [Avoid name clashes for associated data types]
1109

1110
    names :: [String]
1111 1112 1113 1114
    names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 

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

1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136
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.)

1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177

%************************************************************************
%*									*
		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}
1178
tcHsPatSigType :: UserTypeCtxt
1179 1180 1181 1182
	       -> HsWithBndrs (LHsType Name)  -- The type signature
	      -> TcM ( Type                   -- The signature
                      , [(Name, TcTyVar)] )   -- The new bit of type environment, binding
				              -- the scoped type variables
1183 1184 1185 1186
-- 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
1187

1188
tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs, hswb_tvs = sig_tvs })
1189
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
1190
    do	{ kvs <- mapM new_kv sig_kvs
1191
        ; tvs <- mapM new_tv sig_tvs
1192 1193
        ; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs)
	; sig_ty <- tcExtendTyVarEnv2 ktv_binds $
Simon Peyton Jones's avatar