2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
4 \section[GenSpecEtc]{Code for GEN, SPEC, PRED, and REL}
7 #include "HsVersions.h"
12 checkSigTyVars, checkSigTyVarsGivenGlobals
18 import Inst ( Inst, InstOrigin(..), LIE(..), plusLIE,
19 newDicts, tyVarsOfInst, instToId )
20 import TcEnv ( tcGetGlobalTyVars )
21 import TcSimplify ( tcSimplify, tcSimplifyAndCheck, tcSimplifyWithExtraGlobals )
22 import TcType ( TcType(..), TcThetaType(..), TcTauType(..),
23 TcTyVarSet(..), TcTyVar(..), tcInstType, zonkTcType )
25 import HsSyn ( HsBinds(..), Bind(..), MonoBinds(..), HsExpr, OutPat(..),
26 Sig, HsLit, ArithSeqInfo, InPat, GRHSsAndBinds, Match, Fake
28 import TcHsSyn ( TcIdOcc(..), TcIdBndr(..), TcHsBinds(..), TcBind(..), TcExpr(..), tcIdType )
30 import Bag ( Bag, foldBag, bagToList, listToBag, isEmptyBag )
31 import Class ( GenClass )
32 import Id ( GenId, Id(..), mkUserId, idType )
33 import ListSetOps ( minusList, unionLists, intersectLists )
34 import Maybes ( Maybe(..), allMaybes )
35 import Outputable ( interppSP, interpp'SP )
37 import PprType ( GenClass, GenType, GenTyVar )
38 import Type ( mkTyVarTy, splitSigmaTy, mkForAllTys, mkFunTys,
39 getTyVar_maybe, tyVarsOfTypes, eqSimpleTheta )
40 import TyVar ( GenTyVar, TyVar(..), minusTyVarSet, emptyTyVarSet,
41 elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
42 import Usage ( UVar(..) )
43 import Unique ( Unique )
47 %************************************************************************
49 \subsection[Gen-SignatureInfo]{The @TcSigInfo@ type}
51 %************************************************************************
53 A type signature (or user-pragma) is typechecked to produce a
54 @TcSigInfo@. It contains @TcTypes@ because they are unified with
55 the variable's type, and after that checked to see whether they've
60 = TySigInfo (TcIdBndr s) -- for this value...
61 [TcTyVar s] (TcThetaType s) (TcTauType s)
66 %************************************************************************
68 \subsection[Gen-GEN]{Generalising bindings}
70 %************************************************************************
73 genBinds :: [Name] -- Binders
74 -> [TcIdBndr s] -- Monomorphic binders
75 -> TcBind s -- Type-checked monobind
76 -> LIE s -- LIE from typecheck of binds
77 -> [TcSigInfo s] -- Signatures, if any
78 -> (Name -> PragmaInfo) -- Gives pragma info for binder
79 -> TcM s (TcHsBinds s, LIE s, [TcIdBndr s])
82 In the call $(@genBinds@~env~bind~lie~lve)$, $(bind,lie,lve)$
83 is the result of typechecking a @Bind@. @genBinds@ implements the BIND-GEN
85 $lie$ and $lve$ may or may not be
86 fixed points of the current substitution.
91 An @AbsBind@ which wraps up $bind$ in a suitable abstraction.
93 an LIE, which is the part of the input LIE which isn't discharged by
94 the AbsBind. This means the parts which predicate type variables
97 An LVE whose domain is identical to that passed in.
98 Its range is a new set of locals to that passed in,
99 because they have been gen'd.
106 find $constrained$, the free variables of $env$.
107 First we must apply the current substitution to the environment, so that the
108 correct set of constrained type vars are extracted!
110 find $free$, the free variables of $lve$ which are not in $constrained$.
111 We need to apply the current subsitution to $lve$ first, of course.
113 minimise $lie$ to give $lie'$; all the constraints in $lie'$ are on
114 single type variables.
116 split $lie'$ into three: those predicating type variables in $constrained$,
117 those on type variables in $free$, and the rest.
119 complain about ``the rest'' part of $lie'$. These type variables are
122 generate new locals for each member of the domain of $lve$, with appropriately
125 generate a suitable AbsBinds to enclose the bindings.
129 genBinds binder_names mono_ids bind lie sig_infos prag_info_fn
130 = -- CHECK THAT THE SIGNATURES MATCH
131 -- Doesn't affect substitution
132 mapTc checkSigMatch sig_infos `thenTc_`
134 -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE IDENTICAL
135 -- The type signatures on a mutually-recursive group of definitions
136 -- must all have the same context (or none).
137 -- We have to zonk them first to make their type variables line up
138 mapNF_Tc get_zonked_theta sig_infos `thenNF_Tc` \ thetas ->
139 checkTc (null thetas || all (eqSimpleTheta (head thetas)) (tail thetas))
140 (sigContextsErr sig_infos) `thenTc_`
142 -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
143 mapNF_Tc (zonkTcType . idType) mono_ids `thenNF_Tc` \ mono_id_types ->
144 tcGetGlobalTyVars `thenNF_Tc` \ free_tyvars ->
146 mentioned_tyvars = tyVarsOfTypes mono_id_types
147 tyvars_to_gen = mentioned_tyvars `minusTyVarSet` free_tyvars
150 -- DEAL WITH OVERLOADING
151 resolveOverloading tyvars_to_gen lie bind sig_infos
152 `thenTc` \ (lie', reduced_tyvars_to_gen, dict_binds, dicts_bound) ->
154 -- BUILD THE NEW LOCALS
156 tyvars = tyVarSetToList reduced_tyvars_to_gen -- Commit to a particular order
157 dict_tys = map tcIdType dicts_bound
158 poly_tys = map (mkForAllTys tyvars . mkFunTys dict_tys) mono_id_types
159 poly_ids = zipWithEqual mk_poly binder_names poly_tys
160 mk_poly name ty = mkUserId name ty (prag_info_fn name)
166 (map TcId mono_ids `zip` map TcId poly_ids)
173 get_zonked_theta (TySigInfo _ _ theta _ _)
174 = mapNF_Tc (\ (c,t) -> zonkTcType t `thenNF_Tc` \ t' -> returnNF_Tc (c,t')) theta
180 :: TcTyVarSet s -- Tyvars over which we are going to generalise
181 -> LIE s -- The LIE to deal with
182 -> TcBind s -- The binding group
183 -> [TcSigInfo s] -- And its real type-signature information
184 -> TcM s (LIE s, -- LIE to pass up the way; a fixed point of
185 -- the current substitution
186 TcTyVarSet s, -- Revised tyvars to generalise
187 [(TcIdOcc s, TcExpr s)], -- Dict bindings
188 [TcIdOcc s]) -- List of dicts to bind here
190 resolveOverloading tyvars_to_gen dicts bind ty_sigs
191 | not (isUnRestrictedGroup tysig_vars bind)
192 = -- Restricted group, so bind no dictionaries, and
193 -- remove from tyvars_to_gen any constrained type variables
195 -- *Don't* simplify dicts at this point, because we aren't going
196 -- to generalise over these dicts. By the time we do simplify them
197 -- we may well know more. For example (this actually came up)
198 -- f :: Array Int Int
199 -- f x = array ... xs where xs = [1,2,3,4,5]
200 -- We don't want to generate lots of (fromInt Int 1), (fromInt Int 2)
201 -- stuff. If we simplify only at the f-binding (not the xs-binding)
202 -- we'll know that the literals are all Ints, and we can just produce
205 -- Find all the type variables involved in overloading, the "constrained_tyvars"
206 -- These are the ones we *aren't* going to generalise.
207 -- We must be careful about doing this:
208 -- (a) If we fail to generalise a tyvar which is not actually
209 -- constrained, then it will never, ever get bound, and lands
210 -- up printed out in interface files! Notorious example:
211 -- instance Eq a => Eq (Foo a b) where ..
212 -- Here, b is not constrained, even though it looks as if it is.
213 -- Another, more common, example is when there's a Method inst in
214 -- the LIE, whose type might very well involve non-overloaded
216 -- (b) On the other hand, we mustn't generalise tyvars which are constrained,
217 -- because we are going to pass on out the unmodified LIE, with those
218 -- tyvars in it. They won't be in scope if we've generalised them.
220 -- So we are careful, and do a complete simplification just to find the
221 -- constrained tyvars. We don't use any of the results, except to
222 -- find which tyvars are constrained.
224 tcSimplify tyvars_to_gen dicts `thenTc` \ (_, _, dicts_sig) ->
226 -- ASSERT: dicts_sig is already zonked!
227 constrained_tyvars = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet dicts_sig
228 reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
231 -- Do it again, but with increased free_tyvars/reduced_tyvars_to_gen:
232 -- We still need to do this simplification, because some dictionaries
233 -- may gratuitouslyconstrain some tyvars over which we *are* going
235 -- For example d::Eq (Foo a b), where Foo is instanced as above.
236 tcSimplifyWithExtraGlobals constrained_tyvars reduced_tyvars_to_gen dicts
237 `thenTc` \ (dicts_free, dicts_binds, dicts_sig2) ->
238 ASSERT(isEmptyBag dicts_sig2)
240 returnTc (dicts_free, -- All these are left unbound
241 reduced_tyvars_to_gen,
242 dicts_binds, -- Local dict binds
243 []) -- No lambda-bound dicts
245 -- The returned LIE should be a fixed point of the substitution
247 | otherwise -- An unrestricted group
249 [] -> -- NO TYPE SIGNATURES
251 tcSimplify tyvars_to_gen dicts `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
252 returnTc (dicts_free, tyvars_to_gen, dict_binds,
253 map instToId (bagToList dicts_sig))
255 (TySigInfo _ _ theta _ _ : other) -> -- TYPE SIGNATURES PRESENT!
257 tcAddErrCtxt (sigsCtxt tysig_vars) $
259 newDicts SignatureOrigin theta `thenNF_Tc` \ (dicts_sig, dict_ids) ->
261 -- Check that the needed dicts can be expressed in
262 -- terms of the signature ones
264 tyvars_to_gen -- Type vars over which we will quantify
265 dicts_sig -- Available dicts
266 dicts -- Want bindings for these dicts
268 `thenTc` \ (dicts_free, dict_binds) ->
270 returnTc (dicts_free, tyvars_to_gen, dict_binds, dict_ids)
272 tysig_vars = [sig_var | (TySigInfo sig_var _ _ _ _) <- ty_sigs]
275 @checkSigMatch@ does the next step in checking signature matching.
276 The tau-type part has already been unified. What we do here is to
277 check that this unification has not over-constrained the (polymorphic)
278 type variables of the original signature type.
280 The error message here is somewhat unsatisfactory, but it'll do for
284 checkSigMatch :: TcSigInfo s -> TcM s ()
286 checkSigMatch (TySigInfo id sig_tyvars _ tau_ty src_loc)
287 = tcAddSrcLoc src_loc $
288 tcAddErrCtxt (sigCtxt id) $
289 checkSigTyVars sig_tyvars tau_ty
293 %************************************************************************
295 \subsection[GenEtc-monomorphism]{The monomorphism restriction}
297 %************************************************************************
302 isUnRestrictedGroup :: [TcIdBndr s] -- Signatures given for these
306 isUnRestrictedGroup sigs EmptyBind = True
307 isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
308 isUnRestrictedGroup sigs (RecBind monobinds) = isUnResMono sigs monobinds
310 is_elem v vs = isIn "isUnResMono" v vs
312 isUnResMono sigs (PatMonoBind (VarPat (TcId v)) _ _) = v `is_elem` sigs
313 isUnResMono sigs (PatMonoBind other _ _) = False
314 isUnResMono sigs (VarMonoBind (TcId v) _) = v `is_elem` sigs
315 isUnResMono sigs (FunMonoBind _ _ _ _) = True
316 isUnResMono sigs (AndMonoBinds mb1 mb2) = isUnResMono sigs mb1 &&
318 isUnResMono sigs EmptyMonoBinds = True
322 %************************************************************************
324 \subsection[GenEtc-sig]{Matching a type signature}
326 %************************************************************************
328 @checkSigTyVars@ is used after the type in a type signature has been unified with
329 the actual type found. It then checks that the type variables of the type signature
331 (a) still all type variables
332 eg matching signature [a] against inferred type [(p,q)]
333 [then a will be unified to a non-type variable]
335 (b) still all distinct
336 eg matching signature [(a,b)] against inferred type [(p,p)]
337 [then a and b will be unified together]
339 BUT ACTUALLY THESE FIRST TWO ARE FORCED BY USING DontBind TYVARS
341 (c) not mentioned in the environment
342 eg the signature for f in this:
348 Here, f is forced to be monorphic by the free occurence of x.
350 Before doing this, the substitution is applied to the signature type variable.
353 checkSigTyVars :: [TcTyVar s] -- The original signature type variables
354 -> TcType s -- signature type (for err msg)
357 checkSigTyVars sig_tyvars sig_tau
358 = tcGetGlobalTyVars `thenNF_Tc` \ env_tyvars ->
359 checkSigTyVarsGivenGlobals env_tyvars sig_tyvars sig_tau
361 checkSigTyVarsGivenGlobals
362 :: TcTyVarSet s -- Consider these fully-zonked tyvars as global
363 -> [TcTyVar s] -- The original signature type variables
364 -> TcType s -- signature type (for err msg)
367 checkSigTyVarsGivenGlobals globals sig_tyvars sig_tau
369 -- We want to report errors in terms of the original signature tyvars,
370 -- ie sig_tyvars, NOT sig_tyvars'. sig_tys and sig_tyvars' correspond
371 -- 1-1 with sig_tyvars, so we can just map back.
372 checkTc (null mono_tyvars)
373 (notAsPolyAsSigErr sig_tau mono_tyvars)
375 mono_tyvars = filter (`elementOfTyVarSet` globals) sig_tyvars
384 notAsPolyAsSigErr sig_tau mono_tyvars sty
385 = ppHang (ppStr "A type signature is more polymorphic than the inferred type")
386 4 (ppAboves [ppStr "(That is, one or more type variables in the inferred type can't be forall'd.)",
387 ppHang (ppStr "Monomorphic type variable(s):")
388 4 (interpp'SP sty mono_tyvars),
389 ppStr "Possible cause: the RHS mentions something subject to the monomorphism restriction"
395 badMatchErr sig_ty inferred_ty sty
396 = ppHang (ppStr "Type signature doesn't match inferred type")
397 4 (ppAboves [ppHang (ppStr "Signature:") 4 (ppr sty sig_ty),
398 ppHang (ppStr "Inferred :") 4 (ppr sty inferred_ty)
402 = ppSep [ppStr "When checking signature for", ppr sty id]
404 = ppSep [ppStr "When checking signature(s) for:", interpp'SP sty ids]
409 sigContextsErr ty_sigs sty
410 = ppHang (ppStr "A group of type signatures have mismatched contexts")
411 4 (ppAboves (map ppr_sig_info ty_sigs))
413 ppr_sig_info (TySigInfo val tyvars theta tau_ty _)
414 = ppHang (ppBeside (ppr sty val) (ppStr " :: "))
417 else ppBesides [ppStr "(",
418 ppIntersperse (ppStr ", ") (map (ppr_inst sty) theta),
420 ppr_inst sty (clas, ty) = ppCat [ppr sty clas, ppr sty ty]