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
17 import TcMonad hiding ( rnMtoTcM )
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(..),
24 newTyVarTy, zonkTcType, zonkTcTyVar, zonkTcTyVars
26 import Unify ( unifyTauTy )
28 import HsSyn ( HsBinds(..), Bind(..), MonoBinds(..), HsExpr, OutPat(..),
29 Sig, HsLit, ArithSeqInfo, InPat, GRHSsAndBinds, Match, Fake
31 import TcHsSyn ( TcIdOcc(..), TcIdBndr(..), TcHsBinds(..), TcBind(..), TcExpr(..), tcIdType )
33 import Bag ( Bag, foldBag, bagToList, listToBag, isEmptyBag )
34 import Class ( GenClass )
35 import Id ( GenId, Id(..), mkUserId, idType )
36 import Kind ( isUnboxedKind, isTypeKind, mkBoxedTypeKind )
37 import ListSetOps ( minusList, unionLists, intersectLists )
38 import Maybes ( Maybe(..), allMaybes )
39 import Name ( Name{--O only-} )
40 import Outputable ( interppSP, interpp'SP )
42 import PprType ( GenClass, GenType, GenTyVar )
43 import Type ( mkTyVarTy, splitSigmaTy, mkForAllTys, mkFunTys,
44 getTyVar, getTyVar_maybe, tyVarsOfTypes, eqSimpleTheta )
45 import TyVar ( GenTyVar, TyVar(..), tyVarKind, minusTyVarSet, emptyTyVarSet,
46 elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
47 import Usage ( UVar(..) )
48 import Unique ( Unique )
52 %************************************************************************
54 \subsection[Gen-SignatureInfo]{The @TcSigInfo@ type}
56 %************************************************************************
58 A type signature (or user-pragma) is typechecked to produce a
59 @TcSigInfo@. It contains @TcTypes@ because they are unified with
60 the variable's type, and after that checked to see whether they've
65 = TySigInfo (TcIdBndr s) -- for this value...
66 [TcTyVar s] (TcThetaType s) (TcTauType s)
71 %************************************************************************
73 \subsection[Gen-GEN]{Generalising bindings}
75 %************************************************************************
78 genBinds :: [Name] -- Binders
79 -> [TcIdBndr s] -- Monomorphic binders
80 -> TcBind s -- Type-checked monobind
81 -> LIE s -- LIE from typecheck of binds
82 -> [TcSigInfo s] -- Signatures, if any
83 -> (Name -> PragmaInfo) -- Gives pragma info for binder
84 -> TcM s (TcHsBinds s, LIE s, [TcIdBndr s])
87 In the call $(@genBinds@~env~bind~lie~lve)$, $(bind,lie,lve)$
88 is the result of typechecking a @Bind@. @genBinds@ implements the BIND-GEN
90 $lie$ and $lve$ may or may not be
91 fixed points of the current substitution.
96 An @AbsBind@ which wraps up $bind$ in a suitable abstraction.
98 an LIE, which is the part of the input LIE which isn't discharged by
99 the AbsBind. This means the parts which predicate type variables
102 An LVE whose domain is identical to that passed in.
103 Its range is a new set of locals to that passed in,
104 because they have been gen'd.
111 find $constrained$, the free variables of $env$.
112 First we must apply the current substitution to the environment, so that the
113 correct set of constrained type vars are extracted!
115 find $free$, the free variables of $lve$ which are not in $constrained$.
116 We need to apply the current subsitution to $lve$ first, of course.
118 minimise $lie$ to give $lie'$; all the constraints in $lie'$ are on
119 single type variables.
121 split $lie'$ into three: those predicating type variables in $constrained$,
122 those on type variables in $free$, and the rest.
124 complain about ``the rest'' part of $lie'$. These type variables are
127 generate new locals for each member of the domain of $lve$, with appropriately
130 generate a suitable AbsBinds to enclose the bindings.
134 genBinds binder_names mono_ids bind lie sig_infos prag_info_fn
135 = -- CHECK THAT THE SIGNATURES MATCH
136 -- Doesn't affect substitution
137 mapTc checkSigMatch sig_infos `thenTc_`
139 -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE IDENTICAL
140 -- The type signatures on a mutually-recursive group of definitions
141 -- must all have the same context (or none).
142 -- We have to zonk them first to make their type variables line up
143 mapNF_Tc get_zonked_theta sig_infos `thenNF_Tc` \ thetas ->
144 checkTc (null thetas || all (eqSimpleTheta (head thetas)) (tail thetas))
145 (sigContextsErr sig_infos) `thenTc_`
147 -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
148 mapNF_Tc (zonkTcType . idType) mono_ids `thenNF_Tc` \ mono_id_types ->
149 tcGetGlobalTyVars `thenNF_Tc` \ free_tyvars ->
151 mentioned_tyvars = tyVarsOfTypes mono_id_types
152 tyvars_to_gen = mentioned_tyvars `minusTyVarSet` free_tyvars
155 -- DEAL WITH OVERLOADING
156 resolveOverloading tyvars_to_gen lie bind sig_infos
157 `thenTc` \ (lie', reduced_tyvars_to_gen, dict_binds, dicts_bound) ->
159 -- Check for generaliseation over unboxed types, and
160 -- default any TypeKind TyVars to BoxedTypeKind
162 tyvars = tyVarSetToList reduced_tyvars_to_gen -- Commit to a particular order
164 unboxed_kind_tyvars = filter (isUnboxedKind . tyVarKind) tyvars
165 unresolved_kind_tyvars = filter (isTypeKind . tyVarKind) tyvars
167 box_it tyvar = newTyVarTy mkBoxedTypeKind `thenNF_Tc` \ boxed_ty ->
168 unifyTauTy (mkTyVarTy tyvar) boxed_ty
171 ASSERT( null unboxed_kind_tyvars ) -- The instCantBeGeneralised stuff in tcSimplify
172 -- should have dealt with unboxed type variables;
173 -- and it's better done there because we have more
174 -- precise origin information
176 mapTc box_it unresolved_kind_tyvars `thenTc_`
178 -- BUILD THE NEW LOCALS
180 dict_tys = map tcIdType dicts_bound
181 poly_tys = map (mkForAllTys tyvars . mkFunTys dict_tys) mono_id_types
182 poly_ids = zipWithEqual "genspecetc" mk_poly binder_names poly_tys
183 mk_poly name ty = mkUserId name ty (prag_info_fn name)
189 (zipEqual "genBinds" (map TcId mono_ids) (map TcId poly_ids))
196 get_zonked_theta (TySigInfo _ _ theta _ _)
197 = mapNF_Tc (\ (c,t) -> zonkTcType t `thenNF_Tc` \ t' -> returnNF_Tc (c,t')) theta
203 :: TcTyVarSet s -- Tyvars over which we are going to generalise
204 -> LIE s -- The LIE to deal with
205 -> TcBind s -- The binding group
206 -> [TcSigInfo s] -- And its real type-signature information
207 -> TcM s (LIE s, -- LIE to pass up the way; a fixed point of
208 -- the current substitution
209 TcTyVarSet s, -- Revised tyvars to generalise
210 [(TcIdOcc s, TcExpr s)], -- Dict bindings
211 [TcIdOcc s]) -- List of dicts to bind here
213 resolveOverloading tyvars_to_gen dicts bind ty_sigs
214 | not (isUnRestrictedGroup tysig_vars bind)
215 = -- Restricted group, so bind no dictionaries, and
216 -- remove from tyvars_to_gen any constrained type variables
218 -- *Don't* simplify dicts at this point, because we aren't going
219 -- to generalise over these dicts. By the time we do simplify them
220 -- we may well know more. For example (this actually came up)
221 -- f :: Array Int Int
222 -- f x = array ... xs where xs = [1,2,3,4,5]
223 -- We don't want to generate lots of (fromInt Int 1), (fromInt Int 2)
224 -- stuff. If we simplify only at the f-binding (not the xs-binding)
225 -- we'll know that the literals are all Ints, and we can just produce
228 -- Find all the type variables involved in overloading, the "constrained_tyvars"
229 -- These are the ones we *aren't* going to generalise.
230 -- We must be careful about doing this:
231 -- (a) If we fail to generalise a tyvar which is not actually
232 -- constrained, then it will never, ever get bound, and lands
233 -- up printed out in interface files! Notorious example:
234 -- instance Eq a => Eq (Foo a b) where ..
235 -- Here, b is not constrained, even though it looks as if it is.
236 -- Another, more common, example is when there's a Method inst in
237 -- the LIE, whose type might very well involve non-overloaded
239 -- (b) On the other hand, we mustn't generalise tyvars which are constrained,
240 -- because we are going to pass on out the unmodified LIE, with those
241 -- tyvars in it. They won't be in scope if we've generalised them.
243 -- So we are careful, and do a complete simplification just to find the
244 -- constrained tyvars. We don't use any of the results, except to
245 -- find which tyvars are constrained.
247 tcSimplify tyvars_to_gen dicts `thenTc` \ (_, _, dicts_sig) ->
249 -- ASSERT: dicts_sig is already zonked!
250 constrained_tyvars = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet dicts_sig
251 reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
254 -- Do it again, but with increased free_tyvars/reduced_tyvars_to_gen:
255 -- We still need to do this simplification, because some dictionaries
256 -- may gratuitouslyconstrain some tyvars over which we *are* going
258 -- For example d::Eq (Foo a b), where Foo is instanced as above.
259 tcSimplifyWithExtraGlobals constrained_tyvars reduced_tyvars_to_gen dicts
260 `thenTc` \ (dicts_free, dicts_binds, dicts_sig2) ->
261 ASSERT(isEmptyBag dicts_sig2)
263 returnTc (dicts_free, -- All these are left unbound
264 reduced_tyvars_to_gen,
265 dicts_binds, -- Local dict binds
266 []) -- No lambda-bound dicts
268 -- The returned LIE should be a fixed point of the substitution
270 | otherwise -- An unrestricted group
272 [] -> -- NO TYPE SIGNATURES
274 tcSimplify tyvars_to_gen dicts `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
275 returnTc (dicts_free, tyvars_to_gen, dict_binds,
276 map instToId (bagToList dicts_sig))
278 (TySigInfo _ _ theta _ _ : other) -> -- TYPE SIGNATURES PRESENT!
280 tcAddErrCtxt (sigsCtxt tysig_vars) $
282 newDicts SignatureOrigin theta `thenNF_Tc` \ (dicts_sig, dict_ids) ->
284 -- Check that the needed dicts can be expressed in
285 -- terms of the signature ones
287 tyvars_to_gen -- Type vars over which we will quantify
288 dicts_sig -- Available dicts
289 dicts -- Want bindings for these dicts
291 `thenTc` \ (dicts_free, dict_binds) ->
293 returnTc (dicts_free, tyvars_to_gen, dict_binds, dict_ids)
295 tysig_vars = [sig_var | (TySigInfo sig_var _ _ _ _) <- ty_sigs]
298 @checkSigMatch@ does the next step in checking signature matching.
299 The tau-type part has already been unified. What we do here is to
300 check that this unification has not over-constrained the (polymorphic)
301 type variables of the original signature type.
303 The error message here is somewhat unsatisfactory, but it'll do for
307 checkSigMatch :: TcSigInfo s -> TcM s ()
309 checkSigMatch (TySigInfo id sig_tyvars _ tau_ty src_loc)
310 = tcAddSrcLoc src_loc $
311 tcAddErrCtxt (sigCtxt id) $
312 checkSigTyVars sig_tyvars tau_ty
316 %************************************************************************
318 \subsection[GenEtc-monomorphism]{The monomorphism restriction}
320 %************************************************************************
325 isUnRestrictedGroup :: [TcIdBndr s] -- Signatures given for these
329 isUnRestrictedGroup sigs EmptyBind = True
330 isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
331 isUnRestrictedGroup sigs (RecBind monobinds) = isUnResMono sigs monobinds
333 is_elem v vs = isIn "isUnResMono" v vs
335 isUnResMono sigs (PatMonoBind (VarPat (TcId v)) _ _) = v `is_elem` sigs
336 isUnResMono sigs (PatMonoBind other _ _) = False
337 isUnResMono sigs (VarMonoBind (TcId v) _) = v `is_elem` sigs
338 isUnResMono sigs (FunMonoBind _ _ _ _) = True
339 isUnResMono sigs (AndMonoBinds mb1 mb2) = isUnResMono sigs mb1 &&
341 isUnResMono sigs EmptyMonoBinds = True
345 %************************************************************************
347 \subsection[GenEtc-sig]{Matching a type signature}
349 %************************************************************************
351 @checkSigTyVars@ is used after the type in a type signature has been unified with
352 the actual type found. It then checks that the type variables of the type signature
354 (a) still all type variables
355 eg matching signature [a] against inferred type [(p,q)]
356 [then a will be unified to a non-type variable]
358 (b) still all distinct
359 eg matching signature [(a,b)] against inferred type [(p,p)]
360 [then a and b will be unified together]
362 BUT ACTUALLY THESE FIRST TWO ARE FORCED BY USING DontBind TYVARS
364 (c) not mentioned in the environment
365 eg the signature for f in this:
371 Here, f is forced to be monorphic by the free occurence of x.
373 Before doing this, the substitution is applied to the signature type variable.
376 checkSigTyVars :: [TcTyVar s] -- The original signature type variables
377 -> TcType s -- signature type (for err msg)
380 checkSigTyVars sig_tyvars sig_tau
381 = checkSigTyVarsGivenGlobals emptyTyVarSet sig_tyvars sig_tau
383 checkSigTyVarsGivenGlobals
384 :: TcTyVarSet s -- Consider these tyvars as global in addition to envt ones
385 -> [TcTyVar s] -- The original signature type variables
386 -> TcType s -- signature type (for err msg)
389 checkSigTyVarsGivenGlobals extra_globals sig_tyvars sig_tau
390 = zonkTcTyVars extra_globals `thenNF_Tc` \ extra_tyvars' ->
391 tcGetGlobalTyVars `thenNF_Tc` \ env_tyvars ->
393 globals = env_tyvars `unionTyVarSets` extra_tyvars'
394 mono_tyvars = filter (`elementOfTyVarSet` globals) sig_tyvars
397 -- Until the final Bind-handling stuff is in, several type signatures in the same
398 -- bindings group can cause the signature type variable from the different
399 -- signatures to be unified. So we still need to zonk and check point (b).
400 -- Remove when activating the new binding code
401 mapNF_Tc zonkTcTyVar sig_tyvars `thenNF_Tc` \ sig_tys ->
402 checkTcM (hasNoDups (map (getTyVar "checkSigTyVars") sig_tys))
403 (zonkTcType sig_tau `thenNF_Tc` \ sig_tau' ->
404 failTc (badMatchErr sig_tau sig_tau')
409 -- We want to report errors in terms of the original signature tyvars,
410 -- ie sig_tyvars, NOT sig_tyvars'. sig_tys and sig_tyvars' correspond
411 -- 1-1 with sig_tyvars, so we can just map back.
412 checkTc (null mono_tyvars)
413 (notAsPolyAsSigErr sig_tau mono_tyvars)
422 notAsPolyAsSigErr sig_tau mono_tyvars sty
423 = ppHang (ppStr "A type signature is more polymorphic than the inferred type")
424 4 (ppAboves [ppStr "Some type variables in the inferred type can't be forall'd, namely:",
425 interpp'SP sty mono_tyvars,
426 ppStr "Possible cause: the RHS mentions something subject to the monomorphism restriction"
432 badMatchErr sig_ty inferred_ty sty
433 = ppHang (ppStr "Type signature doesn't match inferred type")
434 4 (ppAboves [ppHang (ppStr "Signature:") 4 (ppr sty sig_ty),
435 ppHang (ppStr "Inferred :") 4 (ppr sty inferred_ty)
439 = ppSep [ppStr "When checking signature for", ppr sty id]
441 = ppSep [ppStr "When checking signature(s) for:", interpp'SP sty ids]
446 sigContextsErr ty_sigs sty
447 = ppHang (ppStr "A group of type signatures have mismatched contexts")
448 4 (ppAboves (map ppr_sig_info ty_sigs))
450 ppr_sig_info (TySigInfo val tyvars theta tau_ty _)
451 = ppHang (ppBeside (ppr sty val) (ppStr " :: "))
454 else ppBesides [ppStr "(",
455 ppIntersperse (ppStr ", ") (map (ppr_inst sty) theta),
457 ppr_inst sty (clas, ty) = ppCat [ppr sty clas, ppr sty ty]