6 newTyVarTy, -- Kind -> NF_TcM s (TcType s)
7 newTyVarTys, -- Int -> Kind -> NF_TcM s [TcType s]
12 -----------------------------------------
13 TcType(..), TcMaybe(..),
14 TcTauType(..), TcThetaType(..), TcRhoType(..),
16 -- Find the type to which a type variable is bound
17 tcWriteTyVar, -- :: TcTyVar s -> TcType s -> NF_TcM (TcType s)
18 tcReadTyVar, -- :: TcTyVar s -> NF_TcM (TcMaybe s)
21 tcInstTyVars, -- TyVar -> NF_TcM s (TcTyVar s)
23 tcInstType, tcInstTcType, tcInstTheta, tcInstId,
25 zonkTcTyVars, -- TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
26 zonkTcType, -- TcType s -> NF_TcM s (TcType s)
27 zonkTcTypeToType, -- TcType s -> NF_TcM s Type
28 zonkTcTyVarToTyVar -- TcTyVar s -> NF_TcM s TyVar
35 import Type ( Type(..), ThetaType(..), GenType(..),
36 tyVarsOfTypes, getTyVar_maybe,
37 splitForAllTy, splitRhoTy
39 import TyVar ( TyVar(..), GenTyVar(..), TyVarSet(..), GenTyVarSet(..),
44 import Class ( GenClass )
47 import TcKind ( TcKind )
48 import TcMonad hiding ( rnMtoTcM )
49 import Usage ( Usage(..), GenUsage, UVar(..), duffUsage )
52 import Unique ( Unique )
53 import UniqFM ( UniqFM )
54 import Maybes ( assocMaybe )
55 import Util ( panic, pprPanic )
57 import Outputable ( Outputable(..) ) -- Debugging messages
58 import PprType ( GenTyVar, GenType )
59 import Pretty -- ditto
60 import PprStyle ( PprStyle(..) ) -- ditto
69 type TcType s = GenType (TcTyVar s) UVar -- Used during typechecker
70 -- Invariant on ForAllTy in TcTypes:
72 -- a cannot occur inside a MutTyVar in T; that is,
73 -- T is "flattened" before quantifying over a
75 type TcThetaType s = [(Class, TcType s)]
76 type TcRhoType s = TcType s -- No ForAllTys
77 type TcTauType s = TcType s -- No DictTys or ForAllTys
79 type Box s = MutableVar s (TcMaybe s)
81 data TcMaybe s = UnBound
83 | DontBind -- This variant is used for tyvars
84 -- arising from type signatures, or
85 -- existentially quantified tyvars;
86 -- The idea is that we must not unify
87 -- such tyvars with anything except
90 -- Interestingly, you can't use (Maybe (TcType s)) instead of (TcMaybe s),
91 -- because you get a synonym loop if you do!
93 type TcTyVar s = GenTyVar (Box s)
94 type TcTyVarSet s = GenTyVarSet (Box s)
98 tcTyVarToTyVar :: TcTyVar s -> TyVar
99 tcTyVarToTyVar (TyVar uniq kind name _) = TyVar uniq kind name duffUsage
106 newTcTyVar :: Kind -> NF_TcM s (TcTyVar s)
108 = tcGetUnique `thenNF_Tc` \ uniq ->
109 tcNewMutVar UnBound `thenNF_Tc` \ box ->
110 returnNF_Tc (TyVar uniq kind Nothing box)
112 newTyVarTy :: Kind -> NF_TcM s (TcType s)
114 = newTcTyVar kind `thenNF_Tc` \ tc_tyvar ->
115 returnNF_Tc (TyVarTy tc_tyvar)
117 newTyVarTys :: Int -> Kind -> NF_TcM s [TcType s]
118 newTyVarTys n kind = mapNF_Tc newTyVarTy (take n (repeat kind))
122 -- For signature type variables, mark them as "DontBind"
123 tcInstTyVars, tcInstSigTyVars
125 -> NF_TcM s ([TcTyVar s], [TcType s], [(GenTyVar flexi, TcType s)])
126 tcInstTyVars tyvars = inst_tyvars UnBound tyvars
127 tcInstSigTyVars tyvars = inst_tyvars DontBind tyvars
130 inst_tyvars initial_cts tyvars
131 = mapNF_Tc (inst_tyvar initial_cts) tyvars `thenNF_Tc` \ tc_tyvars ->
133 tys = map TyVarTy tc_tyvars
135 returnNF_Tc (tc_tyvars, tys, tyvars `zip` tys)
137 inst_tyvar initial_cts (TyVar _ kind name _)
138 = tcGetUnique `thenNF_Tc` \ uniq ->
139 tcNewMutVar initial_cts `thenNF_Tc` \ box ->
140 returnNF_Tc (TyVar uniq kind name box)
143 @tcInstType@ and @tcInstTcType@ both create a fresh instance of a
144 type, returning a @TcType@. All inner for-alls are instantiated with
147 There are two versions, one for instantiating a @Type@, and one for a @TcType@.
148 The former must instantiate everything; all tyvars must be bound either
149 by a forall or by an environment passed in. The latter can do some sharing,
150 and is happy with free tyvars (which is vital when instantiating the type
151 of local functions). In the future @tcInstType@ may try to be clever about not
152 instantiating constant sub-parts.
155 tcInstType :: [(TyVar,TcType s)] -> Type -> NF_TcM s (TcType s)
156 tcInstType tenv ty_to_inst
157 = do [(uniq,ty) | (TyVar uniq _ _ _, ty) <- tenv] ty_to_inst
159 do env (TyConTy tycon usage) = returnNF_Tc (TyConTy tycon usage)
161 do env (SynTy tycon tys ty) = mapNF_Tc (do env) tys `thenNF_Tc` \ tys' ->
162 do env ty `thenNF_Tc` \ ty' ->
163 returnNF_Tc (SynTy tycon tys' ty')
165 do env (FunTy arg res usage) = do env arg `thenNF_Tc` \ arg' ->
166 do env res `thenNF_Tc` \ res' ->
167 returnNF_Tc (FunTy arg' res' usage)
169 do env (AppTy fun arg) = do env fun `thenNF_Tc` \ fun' ->
170 do env arg `thenNF_Tc` \ arg' ->
171 returnNF_Tc (AppTy fun' arg')
173 do env (DictTy clas ty usage)= do env ty `thenNF_Tc` \ ty' ->
174 returnNF_Tc (DictTy clas ty' usage)
176 do env (TyVarTy tv@(TyVar uniq kind name _))
177 = case assocMaybe env uniq of
178 Just tc_ty -> returnNF_Tc tc_ty
179 Nothing -> pprPanic "tcInstType:" (ppAboves [ppr PprDebug tenv,
180 ppr PprDebug ty_to_inst, ppr PprDebug tv])
182 do env (ForAllTy tyvar@(TyVar uniq kind name _) ty)
183 = inst_tyvar DontBind tyvar `thenNF_Tc` \ tc_tyvar ->
185 new_env = (uniq, TyVarTy tc_tyvar) : env
187 do new_env ty `thenNF_Tc` \ ty' ->
188 returnNF_Tc (ForAllTy tc_tyvar ty')
190 -- ForAllUsage impossible
193 tcInstTheta :: [(TyVar,TcType s)] -> ThetaType -> NF_TcM s (TcThetaType s)
194 tcInstTheta tenv theta
197 go (clas,ty) = tcInstType tenv ty `thenNF_Tc` \ tc_ty ->
198 returnNF_Tc (clas, tc_ty)
200 -- A useful function that takes an occurrence of a global thing
201 -- and instantiates its type with fresh type variables
203 -> NF_TcM s ([TcTyVar s], -- It's instantiated type
209 (tyvars, rho) = splitForAllTy (idType id)
211 tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', arg_tys, tenv) ->
212 tcInstType tenv rho `thenNF_Tc` \ rho' ->
214 (theta', tau') = splitRhoTy rho'
216 returnNF_Tc (tyvars', theta', tau')
219 tcInstTcType :: [(TcTyVar s,TcType s)] -> TcType s -> NF_TcM s (TcType s)
220 tcInstTcType tenv ty_to_inst
221 = do [(uniq,ty) | (TyVar uniq _ _ _, ty) <- tenv] ty_to_inst
223 do env ty@(TyConTy tycon usage) = returnNF_Tc ty
225 -- Could do clever stuff here to avoid instantiating constant types
226 do env (SynTy tycon tys ty) = mapNF_Tc (do env) tys `thenNF_Tc` \ tys' ->
227 do env ty `thenNF_Tc` \ ty' ->
228 returnNF_Tc (SynTy tycon tys' ty')
230 do env (FunTy arg res usage) = do env arg `thenNF_Tc` \ arg' ->
231 do env res `thenNF_Tc` \ res' ->
232 returnNF_Tc (FunTy arg' res' usage)
234 do env (AppTy fun arg) = do env fun `thenNF_Tc` \ fun' ->
235 do env arg `thenNF_Tc` \ arg' ->
236 returnNF_Tc (AppTy fun' arg')
238 do env (DictTy clas ty usage)= do env ty `thenNF_Tc` \ ty' ->
239 returnNF_Tc (DictTy clas ty' usage)
241 do env ty@(TyVarTy (TyVar uniq kind name _))
242 = case assocMaybe env uniq of
243 Just tc_ty -> returnNF_Tc tc_ty
244 Nothing -> returnNF_Tc ty
246 do env (ForAllTy (TyVar uniq kind name _) ty) = panic "tcInstTcType"
248 -- ForAllUsage impossible
252 Reading and writing TcTyVars
253 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
255 tcWriteTyVar :: TcTyVar s -> TcType s -> NF_TcM s ()
256 tcReadTyVar :: TcTyVar s -> NF_TcM s (TcMaybe s)
262 tcWriteTyVar (TyVar uniq kind name box) ty = tcWriteMutVar box (BoundTo ty)
265 Reading is more interesting. The easy thing to do is just to read, thus:
267 tcReadTyVar (TyVar uniq kind name box) = tcReadMutVar box
270 But it's more fun to short out indirections on the way: If this
271 version returns a TyVar, then that TyVar is unbound. If it returns
272 any other type, then there might be bound TyVars embedded inside it.
274 We return Nothing iff the original box was unbound.
277 tcReadTyVar (TyVar uniq kind name box)
278 = tcReadMutVar box `thenNF_Tc` \ maybe_ty ->
280 BoundTo ty -> short_out ty `thenNF_Tc` \ ty' ->
281 tcWriteMutVar box (BoundTo ty') `thenNF_Tc_`
282 returnNF_Tc (BoundTo ty')
284 other -> returnNF_Tc other
286 short_out :: TcType s -> NF_TcM s (TcType s)
287 short_out ty@(TyVarTy (TyVar uniq kind name box))
288 = tcReadMutVar box `thenNF_Tc` \ maybe_ty ->
290 BoundTo ty' -> short_out ty' `thenNF_Tc` \ ty' ->
291 tcWriteMutVar box (BoundTo ty') `thenNF_Tc_`
294 other -> returnNF_Tc ty
296 short_out other_ty = returnNF_Tc other_ty
302 @zonkTcTypeToType@ converts from @TcType@ to @Type@. It follows through all
303 the substitutions of course.
306 zonkTcTypeToType :: TcType s -> NF_TcM s Type
307 zonkTcTypeToType ty = zonk tcTyVarToTyVar ty
309 zonkTcType :: TcType s -> NF_TcM s (TcType s)
310 zonkTcType ty = zonk (\tyvar -> tyvar) ty
312 zonkTcTyVars :: TcTyVarSet s -> NF_TcM s (TcTyVarSet s)
314 = mapNF_Tc (zonk_tv (\tyvar -> tyvar))
315 (tyVarSetToList tyvars) `thenNF_Tc` \ tys ->
316 returnNF_Tc (tyVarsOfTypes tys)
318 zonkTcTyVarToTyVar :: TcTyVar s -> NF_TcM s TyVar
319 zonkTcTyVarToTyVar tyvar
320 = zonk_tv_to_tv tcTyVarToTyVar tyvar
323 zonk tyvar_fn (TyVarTy tyvar)
324 = zonk_tv tyvar_fn tyvar
326 zonk tyvar_fn (AppTy ty1 ty2)
327 = zonk tyvar_fn ty1 `thenNF_Tc` \ ty1' ->
328 zonk tyvar_fn ty2 `thenNF_Tc` \ ty2' ->
329 returnNF_Tc (AppTy ty1' ty2')
331 zonk tyvar_fn (TyConTy tc u)
332 = returnNF_Tc (TyConTy tc u)
334 zonk tyvar_fn (SynTy tc tys ty)
335 = mapNF_Tc (zonk tyvar_fn) tys `thenNF_Tc` \ tys' ->
336 zonk tyvar_fn ty `thenNF_Tc` \ ty' ->
337 returnNF_Tc (SynTy tc tys' ty')
339 zonk tyvar_fn (ForAllTy tv ty)
340 = zonk_tv_to_tv tyvar_fn tv `thenNF_Tc` \ tv' ->
341 zonk tyvar_fn ty `thenNF_Tc` \ ty' ->
342 returnNF_Tc (ForAllTy tv' ty')
344 zonk tyvar_fn (ForAllUsageTy uv uvs ty)
345 = panic "zonk:ForAllUsageTy"
347 zonk tyvar_fn (FunTy ty1 ty2 u)
348 = zonk tyvar_fn ty1 `thenNF_Tc` \ ty1' ->
349 zonk tyvar_fn ty2 `thenNF_Tc` \ ty2' ->
350 returnNF_Tc (FunTy ty1' ty2' u)
352 zonk tyvar_fn (DictTy c ty u)
353 = zonk tyvar_fn ty `thenNF_Tc` \ ty' ->
354 returnNF_Tc (DictTy c ty' u)
357 zonk_tv tyvar_fn tyvar
358 = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty ->
360 BoundTo ty -> zonk tyvar_fn ty
361 other -> returnNF_Tc (TyVarTy (tyvar_fn tyvar))
364 zonk_tv_to_tv tyvar_fn tyvar
365 = zonk_tv tyvar_fn tyvar `thenNF_Tc` \ ty ->
366 case getTyVar_maybe ty of
367 Nothing -> panic "zonk_tv_to_tv"
368 Just tyvar -> returnNF_Tc tyvar