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,
19 import Inst ( Inst, InstOrigin(..), LIE(..), plusLIE,
20 newDicts, tyVarsOfInst, instToId )
21 import TcEnv ( tcGetGlobalTyVars )
22 import TcSimplify ( tcSimplify, tcSimplifyAndCheck, tcSimplifyWithExtraGlobals )
23 import TcType ( TcType(..), TcThetaType(..), TcTauType(..),
24 TcTyVarSet(..), TcTyVar(..), tcInstType, zonkTcType )
26 import HsSyn ( HsBinds(..), Bind(..), MonoBinds(..), HsExpr, OutPat(..),
27 Sig, HsLit, ArithSeqInfo, InPat, GRHSsAndBinds, Match, Fake
29 import TcHsSyn ( TcIdOcc(..), TcIdBndr(..), TcHsBinds(..), TcBind(..), TcExpr(..) )
31 import Bag ( Bag, foldBag, bagToList, listToBag, isEmptyBag )
32 import Class ( GenClass )
33 import Id ( GenId, Id(..), mkUserId, idType )
34 import ListSetOps ( minusList, unionLists, intersectLists )
35 import Maybes ( Maybe(..), allMaybes )
36 import Outputable ( interppSP, interpp'SP )
38 import PprType ( GenClass, GenType, GenTyVar )
39 import Type ( mkTyVarTy, splitSigmaTy, mkForAllTys, mkFunTys,
40 getTyVar_maybe, tyVarsOfTypes, eqSimpleTheta )
41 import TyVar ( GenTyVar, TyVar(..), minusTyVarSet, emptyTyVarSet,
42 elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
43 import Usage ( UVar(..) )
44 import Unique ( Unique )
48 %************************************************************************
50 \subsection[Gen-SignatureInfo]{The @TcSigInfo@ type}
52 %************************************************************************
54 A type signature (or user-pragma) is typechecked to produce a
55 @TcSigInfo@. It contains @TcTypes@ because they are unified with
56 the variable's type, and after that checked to see whether they've
61 = TySigInfo (TcIdBndr s) -- for this value...
62 [TcTyVar s] (TcThetaType s) (TcTauType s)
67 %************************************************************************
69 \subsection[Gen-GEN]{Generalising bindings}
71 %************************************************************************
74 genBinds :: [Name] -- Binders
75 -> [TcIdBndr s] -- Monomorphic binders
76 -> TcBind s -- Type-checked monobind
77 -> LIE s -- LIE from typecheck of binds
78 -> [TcSigInfo s] -- Signatures, if any
79 -> (Name -> PragmaInfo) -- Gives pragma info for binder
80 -> TcM s (TcHsBinds s, LIE s, [TcIdBndr s])
83 In the call $(@genBinds@~env~bind~lie~lve)$, $(bind,lie,lve)$
84 is the result of typechecking a @Bind@. @genBinds@ implements the BIND-GEN
86 $lie$ and $lve$ may or may not be
87 fixed points of the current substitution.
92 An @AbsBind@ which wraps up $bind$ in a suitable abstraction.
94 an LIE, which is the part of the input LIE which isn't discharged by
95 the AbsBind. This means the parts which predicate type variables
98 An LVE whose domain is identical to that passed in.
99 Its range is a new set of locals to that passed in,
100 because they have been gen'd.
107 find $constrained$, the free variables of $env$.
108 First we must apply the current substitution to the environment, so that the
109 correct set of constrained type vars are extracted!
111 find $free$, the free variables of $lve$ which are not in $constrained$.
112 We need to apply the current subsitution to $lve$ first, of course.
114 minimise $lie$ to give $lie'$; all the constraints in $lie'$ are on
115 single type variables.
117 split $lie'$ into three: those predicating type variables in $constrained$,
118 those on type variables in $free$, and the rest.
120 complain about ``the rest'' part of $lie'$. These type variables are
123 generate new locals for each member of the domain of $lve$, with appropriately
126 generate a suitable AbsBinds to enclose the bindings.
130 genBinds binder_names mono_ids bind lie sig_infos prag_info_fn
131 = -- CHECK THAT THE SIGNATURES MATCH
132 -- Doesn't affect substitution
133 mapTc checkSigMatch sig_infos `thenTc_`
135 -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE IDENTICAL
136 -- The type signatures on a mutually-recursive group of definitions
137 -- must all have the same context (or none).
138 -- We have to zonk them first to make their type variables line up
139 mapNF_Tc get_zonked_theta sig_infos `thenNF_Tc` \ thetas ->
140 checkTc (null thetas || all (eqSimpleTheta (head thetas)) (tail thetas))
141 (sigContextsErr sig_infos) `thenTc_`
143 -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
144 mapNF_Tc (zonkTcType . idType) mono_ids `thenNF_Tc` \ mono_id_types ->
145 tcGetGlobalTyVars `thenNF_Tc` \ free_tyvars ->
147 mentioned_tyvars = tyVarsOfTypes mono_id_types
148 tyvars_to_gen = mentioned_tyvars `minusTyVarSet` free_tyvars
151 -- DEAL WITH OVERLOADING
152 resolveOverloading tyvars_to_gen lie bind sig_infos
153 `thenTc` \ (lie', reduced_tyvars_to_gen, dict_binds, dicts_bound) ->
155 -- BUILD THE NEW LOCALS
157 tyvars = tyVarSetToList reduced_tyvars_to_gen -- Commit to a particular order
158 dict_tys = [idType d | TcId d <- dicts_bound] -- Slightly ugh-ish
159 poly_tys = map (mkForAllTys tyvars . mkFunTys dict_tys) mono_id_types
160 poly_ids = zipWithEqual mk_poly binder_names poly_tys
161 mk_poly name ty = mkUserId name ty (prag_info_fn name)
167 (map TcId mono_ids `zip` map TcId poly_ids)
174 get_zonked_theta (TySigInfo _ _ theta _ _)
175 = mapNF_Tc (\ (c,t) -> zonkTcType t `thenNF_Tc` \ t' -> returnNF_Tc (c,t')) theta
181 :: TcTyVarSet s -- Tyvars over which we are going to generalise
182 -> LIE s -- The LIE to deal with
183 -> TcBind s -- The binding group
184 -> [TcSigInfo s] -- And its real type-signature information
185 -> TcM s (LIE s, -- LIE to pass up the way; a fixed point of
186 -- the current substitution
187 TcTyVarSet s, -- Revised tyvars to generalise
188 [(TcIdOcc s, TcExpr s)], -- Dict bindings
189 [TcIdOcc s]) -- List of dicts to bind here
191 resolveOverloading tyvars_to_gen dicts bind ty_sigs
192 | not (isUnRestrictedGroup tysig_vars bind)
193 = -- Restricted group, so bind no dictionaries, and
194 -- remove from tyvars_to_gen any constrained type variables
196 -- *Don't* simplify dicts at this point, because we aren't going
197 -- to generalise over these dicts. By the time we do simplify them
198 -- we may well know more. For example (this actually came up)
199 -- f :: Array Int Int
200 -- f x = array ... xs where xs = [1,2,3,4,5]
201 -- We don't want to generate lots of (fromInt Int 1), (fromInt Int 2)
202 -- stuff. If we simplify only at the f-binding (not the xs-binding)
203 -- we'll know that the literals are all Ints, and we can just produce
206 -- Find all the type variables involved in overloading, the "constrained_tyvars"
207 -- These are the ones we *aren't* going to generalise.
208 -- We must be careful about doing this:
209 -- (a) If we fail to generalise a tyvar which is not actually
210 -- constrained, then it will never, ever get bound, and lands
211 -- up printed out in interface files! Notorious example:
212 -- instance Eq a => Eq (Foo a b) where ..
213 -- Here, b is not constrained, even though it looks as if it is.
214 -- Another, more common, example is when there's a Method inst in
215 -- the LIE, whose type might very well involve non-overloaded
217 -- (b) On the other hand, we mustn't generalise tyvars which are constrained,
218 -- because we are going to pass on out the unmodified LIE, with those
219 -- tyvars in it. They won't be in scope if we've generalised them.
221 -- So we are careful, and do a complete simplification just to find the
222 -- constrained tyvars. We don't use any of the results, except to
223 -- find which tyvars are constrained.
225 tcSimplify tyvars_to_gen dicts `thenTc` \ (_, _, dicts_sig) ->
227 -- ASSERT: dicts_sig is already zonked!
228 constrained_tyvars = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet dicts_sig
229 reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
232 -- Do it again, but with increased free_tyvars/reduced_tyvars_to_gen:
233 -- We still need to do this simplification, because some dictionaries
234 -- may gratuitouslyconstrain some tyvars over which we *are* going
236 -- For example d::Eq (Foo a b), where Foo is instanced as above.
237 tcSimplifyWithExtraGlobals constrained_tyvars reduced_tyvars_to_gen dicts
238 `thenTc` \ (dicts_free, dicts_binds, dicts_sig2) ->
239 ASSERT(isEmptyBag dicts_sig2)
241 returnTc (dicts_free, -- All these are left unbound
242 reduced_tyvars_to_gen,
243 dicts_binds, -- Local dict binds
244 []) -- No lambda-bound dicts
246 -- The returned LIE should be a fixed point of the substitution
248 | otherwise -- An unrestricted group
250 [] -> -- NO TYPE SIGNATURES
252 tcSimplify tyvars_to_gen dicts `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
253 returnTc (dicts_free, tyvars_to_gen, dict_binds,
254 map instToId (bagToList dicts_sig))
256 (TySigInfo _ _ theta _ _ : other) -> -- TYPE SIGNATURES PRESENT!
258 tcAddErrCtxt (sigsCtxt tysig_vars) $
260 newDicts SignatureOrigin theta `thenNF_Tc` \ (dicts_sig, dict_ids) ->
262 -- Check that the needed dicts can be expressed in
263 -- terms of the signature ones
265 tyvars_to_gen -- Type vars over which we will quantify
266 dicts_sig -- Available dicts
267 dicts -- Want bindings for these dicts
269 `thenTc` \ (dicts_free, dict_binds) ->
271 returnTc (dicts_free, tyvars_to_gen, dict_binds, dict_ids)
273 tysig_vars = [sig_var | (TySigInfo sig_var _ _ _ _) <- ty_sigs]
276 @checkSigMatch@ does the next step in checking signature matching.
277 The tau-type part has already been unified. What we do here is to
278 check that this unification has not over-constrained the (polymorphic)
279 type variables of the original signature type.
281 The error message here is somewhat unsatisfactory, but it'll do for
285 checkSigMatch :: TcSigInfo s -> TcM s [TcTyVar s]
287 checkSigMatch (TySigInfo id sig_tyvars _ tau_ty src_loc)
288 = tcAddSrcLoc src_loc $
289 tcAddErrCtxt (sigCtxt id) $
290 checkSigTyVars sig_tyvars tau_ty (idType id)
294 %************************************************************************
296 \subsection[GenEtc-monomorphism]{The monomorphism restriction}
298 %************************************************************************
303 isUnRestrictedGroup :: [TcIdBndr s] -- Signatures given for these
307 isUnRestrictedGroup sigs EmptyBind = True
308 isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
309 isUnRestrictedGroup sigs (RecBind monobinds) = isUnResMono sigs monobinds
311 is_elem v vs = isIn "isUnResMono" v vs
313 isUnResMono sigs (PatMonoBind (VarPat (TcId v)) _ _) = v `is_elem` sigs
314 isUnResMono sigs (PatMonoBind other _ _) = False
315 isUnResMono sigs (VarMonoBind (TcId v) _) = v `is_elem` sigs
316 isUnResMono sigs (FunMonoBind _ _ _) = True
317 isUnResMono sigs (AndMonoBinds mb1 mb2) = isUnResMono sigs mb1 &&
319 isUnResMono sigs EmptyMonoBinds = True
323 %************************************************************************
325 \subsection[GenEtc-sig]{Matching a type signature}
327 %************************************************************************
329 @checkSigTyVars@ is used after the type in a type signature has been unified with
330 the actual type found. It then checks that the type variables of the type signature
332 (a) still all type variables
333 eg matching signature [a] against inferred type [(p,q)]
334 [then a will be unified to a non-type variable]
336 (b) still all distinct
337 eg matching signature [(a,b)] against inferred type [(p,p)]
338 [then a and b will be unified together]
340 (c) not mentioned in the environment
341 eg the signature for f in this:
347 Here, f is forced to be monorphic by the free occurence of x.
349 Before doing this, the substitution is applied to the signature type variable.
352 checkSigTyVars :: [TcTyVar s] -- The original signature type variables
353 -> TcType s -- signature type (for err msg)
354 -> TcType s -- inferred type (for err msg)
355 -> TcM s [TcTyVar s] -- Post-substitution signature type variables
357 checkSigTyVars sig_tyvars sig_tau inferred_tau
358 = tcGetGlobalTyVars `thenNF_Tc` \ env_tyvars ->
359 checkSigTyVarsGivenGlobals env_tyvars sig_tyvars sig_tau inferred_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)
365 -> TcType s -- inferred type (for err msg)
366 -> TcM s [TcTyVar s] -- Post-substitution signature type variables
368 checkSigTyVarsGivenGlobals globals sig_tyvars sig_tau inferred_tau
369 = -- Check point (a) above
370 mapNF_Tc (zonkTcType.mkTyVarTy) sig_tyvars `thenNF_Tc` \ sig_tys ->
371 checkMaybeTcM (allMaybes (map getTyVar_maybe sig_tys)) match_err `thenTc` \ sig_tyvars' ->
374 checkTcM (hasNoDups sig_tyvars') match_err `thenTc_`
377 -- We want to report errors in terms of the original signature tyvars,
378 -- ie sig_tyvars, NOT sig_tyvars'. sig_tys and sig_tyvars' correspond
379 -- 1-1 with sig_tyvars, so we can just map back.
381 mono_tyvars = [ sig_tyvar
382 | (sig_tyvar,sig_tyvar') <- zipEqual sig_tyvars sig_tyvars',
383 sig_tyvar' `elementOfTyVarSet` globals
386 checkTc (null mono_tyvars)
387 (notAsPolyAsSigErr sig_tau mono_tyvars) `thenTc_`
391 match_err = zonkTcType inferred_tau `thenNF_Tc` \ inferred_tau' ->
392 failTc (badMatchErr sig_tau inferred_tau')
396 %************************************************************************
398 \subsection[GenEtc-SpecTy]{Instantiate a type and create new dicts for it}
400 %************************************************************************
403 specTy :: InstOrigin s
405 -> NF_TcM s ([TcTyVar s], LIE s, TcType s, [TcIdOcc s])
407 specTy origin sigma_ty
408 = tcInstType [] sigma_ty `thenNF_Tc` \ tc_sigma_ty ->
410 (tyvars, theta, tau) = splitSigmaTy tc_sigma_ty
412 -- Instantiate the dictionary types
413 newDicts origin theta `thenNF_Tc` \ (dicts, dict_ids) ->
415 -- Return the list of tyvars, the list of dicts and the tau type
416 returnNF_Tc (tyvars, dicts, tau, dict_ids)
424 notAsPolyAsSigErr sig_tau mono_tyvars sty
425 = ppHang (ppStr "A type signature is more polymorphic than the inferred type")
426 4 (ppAboves [ppStr "(That is, one or more type variables in the inferred type can't be forall'd.)",
427 ppHang (ppStr "Monomorphic type variable(s):")
428 4 (interpp'SP sty mono_tyvars),
429 ppStr "Possible cause: the RHS mentions something subject to the monomorphism restriction"
435 badMatchErr sig_ty inferred_ty sty
436 = ppHang (ppStr "Type signature doesn't match inferred type")
437 4 (ppAboves [ppHang (ppStr "Signature:") 4 (ppr sty sig_ty),
438 ppHang (ppStr "Inferred :") 4 (ppr sty inferred_ty)
442 = ppSep [ppStr "When checking signature for", ppr sty id]
444 = ppSep [ppStr "When checking signature(s) for:", interpp'SP sty ids]
449 sigContextsErr ty_sigs sty
450 = ppHang (ppStr "A group of type signatures have mismatched contexts")
451 4 (ppAboves (map ppr_sig_info ty_sigs))
453 ppr_sig_info (TySigInfo val tyvars theta tau_ty _)
454 = ppHang (ppBeside (ppr sty val) (ppStr " :: "))
457 else ppBesides [ppStr "(",
458 ppIntersperse (ppStr ", ") (map (ppr_inst sty) theta),
460 ppr_inst sty (clas, ty) = ppCat [ppr sty clas, ppr sty ty]