TcHsType.lhs 61.2 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 53 54 55
import TcEnv
import TcMType
import TcUnify
import TcIface
import TcType
56
import Type
dreixel's avatar
dreixel committed
57
import Kind
58
import TypeRep( mkNakedTyConApp )
59
import Var
60
import VarSet
61
import TyCon
62
import DataCon
dreixel's avatar
dreixel committed
63
import TysPrim ( liftedTypeKindTyConName, constraintKindTyConName )
64 65
import Class
import Name
66
import NameEnv
67 68 69
import TysWiredIn
import BasicTypes
import SrcLoc
70
import ErrUtils ( isEmptyMessages )
71
import DynFlags ( ExtensionFlag( Opt_DataKinds ), getDynFlags )
72
import Unique
73
import UniqSupply
74
import Outputable
75
import FastString
76 77
import Util

78
import Control.Monad ( unless, when, zipWithM )
79
import PrelNames( ipClassName, funTyConKey )
80 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
\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.


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

\begin{code}
166
tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
167 168 169
  -- 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
170
tcHsSigType ctxt hs_ty
171
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
172 173
    tcHsSigTypeNC ctxt hs_ty

174 175 176 177 178 179
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
180 181
          -- The kind is checked by checkValidType, and isn't necessarily
          -- of kind * in a Template Haskell quote eg [t| Maybe |]
182

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

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

191
-----------------
dreixel's avatar
dreixel committed
192
tcHsInstHead :: UserTypeCtxt -> LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
193
-- Like tcHsSigTypeNC, but for an instance head.
dreixel's avatar
dreixel committed
194
tcHsInstHead ctxt lhs_ty@(L loc hs_ty)
195 196 197 198
  = setSrcSpan loc $    -- The "In the type..." context comes from the caller
    do { ty <- tcCheckHsTypeAndGen hs_ty constraintKind
       ; ty <- zonkTcType ty
       ; checkValidInstance ctxt lhs_ty ty }
batterseapower's avatar
batterseapower committed
199

200 201 202 203 204 205 206 207 208 209 210 211 212
-----------------
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)
213
           Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) }
214 215 216 217 218 219

-- Used for 'VECTORISE [SCALAR] instance' declarations
--
tcHsVectInst :: LHsType Name -> TcM (Class, [Type])
tcHsVectInst ty
  | Just (L _ cls_name, tys) <- splitLHsClassTy_maybe ty
220 221 222
  = do { (cls, cls_kind) <- tcClass cls_name
       ; (arg_tys, _res_kind) <- tcInferApps cls_name cls_kind tys
       ; return (cls, arg_tys) }
223 224
  | otherwise
  = failWithTc $ ptext (sLit "Malformed instance type")
225 226 227 228 229 230 231 232 233
\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


%************************************************************************
%*									*
234
            The main kind checker: no validity checks here
235 236 237 238 239 240
%*									*
%************************************************************************
	
	First a couple of simple wrappers for kcHsType

\begin{code}
241 242 243 244 245 246 247 248 249 250 251 252
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

253
tcHsConArgType DataType bty = tcHsOpenType (getBangType bty)
254 255 256 257
  -- 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

258
---------------------------
259 260 261 262 263 264 265 266 267 268 269
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..] ]
270

dreixel's avatar
dreixel committed
271
---------------------------
272
tcHsOpenType, tcHsLiftedType :: LHsType Name -> TcM TcType
273 274
-- Used for type signatures
-- Do not do validity checking
275
tcHsOpenType ty   = addTypeCtxt ty $ tc_lhs_type ty ekOpen
276 277 278 279 280 281
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 $ 
282
    tc_lhs_type hs_ty (EK exp_kind expectedKindMsg)
283 284 285 286

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
287

288
---------------------------
289 290 291 292 293
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
294
  = do { ty  <- tc_hs_type hs_ty (EK kind expectedKindMsg)
295
       ; kvs <- kindGeneralize (tyVarsOfType ty) []
296
       ; return (mkForAllTys kvs ty) }
297 298
\end{code}

299
Like tcExpr, tc_hs_type takes an expected kind which it unifies with
dreixel's avatar
dreixel committed
300
the kind it figures out. When we don't know what kind to expect, we use
301
tc_lhs_type_fresh, to first create a new meta kind variable and use that as
dreixel's avatar
dreixel committed
302
the expected kind.
303 304

\begin{code}
305 306 307
tc_infer_lhs_type :: LHsType Name -> TcM (TcType, TcKind)
tc_infer_lhs_type ty =
  do { kv <- newMetaKindVar
308
     ; r <- tc_lhs_type ty (EK kv expectedKindMsg)
309 310 311 312
     ; return (r, kv) }

tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType
tc_lhs_type (L span ty) exp_kind
313
  = setSrcSpan span $
314 315 316 317 318 319
    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

320 321 322 323 324 325 326 327 328 329 330 331
------------------------------------------
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') }

332 333 334 335 336
------------------------------------------
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
337 338 339 340 341
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)
342 343 344 345 346 347 348 349 350 351
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 }

352 353
tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind
  = tc_fun_type ty ty1 ty2 exp_kind
354 355

tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind
356 357 358
  | op `hasKey` funTyConKey
  = tc_fun_type hs_ty ty1 ty2 exp_kind
  | otherwise
359 360 361 362 363 364
  = 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
365 366 367 368 369 370
  | 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
371 372 373
       ; 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]
374 375
  where
    (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397

--------- Foralls
tc_hs_type (HsForAllTy _ hs_tvs context ty) exp_kind
  = tcHsTyVarBndrs hs_tvs $ \ tvs' -> 
    -- Do not kind-generalise here!  See Note [Kind generalisation]
    do { ctxt' <- tcHsContext context
       ; ty'   <- tc_lhs_type ty exp_kind
           -- Why exp_kind?  See Note [Body kind of forall]
       ; 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) }
398

dreixel's avatar
dreixel committed
399
-- See Note [Distinguishing tuple kinds] in HsTypes
400 401 402 403 404
-- 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
405 406
  | otherwise
  = do { k <- newMetaKindVar
407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426
       ; (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
427
         -- check the arguments again to give good error messages
dreixel's avatar
dreixel committed
428 429
         -- in eg. `(Maybe, Maybe)`

430 431
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
432

433 434 435 436 437 438 439 440
--------- 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
441 442
    mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
    mk_nil  k     = mkTyConApp (promoteDataCon nilDataCon) [k]
443 444 445 446 447 448 449 450 451 452 453 454 455

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
456
  = do { ty' <- tc_lhs_type ty ekLifted
457
       ; checkExpectedKind ipTy constraintKind exp_kind
458 459 460 461
       ; ipClass <- tcLookupClass ipClassName
       ; let n' = mkStrLitTy $ hsIPNameFS n
       ; return (mkClassPred ipClass [n',ty'])
       }
462 463 464 465 466

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
467
              (EK kind1 msg_fn)
468 469
       ; checkExpectedKind ty constraintKind exp_kind
       ; return (mkNakedTyConApp eqTyCon [kind1, ty1', ty2']) }
470 471 472
  where
    msg_fn pkind = ptext (sLit "The left argument of the equality had kind")
                   <+> quotes (pprKind pkind)
473 474 475 476 477

--------- Misc
tc_hs_type (HsKindSig ty sig_k) exp_kind 
  = do { sig_k' <- tcLHsKind sig_k
       ; checkExpectedKind ty sig_k' exp_kind
478 479 480 481
       ; tc_lhs_type ty (EK sig_k' msg_fn) }
  where
    msg_fn pkind = ptext (sLit "The signature specified kind") 
                   <+> quotes (pprKind pkind)
482 483 484 485

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


488
#ifdef GHCI	/* Only if bootstrapped */
489 490 491
-- 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
492
tc_hs_type hs_ty@(HsSpliceTy sp fvs _) exp_kind 
493 494 495
  = do { s <- getStage
       ; traceTc "tc_hs_type: splice" (ppr sp $$ ppr s) 
       ; (ty, kind) <- tcSpliceType sp fvs
496 497 498 499 500 501 502 503 504 505
       ; 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
506

507 508 509 510 511 512 513 514 515
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 
  = do { checkExpectedKind hs_ty typeStringKind exp_kind
       ; checkWiredInTyCon typeStringKindCon
       ; return (mkStrLitTy s) }
516

517 518 519 520 521 522
---------------------------
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
523 524 525
  where
    arg_kind = case tup_sort of
                 HsBoxedTuple      -> liftedTypeKind
526
                 HsUnboxedTuple    -> openTypeKind
dreixel's avatar
dreixel committed
527
                 HsConstraintTuple -> constraintKind
528
                 _                 -> panic "tc_hs_type arg_kind"
dreixel's avatar
dreixel committed
529 530 531 532
    cxt_doc = case tup_sort of
                 HsBoxedTuple      -> ptext (sLit "a tuple")
                 HsUnboxedTuple    -> ptext (sLit "an unboxed tuple")
                 HsConstraintTuple -> ptext (sLit "a constraint tuple")
533
                 _                 -> panic "tc_hs_type tup_sort"
dreixel's avatar
dreixel committed
534

535 536 537 538 539 540 541 542 543 544 545 546 547 548
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
549
                 HsUnboxedTuple    -> unliftedTypeKind
550 551 552
                 HsBoxedTuple      -> liftedTypeKind
                 HsConstraintTuple -> constraintKind
                 _                 -> panic "tc_hs_type arg_kind"
553

554
---------------------------
555
tcInferApps :: Outputable a
556 557
       => a 
       -> TcKind			-- Function kind
558
       -> [LHsType Name]		-- Arg types
559 560 561 562
       -> 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
563 564
       ; return (args', res_kind) }

565 566 567 568 569 570 571 572 573 574
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 }
575

576
---------------------------
577 578 579
splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
splitFunKind the_fun fun_kind args
  = go 1 fun_kind args
580
  where
581 582 583 584 585 586 587 588 589
    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) } }
 
590
    too_many_args = quotes the_fun <+>
Ian Lynagh's avatar
Ian Lynagh committed
591
		    ptext (sLit "is applied to too many type arguments")
592

593

594
---------------------------
595 596
tcHsContext :: LHsContext Name -> TcM [PredType]
tcHsContext ctxt = mapM tcHsLPredType (unLoc ctxt)
597

598 599
tcHsLPredType :: LHsType Name -> TcM PredType
tcHsLPredType pred = tc_lhs_type pred ekConstraint
600 601

---------------------------
602
tcTyVar :: Name -> TcM (TcType, TcKind)
dreixel's avatar
dreixel committed
603 604
-- See Note [Type checking recursive type and class declarations]
-- in TcTyClsDecls
605
tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
dreixel's avatar
dreixel committed
606 607 608 609
  = do { traceTc "lk1" (ppr name)
       ; thing <- tcLookup name
       ; traceTc "lk2" (ppr name <+> ppr thing)
       ; case thing of
610 611 612 613 614 615
           ATyVar _ tv 
              | isKindVar tv
              -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr tv)
                             <+> ptext (sLit "used as a type"))
              | otherwise
              -> return (mkTyVarTy tv, tyVarKind tv)
616 617 618 619 620 621 622 623

           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)
624
             | Just tc <- promoteDataCon_maybe dc
625 626 627
             -> do { data_kinds <- xoptM Opt_DataKinds
                   ; unless data_kinds $ promotionErr name NoDataKinds
                   ; inst_tycon (mkTyConApp tc) (tyConKind tc) }
628
             | otherwise -> failWithTc (quotes (ppr dc) <+> ptext (sLit "of type")
629
                            <+> quotes (ppr (dataConUserType dc)) <+> ptext (sLit "is not promotable"))
630

631
           APromotionErr err -> promotionErr name err
632 633

           _  -> wrongThingErr "type" thing name }
dreixel's avatar
dreixel committed
634
  where
635 636 637 638 639 640 641 642 643 644 645 646
    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
647 648
      | otherwise
      = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind)
649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669
           ; 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)
670 671
\end{code}

672 673 674 675 676
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.
677

678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 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
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`.
752

dreixel's avatar
dreixel committed
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 778 779 780 781
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
782 783
	(a) spurious ! annotations.
	(b) a class used as a type
784

dreixel's avatar
dreixel committed
785 786 787 788 789 790 791 792 793 794 795 796 797 798 799
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.


800 801 802 803
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

\begin{code}
804
addTypeCtxt :: LHsType Name -> TcM a -> TcM a
805
	-- Wrap a context around only if we want to show that contexts.  
batterseapower's avatar
batterseapower committed
806
	-- Omit invisble ones and ones user's won't grok
807 808 809 810
addTypeCtxt (L _ ty) thing 
  = addErrCtxt doc thing
  where
    doc = ptext (sLit "In the type") <+> quotes (ppr ty)
811
\end{code}
812 813 814 815 816 817 818

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

dreixel's avatar
dreixel committed
819 820 821 822 823 824 825 826 827 828 829 830 831 832
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)
833 834

\begin{code}
835
kcScopedKindVars :: [Name] -> TcM a -> TcM a
836 837 838
-- 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
839 840 841 842
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 } 
843

844 845
kcHsTyVarBndrs :: Bool    -- True <=> full kind signature provided
                          -- Default UserTyVar to *
846
                          -- and use KindVars not meta kind vars
847 848 849
               -> LHsTyVarBndrs Name 
	       -> ([TcKind] -> TcM r)
	       -> TcM r
850
-- Used in getInitialKind
851 852 853 854 855
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) $
856
    do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs
857
       ; tcExtendKindEnv nks (thing_inside (map snd nks)) } }
858 859 860 861 862
  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
863 864 865
               	       Just (AThing k)   -> return k
               	       _ | full_kind_sig -> return liftedTypeKind
               	         | otherwise     -> newMetaKindVar
866 867 868
           ; return (n, kind) }
    kc_hs_tv (KindedTyVar n k) 
      = do { kind <- tcLHsKind k
869 870 871 872 873 874 875 876
               -- 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)
877
           ; return (n, kind) }
878

879 880 881 882 883 884 885
tcScopedKindVars :: [Name] -> TcM a -> TcM a
-- 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
tcScopedKindVars kv_ns thing_inside 
  = tcExtendTyVarEnv (map mkKindSigVar kv_ns) thing_inside

886
tcHsTyVarBndrs :: LHsTyVarBndrs Name 
887 888 889
	       -> ([TyVar] -> TcM r)
	       -> TcM r
-- Bind the type variables to skolems, each with a meta-kind variable kind
890
tcHsTyVarBndrs (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
891
  = tcScopedKindVars kvs $
892 893 894 895 896 897
    do { tvs <- mapM tcHsTyVarBndr hs_tvs
       ; traceTc "tcHsTyVarBndrs" (ppr hs_tvs $$ ppr tvs)
       ; tcExtendTyVarEnv tvs (thing_inside tvs) }

tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TyVar
-- Return a type variable 
dreixel's avatar
dreixel committed
898 899 900 901 902 903 904 905 906 907
-- 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.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
908
-- See Note [Associated type tyvar names] in TyCon
909 910 911 912 913 914 915 916
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
                   UserTyVar {} -> newMetaKindVar
917
                   KindedTyVar _ kind -> tcLHsKind kind
918
       ; return (mkTcTyVar name kind (SkolemTv False)) } } }
919 920

------------------
921 922 923 924
kindGeneralize :: TyVarSet -> [Name] -> TcM [KindVar]
kindGeneralize tkvs _names_to_avoid
  = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
       ; tkvs    <- zonkTyVarsAndFV tkvs
925
       ; let kvs_to_quantify = filter isKindVar (varSetElems (tkvs `minusVarSet` gbl_tvs))
926 927
                -- ToDo: remove the (filter isKindVar)
                -- Any type variables in tkvs will be in scope,
928 929
                -- and hence in gbl_tvs, so after removing gbl_tvs
                -- we should only have kind variables left
930 931 932 933 934 935
		--
 		-- 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!
936

937
       ; traceTc "kindGeneralise" (vcat [ppr kvs_to_quantify])
938
       ; ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify $$ ppr tkvs)
939
             -- This assertion is obviosly true because of the filter isKindVar
940 941
             -- but we'll remove that when reorganising TH, and then the assertion
             -- will mean something
942 943 944 945 946

             -- 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
947 948
\end{code}

949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964
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
would be *less applicable* than f1, becuase it requires a more
polymorphic argument.

dreixel's avatar
dreixel committed
965 966
Note [Kinds of quantified type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
967
tcTyVarBndrsGen quantifies over a specified list of type variables,
dreixel's avatar
dreixel committed
968 969 970 971 972 973 974 975 976 977 978 979 980 981
*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!  

982
Hence using zonked_kinds when forming tvs'.
dreixel's avatar
dreixel committed
983 984

\begin{code}
985 986 987 988 989 990 991 992 993 994 995 996 997 998
--------------------
-- 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) }

999
kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> TcM a -> TcM a
1000
-- Used for the type variables of a type or class decl,
1001
-- when doing the initial kind-check.  
1002
kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside
1003
  = kcScopedKindVars kvs $
1004
    do 	{ tc_kind <- kcLookupKind name
1005
	; let (arg_ks, _res_k) = splitKindFunTysN (length hs_tvs) tc_kind
1006 1007 1008
                     -- There should be enough arrows, because
                     -- getInitialKinds used the tcdTyVars
        ; name_ks <- zipWithM kc_tv hs_tvs arg_ks
1009
        ; tcExtendKindEnv name_ks thing_inside }
1010
  where
1011 1012 1013 1014
    -- 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
1015
    kc_tv :: LHsTyVarBndr Name -> Kind -> TcM (Name, Kind)
1016
    kc_tv (L _ (UserTyVar n)) exp_k 
1017
      = return (n, exp_k)
1018
    kc_tv (L _ (KindedTyVar n hs_k)) exp_k
1019
      = do { k <- tcLHsKind hs_k
1020
           ; checkKind k exp_k
1021
           ; return (n, exp_k) }
1022 1023

-----------------------
1024
tcTyClTyVars :: Name -> LHsTyVarBndrs Name	-- LHS of the type or class decl
dreixel's avatar
dreixel committed
1025
             -> ([TyVar] -> Kind -> TcM a) -> TcM a
1026 1027
-- Used for the type variables of a type or class decl,
-- on the second pass when constructing the final result
1028 1029 1030
-- (tcTyClTyVars T [a,b] thing_inside) 
--   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
--   calls thing_inside with arguments
1031 1032 1033
--      [k1,k2,a,b] (k2 -> *)
--   having also extended the type environment with bindings 
--   for k1,k2,a,b
dreixel's avatar
dreixel committed
1034 1035 1036
--
-- 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
1037 1038 1039 1040
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
1041
    do { thing <- tcLookup tycon
1042 1043 1044
       ; let { kind = case thing of
                        AThing kind -> kind
                        _ -> panic "tcTyClTyVars"
dreixel's avatar
dreixel committed
1045 1046 1047
                     -- We only call tcTyClTyVars during typechecking in
                     -- TcTyClDecls, where the local env is extended with
                     -- the generalized_env (mapping Names to AThings).
1048 1049 1050 1051 1052 1053 1054
             ; (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
1055
                                                  ; checkKind kind tc_kind
1056
                                                  ; return (mkTyVar n kind) }
1057 1058

-----------------------------------
dreixel's avatar
dreixel committed
1059
tcDataKindSig :: Kind -> TcM [TyVar]
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1060
-- GADT decls can have a (perhaps partial) kind signature
1061 1062
--	e.g.  data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for 
1063 1064
-- 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
1065
tcDataKindSig kind
1066 1067 1068
  = do	{ checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
	; span <- getSrcSpanM
	; us   <- newUniqueSupply 
1069 1070
	; let uniqs = uniqsFromSupply us
	; return [ mk_tv span uniq str kind 
1071
		 | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
1072 1073 1074 1075 1076 1077
  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
1078 1079
	  
    dnames = map ('$' :) names	-- Note [Avoid name clashes for associated data types]
1080

1081
    names :: [String]
1082 1083 1084 1085
    names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] 

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

1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107
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.)

1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148

%************************************************************************
%*									*
		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}
1149
tcHsPatSigType :: UserTypeCtxt
1150 1151 1152 1153
	       -> HsWithBndrs (LHsType Name)  -- The type signature
	      -> TcM ( Type                   -- The signature
                      , [(Name, TcTyVar)] )   -- The new bit of type environment, binding
				              -- the scoped type variables
1154 1155 1156 1157
-- 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
1158

1159
tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs, hswb_tvs = sig_tvs })
1160
  = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
1161
    do	{ kvs <- mapM new_kv sig_kvs
1162
        ; tvs <- mapM new_tv sig_tvs
1163 1164
        ; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs)
	; sig_ty <- tcExtendTyVarEnv2 ktv_binds $
1165 1166
                    tcHsLiftedType hs_ty
        ; sig_ty <- zonkTcType sig_ty
1167
	; checkValidType ctxt sig_ty 
1168 1169 1170 1171 1172 1173 1174 1175 1176 1177
	; 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]
1178 1179

tcPatSig :: UserTypeCtxt
1180
	 -> HsWithBndrs (LHsType Name)
1181
	 -> TcSigmaType
1182 1183 1184 1185 1186
	 -> 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
1187
tcPatSig ctxt sig res_ty
1188
  = do	{ (sig_ty, sig_tvs) <- tcHsPatSigType ctxt sig
1189 1190 1191
    	-- sig_tvs are the type variables free in 'sig', 
	-- and not already in scope. These are the ones
	-- that should be brought into scope
1192 1193

	; if null sig_tvs then do {
1194
		-- Just do the subsumption check and return
1195
                  wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
1196
		; return (sig_ty, [], wrap)
1197
        } else do
1198 1199 1200
		-- Type signature binds at least one scoped type variable
	
		-- A pattern binding cannot bind scoped type variables
1201 1202 1203
                -- It is more convenient to make the test here
                -- than in the renamer
	{ let in_pat_bind = case ctxt of
1204
				BindPatSigCtxt -> True
Ian Lynagh's avatar
Ian Lynagh committed
1205
				_              -> False
1206
	; when in_pat_bind (addErr (patBindSigErr sig_tvs))
1207

1208 1209 1210 1211 1212 1213 1214
		-- 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
1215 1216
	; let bad_tvs = [ tv | (_, tv) <- sig_tvs
                             , not (tv `elemVarSet` exactTyVarsOfType sig_ty) ]
1217 1218
	; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)

1219
	-- Now do a subsumption check of the pattern signature against res_ty
1220 1221
	; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty

1222
	-- Phew!
1223
        ; return (sig_ty, sig_tvs, wrap)
1224
        } }
1225

1226
patBindSigErr :: [(Name, TcTyVar)] -> SDoc
1227 1228
patBindSigErr sig_tvs 
  = hang (ptext (sLit "You cannot bind scoped type variable") <> plural sig_tvs
1229
          <+> pprQuotedList (map fst sig_tvs))
1230
       2 (ptext (sLit "in a pattern binding signature"))
1231 1232
\end{code}

1233 1234 1235 1236 1237 1238 1239 1240 1241
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
1242
   TcErrors.getSkolemInfo can thereby find the binding site for the skolem.
1243 1244 1245 1246 1247

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

 * Then unificaiton makes a_sig := a_sk

1248 1249
That's why we must make a_sig a MetaTv (albeit a SigTv), 
not a SkolemTv, so that it can unify to a_sk.
1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274

For RULE binders, though, things are a bit different (yuk).  
  RULE "foo" forall (x::a) (y::[a]).  f x y = ...
Here this really is the binding site of the type variable so we'd like
to use a skolem, so that we get a complaint if we unify two of them
together.

Note [Unifying SigTvs]
~~~~~~~~~~~~~~~~~~~~~~
ALAS we have no decent way of avoiding two SigTvs getting unified.  
Consider
  f (x::(a,b)) (y::c)) = [fst x, y]
Here we'd really like to complain that 'a' and 'c' are unified. But
for the reasons above we can't make a,b,c into skolems, so they
are just SigTvs that can unify.  And indeed, this would be ok,
  f x (y::c) = case x of
                 (x1 :: a1, True) -> [x,y]
                 (x1 :: a2, False) -> [x,y,y]
Here the type of x's first component is called 'a1' in one branch and
'a2' in the other.  We could try insisting on the same OccName, but
they definitely won't have the sane lexical Name. 

I think we could solve this by recording in a SigTv a list of all the 
in-scope varaibles that it should not unify with, but it's fiddly.

1275

1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291
%************************************************************************
%*                                                                      *
        Checking kinds
%*                                                                      *
%************************************************************************

We would like to get a decent error message from
  (a) Under-applied type constructors
             f :: (Maybe, Maybe)