-It's really not clear what is the Right Thing To Do. If you see
-
- z = (x::Int) + ?y
-
-would you expect the value of ?y to be got from the *occurrence sites*
-of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
-case of function definitions, the answer is clearly the former, but
-less so in the case of non-fucntion definitions. On the other hand,
-if we say that we get the value of ?y from the definition site of 'z',
-then inlining 'z' might change the semantics of the program.
-
-Choice (C) really says "the monomorphism restriction doesn't apply
-to implicit parameters". Which is fine, but remember that every
-innocent binding 'x = ...' that mentions an implicit parameter in
-the RHS becomes a *function* of that parameter, called at each
-use of 'x'. Now, the chances are that there are no intervening 'with'
-clauses that bind ?y, so a decent compiler should common up all
-those function calls. So I think I strongly favour (C). Indeed,
-one could make a similar argument for abolishing the monomorphism
-restriction altogether.
-
-BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
-
-
-
-%************************************************************************
-%* *
-\subsection{tcSimplifyInfer}
-%* *
-%************************************************************************
-
-tcSimplify is called when we *inferring* a type. Here's the overall game plan:
-
- 1. Compute Q = grow( fvs(T), C )
-
- 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
- predicates will end up in Ct; we deal with them at the top level
-
- 3. Try improvement, using functional dependencies
-
- 4. If Step 3 did any unification, repeat from step 1
- (Unification can change the result of 'grow'.)
-
-Note: we don't reduce dictionaries in step 2. For example, if we have
-Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
-after step 2. However note that we may therefore quantify over more
-type variables than we absolutely have to.
-
-For the guts, we need a loop, that alternates context reduction and
-improvement with unification. E.g. Suppose we have
-
- class C x y | x->y where ...
-
-and tcSimplify is called with:
- (C Int a, C Int b)
-Then improvement unifies a with b, giving
- (C Int a, C Int a)
-
-If we need to unify anything, we rattle round the whole thing all over
-again.
-
-
-\begin{code}
-tcSimplifyInfer
- :: SDoc
- -> TcTyVarSet -- fv(T); type vars
- -> [Inst] -- Wanted
- -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
- TcDictBinds, -- Bindings
- [TcId]) -- Dict Ids that must be bound here (zonked)
- -- Any free (escaping) Insts are tossed into the environment
-\end{code}
-
-
-\begin{code}
-tcSimplifyInfer doc tau_tvs wanted_lie
- = inferLoop doc (varSetElems tau_tvs)
- wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
-
- extendLIEs frees `thenM_`
- returnM (qtvs, binds, map instToId irreds)
-
-inferLoop doc tau_tvs wanteds
- = -- Step 1
- zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
- mappM zonkInst wanteds `thenM` \ wanteds' ->
- tcGetGlobalTyVars `thenM` \ gbl_tvs ->
- let
- preds = fdPredsOfInsts wanteds'
- qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
-
- try_me inst
- | isFreeWhenInferring qtvs inst = Free
- | isClassDict inst = DontReduceUnlessConstant -- Dicts
- | otherwise = ReduceMe NoSCs -- Lits and Methods
- in
- traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
- ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
- -- Step 2
- reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
-
- -- Step 3
- if no_improvement then
- returnM (varSetElems qtvs, frees, binds, irreds)
- else
- -- If improvement did some unification, we go round again. There
- -- are two subtleties:
- -- a) We start again with irreds, not wanteds
- -- Using an instance decl might have introduced a fresh type variable
- -- which might have been unified, so we'd get an infinite loop
- -- if we started again with wanteds! See example [LOOP]
- --
- -- b) It's also essential to re-process frees, because unification
- -- might mean that a type variable that looked free isn't now.
- --
- -- Hence the (irreds ++ frees)
-
- -- However, NOTICE that when we are done, we might have some bindings, but
- -- the final qtvs might be empty. See [NO TYVARS] below.
-
- inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
- returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
-\end{code}
-
-Example [LOOP]
-
- class If b t e r | b t e -> r
- instance If T t e t
- instance If F t e e
- class Lte a b c | a b -> c where lte :: a -> b -> c
- instance Lte Z b T
- instance (Lte a b l,If l b a c) => Max a b c
-
-Wanted: Max Z (S x) y
-
-Then we'll reduce using the Max instance to:
- (Lte Z (S x) l, If l (S x) Z y)
-and improve by binding l->T, after which we can do some reduction
-on both the Lte and If constraints. What we *can't* do is start again
-with (Max Z (S x) y)!
-
-[NO TYVARS]
-
- class Y a b | a -> b where
- y :: a -> X b
-
- instance Y [[a]] a where
- y ((x:_):_) = X x
-
- k :: X a -> X a -> X a
-
- g :: Num a => [X a] -> [X a]
- g xs = h xs
- where
- h ys = ys ++ map (k (y [[0]])) xs
-
-The excitement comes when simplifying the bindings for h. Initially
-try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
-From this we get t1:=:t2, but also various bindings. We can't forget
-the bindings (because of [LOOP]), but in fact t1 is what g is
-polymorphic in.
-
-The net effect of [NO TYVARS]
-
-\begin{code}
-isFreeWhenInferring :: TyVarSet -> Inst -> Bool
-isFreeWhenInferring qtvs inst
- = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
- && isInheritableInst inst -- And no implicit parameter involved
- -- (see "Notes on implicit parameters")
-
-isFreeWhenChecking :: TyVarSet -- Quantified tyvars
- -> NameSet -- Quantified implicit parameters
- -> Inst -> Bool
-isFreeWhenChecking qtvs ips inst
- = isFreeWrtTyVars qtvs inst
- && isFreeWrtIPs ips inst
-
-isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
-isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{tcSimplifyCheck}
-%* *
-%************************************************************************
-
-@tcSimplifyCheck@ is used when we know exactly the set of variables
-we are going to quantify over. For example, a class or instance declaration.
-
-\begin{code}
-tcSimplifyCheck
- :: SDoc
- -> [TcTyVar] -- Quantify over these
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds -- Bindings
-
--- tcSimplifyCheck is used when checking expression type signatures,
--- class decls, instance decls etc.
---
--- NB: tcSimplifyCheck does not consult the
--- global type variables in the environment; so you don't
--- need to worry about setting them before calling tcSimplifyCheck
-tcSimplifyCheck doc qtvs givens wanted_lie
- = ASSERT( all isSkolemTyVar qtvs )
- do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
- ; extendLIEs frees
- ; return binds }
- where
--- get_qtvs = zonkTcTyVarsAndFV qtvs
- get_qtvs = return (mkVarSet qtvs) -- All skolems
-
-
--- tcSimplifyInferCheck is used when we know the constraints we are to simplify
--- against, but we don't know the type variables over which we are going to quantify.
--- This happens when we have a type signature for a mutually recursive group
-tcSimplifyInferCheck
- :: SDoc
- -> TcTyVarSet -- fv(T)
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM ([TcTyVar], -- Variables over which to quantify
- TcDictBinds) -- Bindings
-
-tcSimplifyInferCheck doc tau_tvs givens wanted_lie
- = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
- ; extendLIEs frees
- ; return (qtvs', binds) }
- where
- -- Figure out which type variables to quantify over
- -- You might think it should just be the signature tyvars,
- -- but in bizarre cases you can get extra ones
- -- f :: forall a. Num a => a -> a
- -- f x = fst (g (x, head [])) + 1
- -- g a b = (b,a)
- -- Here we infer g :: forall a b. a -> b -> (b,a)
- -- We don't want g to be monomorphic in b just because
- -- f isn't quantified over b.
- all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
-
- get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
- tcGetGlobalTyVars `thenM` \ gbl_tvs ->
- let
- qtvs = all_tvs' `minusVarSet` gbl_tvs
- -- We could close gbl_tvs, but its not necessary for
- -- soundness, and it'll only affect which tyvars, not which
- -- dictionaries, we quantify over
- in
- returnM qtvs
-\end{code}
-
-Here is the workhorse function for all three wrappers.
-
-\begin{code}
-tcSimplCheck doc get_qtvs want_scs givens wanted_lie
- = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
-
- -- Complain about any irreducible ones
- ; if not (null irreds)
- then do { givens' <- mappM zonkInst given_dicts_and_ips
- ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
- else return ()
-
- ; returnM (qtvs, frees, binds) }
- where
- given_dicts_and_ips = filter (not . isMethod) givens
- -- For error reporting, filter out methods, which are
- -- only added to the given set as an optimisation
-
- ip_set = mkNameSet (ipNamesOfInsts givens)
-
- check_loop givens wanteds
- = -- Step 1
- mappM zonkInst givens `thenM` \ givens' ->
- mappM zonkInst wanteds `thenM` \ wanteds' ->
- get_qtvs `thenM` \ qtvs' ->
-
- -- Step 2
- let
- -- When checking against a given signature we always reduce
- -- until we find a match against something given, or can't reduce
- try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
- | otherwise = ReduceMe want_scs
- in
- reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
-
- -- Step 3
- if no_improvement then
- returnM (varSetElems qtvs', frees, binds, irreds)
- else
- check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
- returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
-\end{code}
-
-
-%************************************************************************
-%* *
- tcSimplifySuperClasses
-%* *
-%************************************************************************
-
-Note [SUPERCLASS-LOOP 1]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We have to be very, very careful when generating superclasses, lest we
-accidentally build a loop. Here's an example:
-
- class S a
-
- class S a => C a where { opc :: a -> a }
- class S b => D b where { opd :: b -> b }
-
- instance C Int where
- opc = opd
-
- instance D Int where
- opd = opc
-
-From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
-Simplifying, we may well get:
- $dfCInt = :C ds1 (opd dd)
- dd = $dfDInt
- ds1 = $p1 dd
-Notice that we spot that we can extract ds1 from dd.
-
-Alas! Alack! We can do the same for (instance D Int):
-
- $dfDInt = :D ds2 (opc dc)
- dc = $dfCInt
- ds2 = $p1 dc
-
-And now we've defined the superclass in terms of itself.
-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-
-Two more nasty cases are in
- tcrun021
- tcrun033
-
-\begin{code}
-tcSimplifySuperClasses qtvs givens sc_wanteds
- = ASSERT( all isSkolemTyVar qtvs )
- do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
- ; ext_default <- doptM Opt_ExtendedDefaultRules
- ; binds2 <- tc_simplify_top doc ext_default NoSCs frees
- ; return (binds1 `unionBags` binds2) }
- where
- get_qtvs = return (mkVarSet qtvs)
- doc = ptext SLIT("instance declaration superclass context")
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{tcSimplifyRestricted}
-%* *
-%************************************************************************
-
-tcSimplifyRestricted infers which type variables to quantify for a
-group of restricted bindings. This isn't trivial.
-
-Eg1: id = \x -> x
- We want to quantify over a to get id :: forall a. a->a
-
-Eg2: eq = (==)
- We do not want to quantify over a, because there's an Eq a
- constraint, so we get eq :: a->a->Bool (notice no forall)
-
-So, assume:
- RHS has type 'tau', whose free tyvars are tau_tvs
- RHS has constraints 'wanteds'
-
-Plan A (simple)
- Quantify over (tau_tvs \ ftvs(wanteds))
- This is bad. The constraints may contain (Monad (ST s))
- where we have instance Monad (ST s) where...
- so there's no need to be monomorphic in s!
-
- Also the constraint might be a method constraint,
- whose type mentions a perfectly innocent tyvar:
- op :: Num a => a -> b -> a
- Here, b is unconstrained. A good example would be
- foo = op (3::Int)
- We want to infer the polymorphic type
- foo :: forall b. b -> b
-
-
-Plan B (cunning, used for a long time up to and including GHC 6.2)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem). Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
- Step 2: Now simplify again, treating the constraint as 'free' if
- it does not mention qtvs, and trying to reduce it otherwise.
- The reasons for this is to maximise sharing.
-
- This fails for a very subtle reason. Suppose that in the Step 2
- a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
- In the Step 1 this constraint might have been simplified, perhaps to
- (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
- This won't happen in Step 2... but that in turn might prevent some other
- constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
- and that in turn breaks the invariant that no constraints are quantified over.
-
- Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
- the problem.
-
-
-Plan C (brutal)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem). Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
- Return the bindings from Step 1.
-
-
-A note about Plan C (arising from "bug" reported by George Russel March 2004)
-Consider this:
-
- instance (HasBinary ty IO) => HasCodedValue ty
-
- foo :: HasCodedValue a => String -> IO a
-
- doDecodeIO :: HasCodedValue a => () -> () -> IO a
- doDecodeIO codedValue view
- = let { act = foo "foo" } in act
-
-You might think this should work becuase the call to foo gives rise to a constraint
-(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
-restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
-constraint using the (rather bogus) instance declaration, and now we are stuffed.
-
-I claim this is not really a bug -- but it bit Sergey as well as George. So here's
-plan D
-
-
-Plan D (a variant of plan B)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
- Step 2: Now simplify again, treating the constraint as 'free' if
- it does not mention qtvs, and trying to reduce it otherwise.
-
- The point here is that it's generally OK to have too few qtvs; that is,
- to make the thing more monomorphic than it could be. We don't want to
- do that in the common cases, but in wierd cases it's ok: the programmer
- can always add a signature.
-
- Too few qtvs => too many wanteds, which is what happens if you do less
- improvement.
-
-
-\begin{code}
-tcSimplifyRestricted -- Used for restricted binding groups
- -- i.e. ones subject to the monomorphism restriction
- :: SDoc
- -> TopLevelFlag
- -> [Name] -- Things bound in this group
- -> TcTyVarSet -- Free in the type of the RHSs
- -> [Inst] -- Free in the RHSs
- -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
- TcDictBinds) -- Bindings
- -- tcSimpifyRestricted returns no constraints to
- -- quantify over; by definition there are none.
- -- They are all thrown back in the LIE
-
-tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
- -- Zonk everything in sight
- = mappM zonkInst wanteds `thenM` \ wanteds' ->
- zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
- tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
-
- -- 'reduceMe': Reduce as far as we can. Don't stop at
- -- dicts; the idea is to get rid of as many type
- -- variables as possible, and we don't want to stop
- -- at (say) Monad (ST s), because that reduces
- -- immediately, with no constraint on s.
- --
- -- BUT do no improvement! See Plan D above
- reduceContextWithoutImprovement
- doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
-
- -- Next, figure out the tyvars we will quantify over
- let
- constrained_tvs = tyVarsOfInsts constrained_dicts
- qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
- `minusVarSet` constrained_tvs
- in
- traceTc (text "tcSimplifyRestricted" <+> vcat [
- pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
- ppr _binds,
- ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
-
- -- The first step may have squashed more methods than
- -- necessary, so try again, this time more gently, knowing the exact
- -- set of type variables to quantify over.
- --
- -- We quantify only over constraints that are captured by qtvs;
- -- these will just be a subset of non-dicts. This in contrast
- -- to normal inference (using isFreeWhenInferring) in which we quantify over
- -- all *non-inheritable* constraints too. This implements choice
- -- (B) under "implicit parameter and monomorphism" above.
- --
- -- Remember that we may need to do *some* simplification, to
- -- (for example) squash {Monad (ST s)} into {}. It's not enough
- -- just to float all constraints
- --
- -- At top level, we *do* squash methods becuase we want to
- -- expose implicit parameters to the test that follows
- let
- is_nested_group = isNotTopLevel top_lvl
- try_me inst | isFreeWrtTyVars qtvs inst,
- (is_nested_group || isDict inst) = Free
- | otherwise = ReduceMe AddSCs
- in
- reduceContextWithoutImprovement
- doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
- ASSERT( null irreds )
-
- -- See "Notes on implicit parameters, Question 4: top level"
- if is_nested_group then
- extendLIEs frees `thenM_`
- returnM (varSetElems qtvs, binds)
- else
- let
- (non_ips, bad_ips) = partition isClassDict frees
- in
- addTopIPErrs bndrs bad_ips `thenM_`
- extendLIEs non_ips `thenM_`
- returnM (varSetElems qtvs, binds)
-\end{code}
-
-
-%************************************************************************
-%* *
- tcSimplifyRuleLhs
-%* *
-%************************************************************************
-
-On the LHS of transformation rules we only simplify methods and constants,
-getting dictionaries. We want to keep all of them unsimplified, to serve
-as the available stuff for the RHS of the rule.