2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
4 \section[GenSpecEtc]{Code for GEN, SPEC, PRED, and REL}
7 #include "HsVersions.h"
18 import Inst ( Inst, InstOrigin(..), SYN_IE(LIE), plusLIE,
19 newDicts, tyVarsOfInst, instToId )
20 import TcEnv ( tcGetGlobalTyVars, tcExtendGlobalTyVars )
21 import SpecEnv ( SpecEnv )
22 import TcSimplify ( tcSimplify, tcSimplifyAndCheck )
23 import TcType ( SYN_IE(TcType), SYN_IE(TcThetaType), SYN_IE(TcTauType),
24 SYN_IE(TcTyVarSet), SYN_IE(TcTyVar),
25 newTyVarTy, zonkTcType, zonkTcTyVar, zonkTcTyVars
27 import Unify ( unifyTauTy )
29 import HsSyn ( HsBinds(..), Bind(..), MonoBinds(..), HsExpr, OutPat(..),
30 Sig, HsLit, ArithSeqInfo, InPat, GRHSsAndBinds, Match, Fake
32 import TcHsSyn ( TcIdOcc(..), SYN_IE(TcIdBndr), SYN_IE(TcHsBinds), SYN_IE(TcBind), SYN_IE(TcExpr), tcIdType )
34 import Bag ( Bag, foldBag, bagToList, listToBag, isEmptyBag )
35 import Class ( GenClass )
36 import Id ( GenId, SYN_IE(Id), mkUserId, idType )
37 import Kind ( isUnboxedTypeKind, isTypeKind, mkBoxedTypeKind )
38 import ListSetOps ( minusList, unionLists, intersectLists )
39 import Maybes ( allMaybes )
40 import Name ( Name{--O only-} )
41 import Outputable ( interppSP, interpp'SP )
43 import PprType ( GenClass, GenType, GenTyVar )
44 import Type ( mkTyVarTy, splitSigmaTy, mkForAllTys, mkFunTys,
45 getTyVar, getTyVar_maybe, tyVarsOfTypes, eqSimpleTheta )
46 import TyVar ( GenTyVar, SYN_IE(TyVar), tyVarKind, minusTyVarSet, emptyTyVarSet,
47 elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
48 import Usage ( SYN_IE(UVar) )
49 import Unique ( Unique )
53 %************************************************************************
55 \subsection[Gen-SignatureInfo]{The @TcSigInfo@ type}
57 %************************************************************************
59 A type signature (or user-pragma) is typechecked to produce a
60 @TcSigInfo@. It contains @TcTypes@ because they are unified with
61 the variable's type, and after that checked to see whether they've
66 = TySigInfo (TcIdBndr s) -- for this value...
67 [TcTyVar s] (TcThetaType s) (TcTauType s)
72 %************************************************************************
74 \subsection[Gen-GEN]{Generalising bindings}
76 %************************************************************************
79 genBinds :: [Name] -- Binders
80 -> [TcIdBndr s] -- Monomorphic binders
81 -> TcBind s -- Type-checked monobind
82 -> LIE s -- LIE from typecheck of binds
83 -> [TcSigInfo s] -- Signatures, if any
84 -> (Name -> PragmaInfo) -- Gives pragma info for binder
85 -> TcM s (TcHsBinds s, LIE s, [TcIdBndr s])
88 In the call $(@genBinds@~env~bind~lie~lve)$, $(bind,lie,lve)$
89 is the result of typechecking a @Bind@. @genBinds@ implements the BIND-GEN
91 $lie$ and $lve$ may or may not be
92 fixed points of the current substitution.
97 An @AbsBind@ which wraps up $bind$ in a suitable abstraction.
99 an LIE, which is the part of the input LIE which isn't discharged by
100 the AbsBind. This means the parts which predicate type variables
103 An LVE whose domain is identical to that passed in.
104 Its range is a new set of locals to that passed in,
105 because they have been gen'd.
112 find $constrained$, the free variables of $env$.
113 First we must apply the current substitution to the environment, so that the
114 correct set of constrained type vars are extracted!
116 find $free$, the free variables of $lve$ which are not in $constrained$.
117 We need to apply the current subsitution to $lve$ first, of course.
119 minimise $lie$ to give $lie'$; all the constraints in $lie'$ are on
120 single type variables.
122 split $lie'$ into three: those predicating type variables in $constrained$,
123 those on type variables in $free$, and the rest.
125 complain about ``the rest'' part of $lie'$. These type variables are
128 generate new locals for each member of the domain of $lve$, with appropriately
131 generate a suitable AbsBinds to enclose the bindings.
135 genBinds binder_names mono_ids bind lie sig_infos prag_info_fn
136 = -- CHECK THAT THE SIGNATURES MATCH
137 -- Doesn't affect substitution
138 mapTc checkSigMatch sig_infos `thenTc_`
140 -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE IDENTICAL
141 -- The type signatures on a mutually-recursive group of definitions
142 -- must all have the same context (or none).
143 -- We have to zonk them first to make their type variables line up
144 mapNF_Tc get_zonked_theta sig_infos `thenNF_Tc` \ thetas ->
145 checkTc (null thetas || all (eqSimpleTheta (head thetas)) (tail thetas))
146 (sigContextsErr sig_infos) `thenTc_`
148 -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
149 mapNF_Tc (zonkTcType . idType) mono_ids `thenNF_Tc` \ mono_id_types ->
150 tcGetGlobalTyVars `thenNF_Tc` \ free_tyvars ->
152 mentioned_tyvars = tyVarsOfTypes mono_id_types
153 tyvars_to_gen = mentioned_tyvars `minusTyVarSet` free_tyvars
154 tysig_vars = [sig_var | (TySigInfo sig_var _ _ _ _) <- sig_infos]
157 -- DEAL WITH OVERLOADING
158 resolveOverloading tyvars_to_gen lie bind tysig_vars (head thetas)
159 `thenTc` \ (lie', reduced_tyvars_to_gen, dict_binds, dicts_bound) ->
161 -- Check for generalisation over unboxed types, and
162 -- default any TypeKind TyVars to BoxedTypeKind
164 tyvars = tyVarSetToList reduced_tyvars_to_gen -- Commit to a particular order
166 unboxed_kind_tyvars = filter (isUnboxedTypeKind . tyVarKind) tyvars
167 unresolved_kind_tyvars = filter (isTypeKind . tyVarKind) tyvars
169 box_it tyvar = newTyVarTy mkBoxedTypeKind `thenNF_Tc` \ boxed_ty ->
170 unifyTauTy boxed_ty (mkTyVarTy tyvar)
173 ASSERT( null unboxed_kind_tyvars ) -- The instCantBeGeneralised stuff in tcSimplify
174 -- should have dealt with unboxed type variables;
175 -- and it's better done there because we have more
176 -- precise origin information
178 -- Default any TypeKind variables to BoxedTypeKind
179 mapTc box_it unresolved_kind_tyvars `thenTc_`
181 -- BUILD THE NEW LOCALS
183 dict_tys = map tcIdType dicts_bound
184 poly_tys = map (mkForAllTys tyvars . mkFunTys dict_tys) mono_id_types
185 poly_ids = zipWithEqual "genspecetc" mk_poly binder_names poly_tys
186 mk_poly name ty = mkUserId name ty (prag_info_fn name)
192 (zipEqual "genBinds" (map TcId mono_ids) (map TcId poly_ids))
199 get_zonked_theta (TySigInfo _ _ theta _ _)
200 = mapNF_Tc (\ (c,t) -> zonkTcType t `thenNF_Tc` \ t' -> returnNF_Tc (c,t')) theta
206 :: TcTyVarSet s -- Tyvars over which we are going to generalise
207 -> LIE s -- The LIE to deal with
208 -> TcBind s -- The binding group
209 -> [TcIdBndr s] -- Variables in type signatures
210 -> TcThetaType s -- *Zonked* theta for the overloading in type signature
211 -- (if there are any type signatures; error otherwise)
212 -> TcM s (LIE s, -- LIE to pass up the way; a fixed point of
213 -- the current substitution
214 TcTyVarSet s, -- Revised tyvars to generalise
215 [(TcIdOcc s, TcExpr s)], -- Dict bindings
216 [TcIdOcc s]) -- List of dicts to bind here
218 resolveOverloading tyvars_to_gen dicts bind tysig_vars theta
219 | not (isUnRestrictedGroup tysig_vars bind)
220 = -- Restricted group, so bind no dictionaries, and
221 -- remove from tyvars_to_gen any constrained type variables
223 -- *Don't* simplify dicts at this point, because we aren't going
224 -- to generalise over these dicts. By the time we do simplify them
225 -- we may well know more. For example (this actually came up)
226 -- f :: Array Int Int
227 -- f x = array ... xs where xs = [1,2,3,4,5]
228 -- We don't want to generate lots of (fromInt Int 1), (fromInt Int 2)
229 -- stuff. If we simplify only at the f-binding (not the xs-binding)
230 -- we'll know that the literals are all Ints, and we can just produce
233 -- Find all the type variables involved in overloading, the "constrained_tyvars"
234 -- These are the ones we *aren't* going to generalise.
235 -- We must be careful about doing this:
236 -- (a) If we fail to generalise a tyvar which is not actually
237 -- constrained, then it will never, ever get bound, and lands
238 -- up printed out in interface files! Notorious example:
239 -- instance Eq a => Eq (Foo a b) where ..
240 -- Here, b is not constrained, even though it looks as if it is.
241 -- Another, more common, example is when there's a Method inst in
242 -- the LIE, whose type might very well involve non-overloaded
244 -- (b) On the other hand, we mustn't generalise tyvars which are constrained,
245 -- because we are going to pass on out the unmodified LIE, with those
246 -- tyvars in it. They won't be in scope if we've generalised them.
248 -- So we are careful, and do a complete simplification just to find the
249 -- constrained tyvars. We don't use any of the results, except to
250 -- find which tyvars are constrained.
252 tcSimplify tyvars_to_gen dicts `thenTc` \ (_, _, dicts_sig) ->
254 -- ASSERT: dicts_sig is already zonked!
255 constrained_tyvars = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet dicts_sig
256 reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
259 -- Do it again, but with increased free_tyvars/reduced_tyvars_to_gen:
260 -- We still need to do this simplification, because some dictionaries
261 -- may gratuitouslyconstrain some tyvars over which we *are* going
263 -- For example d::Eq (Foo a b), where Foo is instanced as above.
264 tcExtendGlobalTyVars constrained_tyvars (
265 tcSimplify reduced_tyvars_to_gen dicts
267 `thenTc` \ (dicts_free, dicts_binds, dicts_sig2) ->
268 ASSERT(isEmptyBag dicts_sig2)
270 returnTc (dicts_free, -- All these are left unbound
271 reduced_tyvars_to_gen,
272 dicts_binds, -- Local dict binds
273 []) -- No lambda-bound dicts
275 -- The returned LIE should be a fixed point of the substitution
277 | null tysig_vars -- An unrestricted group with no type signaturs
278 = tcSimplify tyvars_to_gen dicts `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
279 returnTc (dicts_free, tyvars_to_gen, dict_binds,
280 map instToId (bagToList dicts_sig))
282 | otherwise -- An unrestricted group with type signatures
283 = tcAddErrCtxt (sigsCtxt tysig_vars) $
284 newDicts SignatureOrigin theta `thenNF_Tc` \ (dicts_sig, dict_ids) ->
285 -- It's important that theta is pre-zonked, because
286 -- dict_id is later used to form the type of the polymorphic thing,
287 -- and forall-types must be zonked so far as their bound variables
290 -- Check that the needed dicts can be expressed in
291 -- terms of the signature ones
293 tyvars_to_gen -- Type vars over which we will quantify
294 dicts_sig -- Available dicts
295 dicts -- Want bindings for these dicts
297 `thenTc` \ (dicts_free, dict_binds) ->
299 returnTc (dicts_free, tyvars_to_gen, dict_binds, dict_ids)
302 @checkSigMatch@ does the next step in checking signature matching.
303 The tau-type part has already been unified. What we do here is to
304 check that this unification has not over-constrained the (polymorphic)
305 type variables of the original signature type.
307 The error message here is somewhat unsatisfactory, but it'll do for
311 checkSigMatch :: TcSigInfo s -> TcM s ()
313 checkSigMatch (TySigInfo id sig_tyvars _ tau_ty src_loc)
314 = tcAddSrcLoc src_loc $
315 tcAddErrCtxt (sigCtxt id) $
316 checkSigTyVars sig_tyvars tau_ty
320 %************************************************************************
322 \subsection[GenEtc-monomorphism]{The monomorphism restriction}
324 %************************************************************************
329 isUnRestrictedGroup :: [TcIdBndr s] -- Signatures given for these
333 isUnRestrictedGroup sigs EmptyBind = True
334 isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
335 isUnRestrictedGroup sigs (RecBind monobinds) = isUnResMono sigs monobinds
337 is_elem v vs = isIn "isUnResMono" v vs
339 isUnResMono sigs (PatMonoBind (VarPat (TcId v)) _ _) = v `is_elem` sigs
340 isUnResMono sigs (PatMonoBind other _ _) = False
341 isUnResMono sigs (VarMonoBind (TcId v) _) = v `is_elem` sigs
342 isUnResMono sigs (FunMonoBind _ _ _ _) = True
343 isUnResMono sigs (AndMonoBinds mb1 mb2) = isUnResMono sigs mb1 &&
345 isUnResMono sigs EmptyMonoBinds = True
349 %************************************************************************
351 \subsection[GenEtc-sig]{Matching a type signature}
353 %************************************************************************
355 @checkSigTyVars@ is used after the type in a type signature has been unified with
356 the actual type found. It then checks that the type variables of the type signature
358 (a) still all type variables
359 eg matching signature [a] against inferred type [(p,q)]
360 [then a will be unified to a non-type variable]
362 (b) still all distinct
363 eg matching signature [(a,b)] against inferred type [(p,p)]
364 [then a and b will be unified together]
366 BUT ACTUALLY THESE FIRST TWO ARE FORCED BY USING DontBind TYVARS
368 (c) not mentioned in the environment
369 eg the signature for f in this:
375 Here, f is forced to be monorphic by the free occurence of x.
377 Before doing this, the substitution is applied to the signature type variable.
380 checkSigTyVars :: [TcTyVar s] -- The original signature type variables
381 -> TcType s -- signature type (for err msg)
384 checkSigTyVars sig_tyvars sig_tau
385 = tcGetGlobalTyVars `thenNF_Tc` \ globals ->
387 mono_tyvars = filter (`elementOfTyVarSet` globals) sig_tyvars
390 -- Until the final Bind-handling stuff is in, several type signatures in the same
391 -- bindings group can cause the signature type variable from the different
392 -- signatures to be unified. So we still need to zonk and check point (b).
393 -- Remove when activating the new binding code
394 mapNF_Tc zonkTcTyVar sig_tyvars `thenNF_Tc` \ sig_tys ->
395 checkTcM (hasNoDups (map (getTyVar "checkSigTyVars") sig_tys))
396 (zonkTcType sig_tau `thenNF_Tc` \ sig_tau' ->
397 failTc (badMatchErr sig_tau sig_tau')
402 -- We want to report errors in terms of the original signature tyvars,
403 -- ie sig_tyvars, NOT sig_tyvars'. sig_tys and sig_tyvars' correspond
404 -- 1-1 with sig_tyvars, so we can just map back.
405 checkTc (null mono_tyvars)
406 (notAsPolyAsSigErr sig_tau mono_tyvars)
415 notAsPolyAsSigErr sig_tau mono_tyvars sty
416 = ppHang (ppStr "A type signature is more polymorphic than the inferred type")
417 4 (ppAboves [ppStr "Some type variables in the inferred type can't be forall'd, namely:",
418 interpp'SP sty mono_tyvars,
419 ppStr "Possible cause: the RHS mentions something subject to the monomorphism restriction"
425 badMatchErr sig_ty inferred_ty sty
426 = ppHang (ppStr "Type signature doesn't match inferred type")
427 4 (ppAboves [ppHang (ppStr "Signature:") 4 (ppr sty sig_ty),
428 ppHang (ppStr "Inferred :") 4 (ppr sty inferred_ty)
432 = ppSep [ppStr "When checking signature for", ppr sty id]
434 = ppSep [ppStr "When checking signature(s) for:", interpp'SP sty ids]
439 sigContextsErr ty_sigs sty
440 = ppHang (ppStr "A group of type signatures have mismatched contexts")
441 4 (ppAboves (map ppr_sig_info ty_sigs))
443 ppr_sig_info (TySigInfo val tyvars theta tau_ty _)
444 = ppHang (ppBeside (ppr sty val) (ppStr " :: "))
447 else ppBesides [ppStr "(",
448 ppIntersperse (ppStr ", ") (map (ppr_inst sty) theta),
450 ppr_inst sty (clas, ty) = ppCat [ppr sty clas, ppr sty ty]