TcHsType.lhs 62.9 KB
 Simon Marlow committed Oct 11, 2006 1 2 % % (c) The University of Glasgow 2006 simonpj committed Oct 09, 2003 3 4 5 6 7 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % \section[TcMonoType]{Typechecking user-specified @MonoTypes@} \begin{code} Ian Lynagh committed Nov 04, 2011 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 simonpj committed Oct 09, 2003 15 module TcHsType ( chak@cse.unsw.edu.au. committed Oct 31, 2011 16 tcHsSigType, tcHsSigTypeNC, tcHsDeriv, tcHsVectInst, Simon Peyton Jones committed Mar 02, 2012 17 tcHsInstHead, simonpj committed Oct 09, 2003 18 19 UserTypeCtxt(..), Simon Peyton Jones committed Mar 02, 2012 20 21 -- Type checking type and class decls kcTyClTyVars, tcTyClTyVars, Simon Peyton Jones committed Jun 07, 2012 22 tcHsConArgType, tcDataKindSig, Simon Peyton Jones committed Mar 02, 2012 23 tcClassSigType, dreixel committed Nov 11, 2011 24 Simon Peyton Jones committed Mar 02, 2012 25 26 -- Kind-checking types -- No kind generalisation, no checkValidType Simon Peyton Jones committed Jun 07, 2012 27 kcHsTyVarBndrs, tcHsTyVarBndrs, Simon Peyton Jones committed Jun 07, 2012 28 tcHsLiftedType, tcHsOpenType, Simon Peyton Jones committed Mar 02, 2012 29 30 tcLHsType, tcCheckLHsType, tcHsContext, tcInferApps, tcHsArgTys, batterseapower committed Sep 06, 2011 31 Simon Peyton Jones committed Sep 28, 2012 32 kindGeneralize, checkKind, Simon Peyton Jones committed Mar 02, 2012 33 34 35 -- Sort-checking kinds tcLHsKind, simonpj committed Oct 09, 2003 36 simonpj@microsoft.com committed Jan 25, 2006 37 38 -- Pattern type signatures tcHsPatSigType, tcPatSig simonpj committed Oct 09, 2003 39 40 41 42 ) where #include "HsVersions.h" simonpj@microsoft.com committed May 27, 2009 43 #ifdef GHCI /* Only if bootstrapped */ Simon Peyton Jones committed Mar 02, 2012 44 import {-# SOURCE #-} TcSplice( tcSpliceType ) simonpj@microsoft.com committed May 27, 2009 45 46 #endif Simon Marlow committed Oct 11, 2006 47 import HsSyn Simon Peyton Jones committed Mar 02, 2012 48 import TcHsSyn ( zonkTcTypeToType, emptyZonkEnv ) simonpj committed Oct 09, 2003 49 import TcRnMonad Simon Peyton Jones committed Dec 05, 2011 50 import TcEvidence( HsWrapper ) Simon Marlow committed Oct 11, 2006 51 52 import TcEnv import TcMType Simon Peyton Jones committed Jan 08, 2013 53 import TcValidity Simon Marlow committed Oct 11, 2006 54 55 56 import TcUnify import TcIface import TcType Simon Peyton Jones committed Mar 02, 2012 57 import Type dreixel committed Nov 11, 2011 58 import Kind Simon Peyton Jones committed Mar 02, 2012 59 import TypeRep( mkNakedTyConApp ) Simon Marlow committed Oct 11, 2006 60 import Var simonpj@microsoft.com committed Aug 25, 2009 61 import VarSet Simon Marlow committed Oct 11, 2006 62 import TyCon Simon Peyton Jones committed Feb 06, 2012 63 import DataCon dreixel committed Nov 11, 2011 64 import TysPrim ( liftedTypeKindTyConName, constraintKindTyConName ) Simon Marlow committed Oct 11, 2006 65 66 import Class import Name Simon Peyton Jones committed Mar 02, 2012 67 import NameEnv Simon Marlow committed Oct 11, 2006 68 69 70 import TysWiredIn import BasicTypes import SrcLoc Simon Peyton Jones committed Nov 26, 2012 71 import ErrUtils ( isEmptyMessages ) Simon Peyton Jones committed Oct 31, 2012 72 import DynFlags ( ExtensionFlag( Opt_DataKinds ), getDynFlags ) Simon Peyton Jones committed Oct 12, 2012 73 import Unique Simon Marlow committed Oct 11, 2006 74 import UniqSupply simonpj committed Oct 09, 2003 75 import Outputable Ian Lynagh committed Mar 29, 2008 76 import FastString Ian Lynagh committed Jun 05, 2012 77 78 import Util Simon Peyton Jones committed Mar 02, 2012 79 import Control.Monad ( unless, when, zipWithM ) Simon Peyton Jones committed Oct 12, 2012 80 import PrelNames( ipClassName, funTyConKey ) simonpj committed Oct 09, 2003 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. %************************************************************************ %* * Simon Peyton Jones committed Mar 02, 2012 162 Check types AND do validity checking simonpj committed Oct 09, 2003 163 164 165 166 %* * %************************************************************************ \begin{code} simonpj@microsoft.com committed May 27, 2009 167 tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type simonpj committed Dec 24, 2004 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 Simon Peyton Jones committed Mar 02, 2012 171 tcHsSigType ctxt hs_ty simonpj committed Oct 13, 2003 172 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $simonpj@microsoft.com committed May 27, 2009 173 174 tcHsSigTypeNC ctxt hs_ty Simon Peyton Jones committed Mar 02, 2012 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 dreixel committed Nov 16, 2011 181 182 -- The kind is checked by checkValidType, and isn't necessarily -- of kind * in a Template Haskell quote eg [t| Maybe |] simonpj committed Jan 27, 2005 183 Simon Peyton Jones committed Feb 14, 2013 184 -- Generalise here: see Note [Kind generalisation] Simon Peyton Jones committed Mar 02, 2012 185 ; ty <- tcCheckHsTypeAndGen hs_ty kind dreixel committed Nov 11, 2011 186 Simon Peyton Jones committed Mar 02, 2012 187 188 189 190 -- Zonk to expose kind information to checkValidType ; ty <- zonkTcType ty ; checkValidType ctxt ty ; return ty } dreixel committed Nov 11, 2011 191 Simon Peyton Jones committed Mar 02, 2012 192 ----------------- dreixel committed Nov 11, 2011 193 tcHsInstHead :: UserTypeCtxt -> LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type]) Simon Peyton Jones committed Mar 02, 2012 194 -- Like tcHsSigTypeNC, but for an instance head. Simon Peyton Jones committed Apr 30, 2013 195 tcHsInstHead user_ctxt lhs_ty@(L loc hs_ty) Simon Peyton Jones committed Mar 02, 2012 196 = setSrcSpan loc $-- The "In the type..." context comes from the caller Simon Peyton Jones committed Apr 30, 2013 197 do { inst_ty <- tc_inst_head hs_ty Simon Peyton Jones committed May 03, 2013 198 199 ; kvs <- zonkTcTypeAndFV inst_ty ; kvs <- kindGeneralize kvs [] Simon Peyton Jones committed Apr 30, 2013 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 committed Sep 06, 2011 212 Simon Peyton Jones committed Mar 02, 2012 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) Simon Peyton Jones committed Mar 09, 2012 226 Nothing -> failWithTc (ptext (sLit "Illegal deriving item") <+> quotes (ppr hs_ty)) } chak@cse.unsw.edu.au. committed Oct 31, 2011 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 Simon Peyton Jones committed Mar 02, 2012 233 234 235 = do { (cls, cls_kind) <- tcClass cls_name ; (arg_tys, _res_kind) <- tcInferApps cls_name cls_kind tys ; return (cls, arg_tys) } chak@cse.unsw.edu.au. committed Oct 31, 2011 236 237 | otherwise = failWithTc $ptext (sLit "Malformed instance type") simonpj committed Oct 09, 2003 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 %************************************************************************ %* * Simon Peyton Jones committed Mar 02, 2012 247 The main kind checker: no validity checks here simonpj committed Oct 09, 2003 248 249 250 251 252 253 %* * %************************************************************************ First a couple of simple wrappers for kcHsType \begin{code} Simon Peyton Jones committed Mar 02, 2012 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 batterseapower committed May 15, 2012 266 tcHsConArgType DataType bty = tcHsOpenType (getBangType bty) Simon Peyton Jones committed Mar 02, 2012 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 simonpj committed Oct 09, 2003 271 --------------------------- Simon Peyton Jones committed Mar 02, 2012 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..] ] Simon Peyton Jones committed Oct 22, 2011 283 dreixel committed Nov 11, 2011 284 --------------------------- batterseapower committed May 15, 2012 285 tcHsOpenType, tcHsLiftedType :: LHsType Name -> TcM TcType Simon Peyton Jones committed Mar 02, 2012 286 287 -- Used for type signatures -- Do not do validity checking batterseapower committed May 15, 2012 288 tcHsOpenType ty = addTypeCtxt ty$ tc_lhs_type ty ekOpen Simon Peyton Jones committed Mar 02, 2012 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$ Simon Peyton Jones committed Oct 19, 2012 295 tc_lhs_type hs_ty (EK exp_kind expectedKindMsg) Simon Peyton Jones committed Mar 02, 2012 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 committed Nov 11, 2011 300 simonpj committed Oct 09, 2003 301 --------------------------- Simon Peyton Jones committed Mar 02, 2012 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 Simon Peyton Jones committed Oct 19, 2012 307 = do { ty <- tc_hs_type hs_ty (EK kind expectedKindMsg) Simon Peyton Jones committed May 03, 2013 308 309 310 311 ; traceTc "tcCheckHsTypeAndGen" (ppr hs_ty) ; traceTc "tcCheckHsTypeAndGen" (ppr ty) ; kvs <- zonkTcTypeAndFV ty ; kvs <- kindGeneralize kvs [] Simon Peyton Jones committed Mar 02, 2012 312 ; return (mkForAllTys kvs ty) } simonpj committed Oct 09, 2003 313 314 \end{code} Simon Peyton Jones committed Mar 02, 2012 315 Like tcExpr, tc_hs_type takes an expected kind which it unifies with dreixel committed Nov 16, 2011 316 the kind it figures out. When we don't know what kind to expect, we use Simon Peyton Jones committed Mar 02, 2012 317 tc_lhs_type_fresh, to first create a new meta kind variable and use that as dreixel committed Nov 16, 2011 318 the expected kind. simonpj committed Oct 09, 2003 319 320 \begin{code} Simon Peyton Jones committed Mar 02, 2012 321 322 323 tc_infer_lhs_type :: LHsType Name -> TcM (TcType, TcKind) tc_infer_lhs_type ty = do { kv <- newMetaKindVar Simon Peyton Jones committed Oct 19, 2012 324 ; r <- tc_lhs_type ty (EK kv expectedKindMsg) Simon Peyton Jones committed Mar 02, 2012 325 326 327 328 ; return (r, kv) } tc_lhs_type :: LHsType Name -> ExpKind -> TcM TcType tc_lhs_type (L span ty) exp_kind simonpj@microsoft.com committed Feb 04, 2009 329 = setSrcSpan span $Simon Peyton Jones committed Mar 02, 2012 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 Simon Peyton Jones committed Oct 12, 2012 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') } Simon Peyton Jones committed Mar 02, 2012 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 parcs committed Sep 06, 2012 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) Simon Peyton Jones committed Mar 02, 2012 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 } Simon Peyton Jones committed Oct 12, 2012 368 369 tc_hs_type ty@(HsFunTy ty1 ty2) exp_kind = tc_fun_type ty ty1 ty2 exp_kind Simon Peyton Jones committed Mar 02, 2012 370 371 tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind Simon Peyton Jones committed Oct 12, 2012 372 373 374 | op hasKey funTyConKey = tc_fun_type hs_ty ty1 ty2 exp_kind | otherwise Simon Peyton Jones committed Mar 02, 2012 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 Simon Peyton Jones committed Oct 12, 2012 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 Simon Peyton Jones committed Mar 02, 2012 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 committed May 15, 2013 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)? Simon Peyton Jones committed Oct 12, 2012 393 394 where (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2] Simon Peyton Jones committed Mar 02, 2012 395 396 --------- Foralls Simon Peyton Jones committed Apr 30, 2013 397 tc_hs_type hs_ty@(HsForAllTy _ hs_tvs context ty) exp_kind Simon Peyton Jones committed Mar 02, 2012 398 399 400 = tcHsTyVarBndrs hs_tvs \ tvs' -> -- Do not kind-generalise here! See Note [Kind generalisation] do { ctxt' <- tcHsContext context Simon Peyton Jones committed Apr 30, 2013 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 Simon Peyton Jones committed Apr 30, 2013 405 -- _function_, so the kind of the result really is * Simon Peyton Jones committed Apr 30, 2013 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 } Simon Peyton Jones committed Mar 02, 2012 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) } twanvl committed Jan 17, 2008 423 dreixel committed Nov 16, 2011 424 -- See Note [Distinguishing tuple kinds] in HsTypes Simon Peyton Jones committed Mar 02, 2012 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 committed Nov 25, 2011 430 431 | otherwise = do { k <- newMetaKindVar Simon Peyton Jones committed Nov 26, 2012 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 Simon Peyton Jones committed Mar 02, 2012 452 -- check the arguments again to give good error messages dreixel committed Nov 25, 2011 453 454 -- in eg. (Maybe, Maybe) Simon Peyton Jones committed Mar 02, 2012 455 456 tc_hs_type hs_ty@(HsTupleTy tup_sort tys) exp_kind = tc_tuple hs_ty tup_sort tys exp_kind dreixel committed Nov 25, 2011 457 Simon Peyton Jones committed Mar 02, 2012 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] Simon Peyton Jones committed Mar 02, 2012 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 Simon Peyton Jones committed Oct 19, 2012 481 = do { ty' <- tc_lhs_type ty ekLifted Simon Peyton Jones committed Mar 02, 2012 482 ; checkExpectedKind ipTy constraintKind exp_kind Simon Peyton Jones committed Jun 13, 2012 483 484 485 486 ; ipClass <- tcLookupClass ipClassName ; let n' = mkStrLitTy hsIPNameFS n ; return (mkClassPred ipClass [n',ty']) } Simon Peyton Jones committed Mar 02, 2012 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 Simon Peyton Jones committed Oct 19, 2012 492 (EK kind1 msg_fn) Simon Peyton Jones committed Mar 02, 2012 493 494 ; checkExpectedKind ty constraintKind exp_kind ; return (mkNakedTyConApp eqTyCon [kind1, ty1', ty2']) } Simon Peyton Jones committed Oct 19, 2012 495 496 497 where msg_fn pkind = ptext (sLit "The left argument of the equality had kind") <+> quotes (pprKind pkind) Simon Peyton Jones committed Mar 02, 2012 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 Simon Peyton Jones committed Oct 19, 2012 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) Simon Peyton Jones committed Mar 02, 2012 507 508 509 510 tc_hs_type (HsCoreTy ty) exp_kind = do { checkExpectedKind ty (typeKind ty) exp_kind ; return ty } dreixel committed Nov 25, 2011 511 512 Simon Peyton Jones committed Mar 02, 2012 513 #ifdef GHCI /* Only if bootstrapped */ Simon Peyton Jones committed Apr 05, 2012 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 Simon Peyton Jones committed Mar 02, 2012 517 tc_hs_type hs_ty@(HsSpliceTy sp fvs _) exp_kind Simon Peyton Jones committed Apr 05, 2012 518 519 520 = do { s <- getStage ; traceTc "tc_hs_type: splice" (ppr sp$$ ppr s) ; (ty, kind) <- tcSpliceType sp fvs Simon Peyton Jones committed Mar 02, 2012 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 committed Nov 25, 2011 531 Simon Peyton Jones committed Dec 19, 2012 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 Simon Peyton Jones committed Jan 25, 2013 538 539 = do { checkExpectedKind hs_ty typeSymbolKind exp_kind ; checkWiredInTyCon typeSymbolKindCon Simon Peyton Jones committed Dec 19, 2012 540 ; return (mkStrLitTy s) } Iavor S. Diatchki committed Mar 13, 2012 541 Simon Peyton Jones committed Mar 02, 2012 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 committed Nov 25, 2011 548 549 550 where arg_kind = case tup_sort of HsBoxedTuple -> liftedTypeKind batterseapower committed May 15, 2012 551 HsUnboxedTuple -> openTypeKind dreixel committed Nov 25, 2011 552 HsConstraintTuple -> constraintKind Simon Peyton Jones committed Mar 02, 2012 553 _ -> panic "tc_hs_type arg_kind" dreixel committed Nov 25, 2011 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") Simon Peyton Jones committed Mar 02, 2012 558 _ -> panic "tc_hs_type tup_sort" dreixel committed Nov 11, 2011 559 Simon Peyton Jones committed Mar 02, 2012 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 batterseapower committed May 15, 2012 574 HsUnboxedTuple -> unliftedTypeKind Simon Peyton Jones committed Mar 02, 2012 575 576 577 HsBoxedTuple -> liftedTypeKind HsConstraintTuple -> constraintKind _ -> panic "tc_hs_type arg_kind" Iavor S. Diatchki committed Jan 24, 2012 578 simonpj committed Oct 09, 2003 579 --------------------------- Simon Peyton Jones committed Mar 02, 2012 580 tcInferApps :: Outputable a simonpj@microsoft.com committed Feb 04, 2009 581 582 => a -> TcKind -- Function kind simonmar committed Dec 10, 2003 583 -> [LHsType Name] -- Arg types Simon Peyton Jones committed Mar 02, 2012 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 simonpj@microsoft.com committed Feb 04, 2009 588 589 ; return (args', res_kind) } Simon Peyton Jones committed Mar 02, 2012 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 } simonpj committed Oct 09, 2003 600 simonpj@microsoft.com committed Feb 04, 2009 601 --------------------------- Simon Peyton Jones committed Mar 02, 2012 602 603 604 splitFunKind :: SDoc -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind) splitFunKind the_fun fun_kind args = go 1 fun_kind args simonpj@microsoft.com committed Feb 04, 2009 605 where Simon Peyton Jones committed Mar 02, 2012 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) } } simonpj@microsoft.com committed May 13, 2009 615 too_many_args = quotes the_fun <+> Ian Lynagh committed Apr 12, 2008 616 ptext (sLit "is applied to too many type arguments") simonpj committed Oct 09, 2003 617 Simon Peyton Jones committed Mar 02, 2012 618 simonpj committed Oct 09, 2003 619 --------------------------- Simon Peyton Jones committed Mar 02, 2012 620 621 tcHsContext :: LHsContext Name -> TcM [PredType] tcHsContext ctxt = mapM tcHsLPredType (unLoc ctxt) simonpj committed Apr 05, 2004 622 Simon Peyton Jones committed Mar 02, 2012 623 624 tcHsLPredType :: LHsType Name -> TcM PredType tcHsLPredType pred = tc_lhs_type pred ekConstraint simonpj committed Oct 09, 2003 625 626 --------------------------- Simon Peyton Jones committed Mar 02, 2012 627 tcTyVar :: Name -> TcM (TcType, TcKind) dreixel committed Nov 11, 2011 628 629 -- See Note [Type checking recursive type and class declarations] -- in TcTyClsDecls Simon Peyton Jones committed Mar 02, 2012 630 tcTyVar name -- Could be a tyvar, a tycon, or a datacon dreixel committed Nov 11, 2011 631 632 633 634 = do { traceTc "lk1" (ppr name) ; thing <- tcLookup name ; traceTc "lk2" (ppr name <+> ppr thing) ; case thing of Simon Peyton Jones committed Sep 10, 2012 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) Simon Peyton Jones committed Mar 02, 2012 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 jpm@cs.ox.ac.uk committed Nov 21, 2012 650 651 652 -> do { data_kinds <- xoptM Opt_DataKinds ; unless data_kinds$ promotionErr name NoDataKinds ; inst_tycon (mkTyConApp tc) (tyConKind tc) } Simon Peyton Jones committed Jan 25, 2013 653 654 655 | otherwise -> failWithTc (ptext (sLit "Data constructor") <+> quotes (ppr dc) <+> ptext (sLit "comes from an un-promotable type") <+> quotes (ppr (dataConTyCon dc))) Simon Peyton Jones committed Mar 02, 2012 656 Simon Peyton Jones committed Jul 10, 2012 657 APromotionErr err -> promotionErr name err Simon Peyton Jones committed Mar 02, 2012 658 659 _ -> wrongThingErr "type" thing name } dreixel committed Nov 11, 2011 660 where Simon Peyton Jones committed Mar 02, 2012 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 committed Nov 11, 2011 673 674 | otherwise = do { traceTc "lk4" (ppr name <+> dcolon <+> ppr kind) Simon Peyton Jones committed Mar 02, 2012 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) simonpj committed Oct 09, 2003 696 697 \end{code} Simon Peyton Jones committed Mar 02, 2012 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. simonpj committed Oct 09, 2003 703 Simon Peyton Jones committed Mar 02, 2012 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. simonpj committed Oct 09, 2003 778 dreixel committed Nov 11, 2011 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 simonpj committed Mar 11, 2005 808 809 (a) spurious ! annotations. (b) a class used as a type simonpj committed Oct 09, 2003 810 dreixel committed Nov 11, 2011 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. simonpj committed Oct 09, 2003 826 827 828 829 Help functions for type applications ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} Simon Peyton Jones committed Mar 02, 2012 830 addTypeCtxt :: LHsType Name -> TcM a -> TcM a simonpj@microsoft.com committed Feb 04, 2009 831 -- Wrap a context around only if we want to show that contexts. batterseapower committed Sep 06, 2011 832 -- Omit invisble ones and ones user's won't grok Simon Peyton Jones committed Mar 02, 2012 833 834 835 836 addTypeCtxt (L _ ty) thing = addErrCtxt doc thing where doc = ptext (sLit "In the type") <+> quotes (ppr ty) simonpj committed Sep 30, 2004 837 \end{code} simonpj committed Oct 09, 2003 838 839 840 841 842 843 844 %************************************************************************ %* * Type-variable binders %* * %************************************************************************ dreixel committed Nov 11, 2011 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) simonpj committed Oct 09, 2003 859 860 \begin{code} Simon Peyton Jones committed Jul 10, 2012 861 kcScopedKindVars :: [Name] -> TcM a -> TcM a Simon Peyton Jones committed Mar 02, 2012 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 Simon Peyton Jones committed Jul 10, 2012 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 } Simon Peyton Jones committed Jun 07, 2012 869 Simon Peyton Jones committed Oct 19, 2012 870 871 kcHsTyVarBndrs :: Bool -- True <=> full kind signature provided -- Default UserTyVar to * Simon Peyton Jones committed Jul 10, 2012 872 -- and use KindVars not meta kind vars Simon Peyton Jones committed Jun 07, 2012 873 874 875 -> LHsTyVarBndrs Name -> ([TcKind] -> TcM r) -> TcM r Simon Peyton Jones committed Oct 19, 2012 876 -- Used in getInitialKind Simon Peyton Jones committed Jul 10, 2012 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) $Simon Peyton Jones committed Jun 07, 2012 882 do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs Simon Peyton Jones committed Jul 10, 2012 883 ; tcExtendKindEnv nks (thing_inside (map snd nks)) } } Simon Peyton Jones committed Jun 07, 2012 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 Simon Peyton Jones committed Jul 10, 2012 889 890 891 Just (AThing k) -> return k _ | full_kind_sig -> return liftedTypeKind | otherwise -> newMetaKindVar Simon Peyton Jones committed Jun 07, 2012 892 893 894 ; return (n, kind) } kc_hs_tv (KindedTyVar n k) = do { kind <- tcLHsKind k Simon Peyton Jones committed Oct 19, 2012 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) Simon Peyton Jones committed Jun 07, 2012 903 ; return (n, kind) } Simon Peyton Jones committed Mar 02, 2012 904 Simon Peyton Jones committed May 11, 2012 905 tcHsTyVarBndrs :: LHsTyVarBndrs Name 906 -> ([TcTyVar] -> TcM r) Simon Peyton Jones committed Mar 02, 2012 907 -> TcM r Simon Peyton Jones committed May 03, 2013 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 } } Simon Peyton Jones committed Mar 02, 2012 924 925 tcHsTyVarBndr :: LHsTyVarBndr Name -> TcM TcTyVar Simon Peyton Jones committed Mar 02, 2012 926 -- Return a type variable dreixel committed Nov 11, 2011 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 Simon Peyton Jones committed Mar 02, 2012 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 Simon Peyton Jones committed May 11, 2012 946 KindedTyVar _ kind -> tcLHsKind kind Simon Peyton Jones committed Apr 25, 2012 947 ; return (mkTcTyVar name kind (SkolemTv False)) } } } simonpj committed Oct 09, 2003 948 949 ------------------ Simon Peyton Jones committed Jul 10, 2012 950 951 952 953 kindGeneralize :: TyVarSet -> [Name] -> TcM [KindVar] kindGeneralize tkvs _names_to_avoid = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked ; tkvs <- zonkTyVarsAndFV tkvs Simon Peyton Jones committed May 24, 2012 954 ; let kvs_to_quantify = filter isKindVar (varSetElems (tkvs minusVarSet gbl_tvs)) Simon Peyton Jones committed Jul 10, 2012 955 956 -- ToDo: remove the (filter isKindVar) -- Any type variables in tkvs will be in scope, Simon Peyton Jones committed Apr 25, 2012 957 958 -- and hence in gbl_tvs, so after removing gbl_tvs -- we should only have kind variables left Simon Peyton Jones committed May 24, 2012 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! Simon Peyton Jones committed Mar 02, 2012 965 Simon Peyton Jones committed Jul 10, 2012 966 ; traceTc "kindGeneralise" (vcat [ppr kvs_to_quantify]) Simon Peyton Jones committed Mar 02, 2012 967 ; ASSERT2 (all isKindVar kvs_to_quantify, ppr kvs_to_quantify  ppr tkvs) Simon Peyton Jones committed Jul 10, 2012 968 -- This assertion is obviosly true because of the filter isKindVar Simon Peyton Jones committed May 24, 2012 969 970 -- but we'll remove that when reorganising TH, and then the assertion -- will mean something Simon Peyton Jones committed Jul 10, 2012 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 committed Nov 11, 2011 976 977 \end{code} Simon Peyton Jones committed Mar 02, 2012 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 committed Jan 30, 2013 991 would be *less applicable* than f1, because it requires a more Simon Peyton Jones committed Mar 02, 2012 992 993 polymorphic argument. dreixel committed Nov 11, 2011 994 995 Note [Kinds of quantified type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Simon Peyton Jones committed Mar 02, 2012 996 tcTyVarBndrsGen quantifies over a specified list of type variables, dreixel committed Nov 11, 2011 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! Simon Peyton Jones committed Mar 02, 2012 1011 Hence using zonked_kinds when forming tvs'. dreixel committed Nov 11, 2011 1012 1013 \begin{code} Simon Peyton Jones committed Mar 02, 2012 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) } Simon Peyton Jones committed Oct 19, 2012 1028 kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> TcM a -> TcM a Simon Peyton Jones committed Mar 14, 2012 1029 -- Used for the type variables of a type or class decl, Simon Peyton Jones committed Mar 02, 2012 1030 -- when doing the initial kind-check. Simon Peyton Jones committed May 11, 2012 1031 kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside Simon Peyton Jones committed Jul 10, 2012 1032 = kcScopedKindVars kvs $Simon Peyton Jones committed Mar 02, 2012 1033 do { tc_kind <- kcLookupKind name Simon Peyton Jones committed Oct 19, 2012 1034 ; let (arg_ks, _res_k) = splitKindFunTysN (length hs_tvs) tc_kind Simon Peyton Jones committed Mar 02, 2012 1035 1036 1037 -- There should be enough arrows, because -- getInitialKinds used the tcdTyVars ; name_ks <- zipWithM kc_tv hs_tvs arg_ks Simon Peyton Jones committed Oct 19, 2012 1038 ; tcExtendKindEnv name_ks thing_inside } Simon Peyton Jones committed Mar 02, 2012 1039 where Simon Peyton Jones committed Oct 19, 2012 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 Simon Peyton Jones committed Mar 02, 2012 1044 kc_tv :: LHsTyVarBndr Name -> Kind -> TcM (Name, Kind) Simon Peyton Jones committed Mar 14, 2012 1045 kc_tv (L _ (UserTyVar n)) exp_k Simon Peyton Jones committed Oct 19, 2012 1046 = return (n, exp_k) Simon Peyton Jones committed May 11, 2012 1047 kc_tv (L _ (KindedTyVar n hs_k)) exp_k Simon Peyton Jones committed Mar 02, 2012 1048 = do { k <- tcLHsKind hs_k Simon Peyton Jones committed Sep 28, 2012 1049 ; checkKind k exp_k Simon Peyton Jones committed Oct 19, 2012 1050 ; return (n, exp_k) } Simon Peyton Jones committed Mar 02, 2012 1051 1052 ----------------------- Simon Peyton Jones committed May 11, 2012 1053 tcTyClTyVars :: Name -> LHsTyVarBndrs Name -- LHS of the type or class decl dreixel committed Nov 11, 2011 1054 -> ([TyVar] -> Kind -> TcM a) -> TcM a Simon Peyton Jones committed Mar 02, 2012 1055 1056 -- Used for the type variables of a type or class decl, -- on the second pass when constructing the final result Simon Peyton Jones committed Feb 16, 2012 1057 1058 1059 -- (tcTyClTyVars T [a,b] thing_inside) -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> * -- calls thing_inside with arguments Simon Peyton Jones committed Mar 02, 2012 1060 1061 1062 -- [k1,k2,a,b] (k2 -> *) -- having also extended the type environment with bindings -- for k1,k2,a,b dreixel committed Nov 11, 2011 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 committed Aug 14, 2012 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 Simon Peyton Jones committed Jul 10, 2012 1070 do { thing <- tcLookup tycon Simon Peyton Jones committed Mar 02, 2012 1071 1072 1073 ; let { kind = case thing of AThing kind -> kind _ -> panic "tcTyClTyVars" dreixel committed Nov 11, 2011 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). Simon Peyton Jones committed Jul 10, 2012 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 Simon Peyton Jones committed Sep 28, 2012 1084 ; checkKind kind tc_kind Simon Peyton Jones committed Jul 10, 2012 1085 ; return (mkTyVar n kind) } simonpj committed Dec 03, 2004 1086 1087 ----------------------------------- dreixel committed Nov 11, 2011 1088 tcDataKindSig :: Kind -> TcM [TyVar] simonpj@microsoft.com committed Aug 08, 2006 1089 -- GADT decls can have a (perhaps partial) kind signature simonpj committed Dec 03, 2004 1090 1091 -- e.g. data T :: * -> * -> * where ... -- This function makes up suitable (kinded) type variables for chak@cse.unsw.edu.au. committed Sep 20, 2006 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 committed Nov 11, 2011 1094 tcDataKindSig kind simonpj committed Dec 03, 2004 1095 1096 1097 = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind) ; span <- getSrcSpanM ; us <- newUniqueSupply Simon Marlow committed May 11, 2007 1098 1099 ; let uniqs = uniqsFromSupply us ; return [ mk_tv span uniq str kind simonpj@microsoft.com committed Dec 30, 2008 1100 | ((kind, str), uniq) <- arg_kinds zip dnames zip uniqs ] } simonpj committed Dec 03, 2004 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 simonpj@microsoft.com committed Dec 30, 2008 1107 1108 dnames = map ('$' :) names -- Note [Avoid name clashes for associated data types] simonpj committed Dec 03, 2004 1109 simonpj@microsoft.com committed Dec 30, 2008 1110 names :: [String] simonpj committed Dec 03, 2004 1111 1112 1113 1114 names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ] badKindSig :: Kind -> SDoc badKindSig kind Ian Lynagh committed Apr 12, 2008 1115 = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind")) simonpj committed Dec 03, 2004 1116 2 (ppr kind) simonpj committed Oct 09, 2003 1117 1118 \end{code} simonpj@microsoft.com committed Dec 30, 2008 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.) simonpj committed Oct 09, 2003 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} simonpj@microsoft.com committed Jan 25, 2006 1178 tcHsPatSigType :: UserTypeCtxt Simon Peyton Jones committed May 11, 2012 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 simonpj@microsoft.com committed Jan 25, 2006 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 simonpj committed Sep 30, 2004 1187 Simon Peyton Jones committed May 11, 2012 1188 tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs, hswb_tvs = sig_tvs }) simonpj@microsoft.com committed Jan 25, 2006 1189 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $Simon Peyton Jones committed Apr 13, 2012 1190 do { kvs <- mapM new_kv sig_kvs Simon Peyton Jones committed Mar 02, 2012 1191 ; tvs <- mapM new_tv sig_tvs Simon Peyton Jones committed Apr 13, 2012 1192 1193 ; let ktv_binds = (sig_kvs zip kvs) ++ (sig_tvs zip tvs) ; sig_ty <- tcExtendTyVarEnv2 ktv_binds$