2 #include "HsVersions.h"
8 newTyVarTy, -- Kind -> NF_TcM s (TcType s)
9 newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
14 -----------------------------------------
15 SYN_IE(TcType), TcMaybe(..),
16 SYN_IE(TcTauType), SYN_IE(TcThetaType), SYN_IE(TcRhoType),
18 -- Find the type to which a type variable is bound
19 tcWriteTyVar, -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
20 tcReadTyVar, -- :: TcTyVar s -> NF_TcM (TcMaybe s)
23 tcSplitForAllTy, tcSplitRhoTy,
27 tcInstType, tcInstSigType, tcInstTcType, tcInstSigTcType,
28 tcInstTheta, tcInstId,
41 import Type ( SYN_IE(Type), SYN_IE(ThetaType), GenType(..),
42 tyVarsOfTypes, getTyVar_maybe,
43 splitForAllTy, splitRhoTy, isTyVarTy,
44 mkForAllTys, instantiateTy
46 import TyVar ( SYN_IE(TyVar), GenTyVar(..), SYN_IE(TyVarSet), SYN_IE(GenTyVarSet),
47 SYN_IE(TyVarEnv), lookupTyVarEnv, addOneToTyVarEnv,
48 nullTyVarEnv, mkTyVarEnv,
53 import Class ( GenClass, SYN_IE(Class) )
54 import TyCon ( isFunTyCon )
55 import Id ( idType, SYN_IE(Id) )
57 import TcKind ( TcKind )
59 import Usage ( SYN_IE(Usage), GenUsage, SYN_IE(UVar), duffUsage )
61 import TysPrim ( voidTy )
64 import Unique ( Unique )
65 import UniqFM ( UniqFM )
66 import Maybes ( assocMaybe )
67 import Util ( zipEqual, nOfThem, panic{-, pprPanic, pprTrace ToDo:rm-} )
76 type TcType s = GenType (TcTyVar s) UVar -- Used during typechecker
77 -- Invariant on ForAllTy in TcTypes:
79 -- a cannot occur inside a MutTyVar in T; that is,
80 -- T is "flattened" before quantifying over a
82 type TcThetaType s = [(Class, TcType s)]
83 type TcRhoType s = TcType s -- No ForAllTys
84 type TcTauType s = TcType s -- No DictTys or ForAllTys
86 type Box s = MutableVar s (TcMaybe s)
88 data TcMaybe s = UnBound
90 | DontBind -- This variant is used for tyvars
91 -- arising from type signatures, or
92 -- existentially quantified tyvars;
93 -- The idea is that we must not unify
94 -- such tyvars with anything except
97 -- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
98 -- because you get a synonym loop if you do!
100 type TcTyVar s = GenTyVar (Box s)
101 type TcTyVarSet s = GenTyVarSet (Box s)
105 tcTyVarToTyVar :: TcTyVar s -> TyVar
106 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
111 These tcSplit functions are like their non-Tc analogues, but they
112 follow through bound type variables.
115 tcSplitForAllTy :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
119 go syn_t (ForAllTy tv t) tvs = go t t (tv:tvs)
120 go syn_t (SynTy _ _ t) tvs = go syn_t t tvs
121 go syn_t (TyVarTy tv) tvs = tcReadTyVar tv `thenNF_Tc` \ maybe_ty ->
123 BoundTo ty | not (isTyVarTy ty) -> go syn_t ty tvs
124 other -> returnNF_Tc (reverse tvs, syn_t)
125 go syn_t t tvs = returnNF_Tc (reverse tvs, syn_t)
127 tcSplitRhoTy :: TcType s -> NF_TcM s ([(Class,TcType s)], TcType s)
131 go syn_t (FunTy (DictTy c t _) r _) ts = go r r ((c,t):ts)
132 go syn_t (AppTy (AppTy (TyConTy tycon _) (DictTy c t _)) r) ts
135 go syn_t (SynTy _ _ t) ts = go syn_t t ts
136 go syn_t (TyVarTy tv) ts = tcReadTyVar tv `thenNF_Tc` \ maybe_ty ->
138 BoundTo ty | not (isTyVarTy ty) -> go syn_t ty ts
139 other -> returnNF_Tc (reverse ts, syn_t)
140 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
148 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
150 = tcGetUnique `thenNF_Tc` \ uniq ->
151 tcNewMutVar UnBound `thenNF_Tc` \ box ->
152 returnNF_Tc (TyVar uniq kind Nothing box)
154 newTyVarTy :: Kind -> NF_TcM s (TcType s)
156 = newTcTyVar kind `thenNF_Tc` \ tc_tyvar ->
157 returnNF_Tc (TyVarTy tc_tyvar)
159 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
160 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
163 -- For signature type variables, mark them as "DontBind"
164 tcInstTyVars, tcInstSigTyVars
166 -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
168 tcInstTyVars tyvars = inst_tyvars UnBound tyvars
169 tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
171 inst_tyvars initial_cts tyvars
172 = mapNF_Tc (inst_tyvar initial_cts) tyvars `thenNF_Tc` \ tc_tyvars ->
174 tys = map TyVarTy tc_tyvars
176 returnNF_Tc (tc_tyvars, tys, zipEqual "inst_tyvars" tyvars tys)
178 inst_tyvar initial_cts (TyVar _ kind name _)
179 = tcGetUnique `thenNF_Tc` \ uniq ->
180 tcNewMutVar initial_cts `thenNF_Tc` \ box ->
181 returnNF_Tc (TyVar uniq kind name box)
184 @tcInstType@ and @tcInstSigType@ both create a fresh instance of a
185 type, returning a @TcType@. All inner for-alls are instantiated with
188 The difference is that tcInstType instantiates all forall'd type
189 variables (and their bindees) with UnBound type variables, whereas
190 tcInstSigType instantiates them with DontBind types variables.
191 @tcInstSigType@ also doesn't take an environment.
193 On the other hand, @tcInstTcType@ instantiates a TcType. It uses
194 instantiateTy which could take advantage of sharing some day.
197 tcInstTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
199 = tcSplitForAllTy ty `thenNF_Tc` \ (tyvars, rho) ->
201 [] -> returnNF_Tc ([], ty) -- Nothing to do
202 other -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
203 returnNF_Tc (tyvars', instantiateTy tenv rho)
205 tcInstSigTcType :: TcType s -> NF_TcM s ([TcTyVar s], TcType s)
207 = tcSplitForAllTy ty `thenNF_Tc` \ (tyvars, rho) ->
209 [] -> returnNF_Tc ([], ty) -- Nothing to do
210 other -> tcInstSigTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
211 returnNF_Tc (tyvars', instantiateTy tenv rho)
213 tcInstType :: [(GenTyVar flexi,TcType s)]
214 -> GenType (GenTyVar flexi) UVar
215 -> NF_TcM s (TcType s)
216 tcInstType tenv ty_to_inst
217 = tcConvert bind_fn occ_fn (mkTyVarEnv tenv) ty_to_inst
219 bind_fn = inst_tyvar UnBound
220 occ_fn env tyvar = case lookupTyVarEnv env tyvar of
221 Just ty -> returnNF_Tc ty
222 Nothing -> panic "tcInstType:1" --(vcat [ppr PprDebug ty_to_inst,
223 -- ppr PprDebug tyvar])
225 tcInstSigType :: GenType (GenTyVar flexi) UVar -> NF_TcM s (TcType s)
226 tcInstSigType ty_to_inst
227 = tcConvert bind_fn occ_fn nullTyVarEnv ty_to_inst
229 bind_fn = inst_tyvar DontBind
230 occ_fn env tyvar = case lookupTyVarEnv env tyvar of
231 Just ty -> returnNF_Tc ty
232 Nothing -> panic "tcInstType:2"-- (vcat [ppr PprDebug ty_to_inst,
233 -- ppr PprDebug tyvar])
235 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
236 zonkTcTyVarToTyVar tv
237 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
238 case tv_ty of -- Should be a tyvar!
240 TyVarTy tv' -> returnNF_Tc (tcTyVarToTyVar tv')
242 _ -> --pprTrace "zonkTcTyVarToTyVar:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
243 returnNF_Tc (tcTyVarToTyVar tv)
246 zonkTcTypeToType :: TyVarEnv Type -> TcType s -> NF_TcM s Type
247 zonkTcTypeToType env ty
248 = tcConvert zonkTcTyVarToTyVar occ_fn env ty
251 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
253 BoundTo (TyVarTy tyvar') -> lookup env tyvar'
254 BoundTo other_ty -> tcConvert zonkTcTyVarToTyVar occ_fn env other_ty
255 other -> lookup env tyvar
257 lookup env tyvar = case lookupTyVarEnv env tyvar of
258 Just ty -> returnNF_Tc ty
259 Nothing -> returnNF_Tc voidTy -- Unbound type variables go to Void
262 tcConvert bind_fn occ_fn env ty_to_convert
263 = doo env ty_to_convert
265 doo env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
267 doo env (SynTy tycon tys ty) = mapNF_Tc (doo env) tys `thenNF_Tc` \ tys' ->
268 doo env ty `thenNF_Tc` \ ty' ->
269 returnNF_Tc (SynTy tycon tys' ty')
271 doo env (FunTy arg res usage) = doo env arg `thenNF_Tc` \ arg' ->
272 doo env res `thenNF_Tc` \ res' ->
273 returnNF_Tc (FunTy arg' res' usage)
275 doo env (AppTy fun arg) = doo env fun `thenNF_Tc` \ fun' ->
276 doo env arg `thenNF_Tc` \ arg' ->
277 returnNF_Tc (AppTy fun' arg')
279 doo env (DictTy clas ty usage)= doo env ty `thenNF_Tc` \ ty' ->
280 returnNF_Tc (DictTy clas ty' usage)
282 doo env (ForAllUsageTy u us ty) = doo env ty `thenNF_Tc` \ ty' ->
283 returnNF_Tc (ForAllUsageTy u us ty')
285 -- The two interesting cases!
286 doo env (TyVarTy tv) = occ_fn env tv
288 doo env (ForAllTy tyvar ty)
289 = bind_fn tyvar `thenNF_Tc` \ tyvar' ->
291 new_env = addOneToTyVarEnv env tyvar (TyVarTy tyvar')
293 doo new_env ty `thenNF_Tc` \ ty' ->
294 returnNF_Tc (ForAllTy tyvar' ty')
297 tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s)
298 tcInstTheta tenv theta
301 go (clas,ty) = tcInstType tenv ty `thenNF_Tc` \ tc_ty ->
302 returnNF_Tc (clas, tc_ty)
304 -- A useful function that takes an occurrence of a global thing
305 -- and instantiates its type with fresh type variables
307 -> NF_TcM s ([TcTyVar s], -- It's instantiated type
313 (tyvars, rho) = splitForAllTy (idType id)
315 tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
316 tcInstType tenv rho `thenNF_Tc` \ rho' ->
318 (theta', tau') = splitRhoTy rho'
320 returnNF_Tc (tyvars', theta', tau')
323 Reading and writing TcTyVars
324 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
326 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
327 tcReadTyVar :: TcTyVar s -> NF_TcM s (TcMaybe s)
333 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
336 Reading is more interesting. The easy thing to do is just to read, thus:
338 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
341 But it's more fun to short out indirections on the way: If this
342 version returns a TyVar, then that TyVar is unbound. If it returns
343 any other type, then there might be bound TyVars embedded inside it.
345 We return Nothing iff the original box was unbound.
348 tcReadTyVar (TyVar uniq kind name box)
349 = tcReadMutVar box `thenNF_Tc` \ maybe_ty ->
351 BoundTo ty -> short_out ty `thenNF_Tc` \ ty' ->
352 tcWriteMutVar box (BoundTo ty') `thenNF_Tc_`
353 returnNF_Tc (BoundTo ty')
355 other -> returnNF_Tc other
357 short_out :: TcType s -> NF_TcM s (TcType s)
358 short_out ty@(TyVarTy (TyVar uniq kind name box))
359 = tcReadMutVar box `thenNF_Tc` \ maybe_ty ->
361 BoundTo ty' -> short_out ty' `thenNF_Tc` \ ty' ->
362 tcWriteMutVar box (BoundTo ty') `thenNF_Tc_`
365 other -> returnNF_Tc ty
367 short_out other_ty = returnNF_Tc other_ty
374 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
376 = mapNF_Tc zonkTcTyVar (tyVarSetToList tyvars) `thenNF_Tc` \ tys ->
377 returnNF_Tc (tyVarsOfTypes tys)
379 zonkTcTyVar :: TcTyVar s -> NF_TcM s (TcType s)
381 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
383 BoundTo ty@(TyVarTy tyvar') -> returnNF_Tc ty
384 BoundTo other -> zonkTcType other
385 other -> returnNF_Tc (TyVarTy tyvar)
387 zonkTcType :: TcType s -> NF_TcM s (TcType s)
389 zonkTcType (TyVarTy tyvar) = zonkTcTyVar tyvar
391 zonkTcType (AppTy ty1 ty2)
392 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
393 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
394 returnNF_Tc (AppTy ty1' ty2')
396 zonkTcType (TyConTy tc u)
397 = returnNF_Tc (TyConTy tc u)
399 zonkTcType (SynTy tc tys ty)
400 = mapNF_Tc zonkTcType tys `thenNF_Tc` \ tys' ->
401 zonkTcType ty `thenNF_Tc` \ ty' ->
402 returnNF_Tc (SynTy tc tys' ty')
404 zonkTcType (ForAllTy tv ty)
405 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
406 zonkTcType ty `thenNF_Tc` \ ty' ->
407 case tv_ty of -- Should be a tyvar!
409 returnNF_Tc (ForAllTy tv' ty')
410 _ -> --pprTrace "zonkTcType:ForAllTy:" (hsep [ppr PprDebug tv, ppr PprDebug tv_ty]) $
412 returnNF_Tc (ForAllTy tv{-(tcTyVarToTyVar tv)-} ty')
414 zonkTcType (ForAllUsageTy uv uvs ty)
415 = panic "zonk:ForAllUsageTy"
417 zonkTcType (FunTy ty1 ty2 u)
418 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
419 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
420 returnNF_Tc (FunTy ty1' ty2' u)
422 zonkTcType (DictTy c ty u)
423 = zonkTcType ty `thenNF_Tc` \ ty' ->
424 returnNF_Tc (DictTy c ty' u)