-Note [Implicit parameters and ambiguity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What type should we infer for this?
- f x = (show ?y, x::Int)
-Since we must quantify over the ?y, the most plausible type is
- f :: (Show a, ?y::a) => Int -> (String, Int)
-But notice that the type of the RHS is (String,Int), with no type
-varibables mentioned at all! The type of f looks ambiguous. But
-it isn't, because at a call site we might have
- let ?y = 5::Int in f 7
-and all is well. In effect, implicit parameters are, well, parameters,
-so we can take their type variables into account as part of the
-"tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
-
-
-Question 2: type signatures
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-BUT WATCH OUT: When you supply a type signature, we can't force you
-to quantify over implicit parameters. For example:
-
- (?x + 1) :: Int
-
-This is perfectly reasonable. We do not want to insist on
-
- (?x + 1) :: (?x::Int => Int)
-
-That would be silly. Here, the definition site *is* the occurrence site,
-so the above strictures don't apply. Hence the difference between
-tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
-and tcSimplifyCheckBind (which does not).
-
-What about when you supply a type signature for a binding?
-Is it legal to give the following explicit, user type
-signature to f, thus:
-
- f :: Int -> Int
- f x = (x::Int) + ?y
-
-At first sight this seems reasonable, but it has the nasty property
-that adding a type signature changes the dynamic semantics.
-Consider this:
-
- (let f x = (x::Int) + ?y
- in (f 3, f 3 with ?y=5)) with ?y = 6
-
- returns (3+6, 3+5)
-vs
- (let f :: Int -> Int
- f x = x + ?y
- in (f 3, f 3 with ?y=5)) with ?y = 6
-
- returns (3+6, 3+6)
-
-Indeed, simply inlining f (at the Haskell source level) would change the
-dynamic semantics.
-
-Nevertheless, as Launchbury says (email Oct 01) we can't really give the
-semantics for a Haskell program without knowing its typing, so if you
-change the typing you may change the semantics.
-
-To make things consistent in all cases where we are *checking* against
-a supplied signature (as opposed to inferring a type), we adopt the
-rule:
-
- a signature does not need to quantify over implicit params.
-
-[This represents a (rather marginal) change of policy since GHC 5.02,
-which *required* an explicit signature to quantify over all implicit
-params for the reasons mentioned above.]
-
-But that raises a new question. Consider
-
- Given (signature) ?x::Int
- Wanted (inferred) ?x::Int, ?y::Bool
-
-Clearly we want to discharge the ?x and float the ?y out. But
-what is the criterion that distinguishes them? Clearly it isn't
-what free type variables they have. The Right Thing seems to be
-to float a constraint that
- neither mentions any of the quantified type variables
- nor any of the quantified implicit parameters
-
-See the predicate isFreeWhenChecking.
-
-
-Question 3: monomorphism
-~~~~~~~~~~~~~~~~~~~~~~~~
-There's a nasty corner case when the monomorphism restriction bites:
-
- z = (x::Int) + ?y
-
-The argument above suggests that we *must* generalise
-over the ?y parameter, to get
- z :: (?y::Int) => Int,
-but the monomorphism restriction says that we *must not*, giving
- z :: Int.
-Why does the momomorphism restriction say this? Because if you have
-
- let z = x + ?y in z+z
-
-you might not expect the addition to be done twice --- but it will if
-we follow the argument of Question 2 and generalise over ?y.
-
-
-Question 4: top level
-~~~~~~~~~~~~~~~~~~~~~
-At the top level, monomorhism makes no sense at all.
-
- module Main where
- main = let ?x = 5 in print foo
-
- foo = woggle 3
-
- woggle :: (?x :: Int) => Int -> Int
- woggle y = ?x + y
-
-We definitely don't want (foo :: Int) with a top-level implicit parameter
-(?x::Int) becuase there is no way to bind it.
-
-
-Possible choices
-~~~~~~~~~~~~~~~~
-(A) Always generalise over implicit parameters
- Bindings that fall under the monomorphism restriction can't
- be generalised
-
- Consequences:
- * Inlining remains valid
- * No unexpected loss of sharing
- * But simple bindings like
- z = ?y + 1
- will be rejected, unless you add an explicit type signature
- (to avoid the monomorphism restriction)
- z :: (?y::Int) => Int
- z = ?y + 1
- This seems unacceptable
-
-(B) Monomorphism restriction "wins"
- Bindings that fall under the monomorphism restriction can't
- be generalised
- Always generalise over implicit parameters *except* for bindings
- that fall under the monomorphism restriction
-
- Consequences
- * Inlining isn't valid in general
- * No unexpected loss of sharing
- * Simple bindings like
- z = ?y + 1
- accepted (get value of ?y from binding site)
-
-(C) Always generalise over implicit parameters
- Bindings that fall under the monomorphism restriction can't
- be generalised, EXCEPT for implicit parameters
- Consequences
- * Inlining remains valid
- * Unexpected loss of sharing (from the extra generalisation)
- * Simple bindings like
- z = ?y + 1
- accepted (get value of ?y from occurrence sites)
-
-
-Discussion
-~~~~~~~~~~
-None of these choices seems very satisfactory. But at least we should
-decide which we want to do.
-
-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 and quantified)
- [Inst], -- Dict Ids that must be bound here (zonked)
- TcDictBinds) -- Bindings
- -- Any free (escaping) Insts are tossed into the environment
-\end{code}
-
-
-\begin{code}
-tcSimplifyInfer doc tau_tvs wanted
- = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars
- ; gbl_tvs <- tcGetGlobalTyVars
- ; let preds = fdPredsOfInsts wanted'
- qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
- (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
- ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound))
- ; extendLIEs free
-
- -- To make types simple, reduce as much as possible
- ; let try_me inst = ReduceMe AddSCs
- ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
-
- ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
-
- -- We can't abstract over implications
- ; let (dicts, implics) = partition isDict irreds
- ; loc <- getInstLoc (ImplicOrigin doc)
- ; implic_bind <- bindIrreds loc qtvs' dicts implics
-
- ; return (qtvs', dicts, binds `unionBags` implic_bind) }
- -- NB: when we are done, we might have some bindings, but
- -- the final qtvs might be empty. See Note [NO TYVARS] below.
-\end{code}
-
-\begin{code}
------------------------------------------------------------
--- 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
- :: InstLoc
- -> TcTyVarSet -- fv(T)
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM ([TyVar], -- Fully zonked, and quantified
- TcDictBinds) -- Bindings
-
-tcSimplifyInferCheck loc tau_tvs givens wanteds
- = do { (irreds, binds) <- innerCheckLoop loc givens wanteds
-
- -- 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.
- ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
- ; all_tvs <- zonkTcTyVarsAndFV all_tvs
- ; gbl_tvs <- tcGetGlobalTyVars
- ; let qtvs = varSetElems (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
-
- ; qtvs' <- zonkQuantifiedTyVars qtvs
-
- -- Now we are back to normal (c.f. tcSimplCheck)
- ; implic_bind <- bindIrreds loc qtvs' givens irreds
-
- ; return (qtvs', binds `unionBags` implic_bind) }
-\end{code}
-
-Note [Squashing methods]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Be careful if you want to float methods more:
- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
-From an application (truncate f i) we get
- t1 = truncate at f
- t2 = t1 at i
-If we have also have a second occurrence of truncate, we get
- t3 = truncate at f
- t4 = t3 at i
-When simplifying with i,f free, we might still notice that
-t1=t3; but alas, the binding for t2 (which mentions t1)
-may continue to float out!
-
-
-Note [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 Note [Inheriting implicit parameters]
-
-{- No longer used (with implication constraints)
-isFreeWhenChecking :: TyVarSet -- Quantified tyvars
- -> NameSet -- Quantified implicit parameters
- -> Inst -> Bool
-isFreeWhenChecking qtvs ips inst
- = isFreeWrtTyVars qtvs inst
- && isFreeWrtIPs ips inst
--}
-
-isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` 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.