module TcSimplify (
tcSimplifyInfer, tcSimplifyInferCheck,
tcSimplifyCheck, tcSimplifyRestricted,
- tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
+ tcSimplifyToDicts, tcSimplifyIPs,
+ tcSimplifyTop, tcSimplifyInteractive,
+ tcSimplifyBracket,
- tcSimplifyThetas, tcSimplifyCheckThetas,
+ tcSimplifyDeriv, tcSimplifyDefault,
bindInstsOfLocalFuns
) where
#include "HsVersions.h"
-import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
-import TcHsSyn ( TcExpr, TcId,
- TcMonoBinds, TcDictBinds
- )
-
-import TcMonad
-import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
- tyVarsOfInst, predsOfInsts, predsOfInst,
- isDict, isClassDict, instName,
- isStdClassTyVarDict, isMethodFor,
- instToId, tyVarsOfInsts,
- instBindingRequired, instCanBeGeneralised,
- newDictsFromOld, instMentionsIPs,
+import {-# SOURCE #-} TcUnify( unifyTauTy )
+import TcEnv -- temp
+import HsSyn ( HsBind(..), LHsBinds, HsExpr(..), LHsExpr )
+import TcHsSyn ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
+
+import TcRnMonad
+import Inst ( lookupInst, LookupInstResult(..),
+ tyVarsOfInst, fdPredsOfInsts, fdPredsOfInst, newDicts,
+ isDict, isClassDict, isLinearInst, linearInstType,
+ isStdClassTyVarDict, isMethodFor, isMethod,
+ instToId, tyVarsOfInsts, cloneDict,
+ ipNamesOfInsts, ipNamesOfInst, dictPred,
+ instBindingRequired,
+ newDictsFromOld, tcInstClassOp,
getDictClassTys, isTyVarDict,
- instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
- Inst, LIE, pprInsts, pprInstsInFull,
- mkLIE, lieToList
+ instLoc, zonkInst, tidyInsts, tidyMoreInsts,
+ Inst, pprInsts, pprInstsInFull, tcGetInstEnvs,
+ isIPDict, isInheritableInst, pprDFuns
)
-import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
-import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
-
-import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
-import TcType ( ThetaType, PredType, mkClassPred, isOverloadedTy,
- mkTyVarTy, tcGetTyVar, isTyVarClassPred,
- tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
- inheritablePred, predHasFDs )
-import Id ( idType )
-import NameSet ( mkNameSet )
-import Class ( classBigSig )
+import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals )
+import InstEnv ( lookupInstEnv, classInstEnv )
+import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
+import TcType ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
+ mkClassPred, isOverloadedTy, mkTyConApp,
+ mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
+ tyVarsOfPred, tcEqType )
+import Id ( idType, mkUserLocal )
+import Var ( TyVar )
+import Name ( getOccName, getSrcLoc )
+import NameSet ( NameSet, mkNameSet, elemNameSet )
+import Class ( classBigSig, classKey )
import FunDeps ( oclose, grow, improve, pprEquationDoc )
-import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
-
+import PrelInfo ( isNumericClass )
+import PrelNames ( splitName, fstName, sndName, integerTyConName,
+ showClassKey, eqClassKey, ordClassKey )
import Subst ( mkTopTyVarSubst, substTheta, substTy )
-import TysWiredIn ( unitTy )
+import TysWiredIn ( pairTyCon, doubleTy )
+import ErrUtils ( Message )
import VarSet
+import VarEnv ( TidyEnv )
import FiniteMap
+import Bag
import Outputable
import ListSetOps ( equivClasses )
-import Util ( zipEqual )
+import Util ( zipEqual, isSingleton )
import List ( partition )
+import SrcLoc ( Located(..) )
import CmdLineOpts
\end{code}
%************************************************************************
--------------------------------------
+ Notes on functional dependencies (a bug)
+ --------------------------------------
+
+| > class Foo a b | a->b
+| >
+| > class Bar a b | a->b
+| >
+| > data Obj = Obj
+| >
+| > instance Bar Obj Obj
+| >
+| > instance (Bar a b) => Foo a b
+| >
+| > foo:: (Foo a b) => a -> String
+| > foo _ = "works"
+| >
+| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
+| > runFoo f = f Obj
+|
+| *Test> runFoo foo
+|
+| <interactive>:1:
+| Could not deduce (Bar a b) from the context (Foo a b)
+| arising from use of `foo' at <interactive>:1
+| Probable fix:
+| Add (Bar a b) to the expected type of an expression
+| In the first argument of `runFoo', namely `foo'
+| In the definition of `it': it = runFoo foo
+|
+| Why all of the sudden does GHC need the constraint Bar a b? The
+| function foo didn't ask for that...
+
+The trouble is that to type (runFoo foo), GHC has to solve the problem:
+
+ Given constraint Foo a b
+ Solve constraint Foo a b'
+
+Notice that b and b' aren't the same. To solve this, just do
+improvement and then they are the same. But GHC currently does
+ simplify constraints
+ apply improvement
+ and loop
+
+That is usually fine, but it isn't here, because it sees that Foo a b is
+not the same as Foo a b', and so instead applies the instance decl for
+instance Bar a b => Foo a b. And that's where the Bar constraint comes
+from.
+
+The Right Thing is to improve whenever the constraint set changes at
+all. Not hard in principle, but it'll take a bit of fiddling to do.
+
+
+
+ --------------------------------------
Notes on quantification
--------------------------------------
--------------------------------------
+ The need for forall's in constraints
+ --------------------------------------
+
+[Exchange on Haskell Cafe 5/6 Dec 2000]
+
+ class C t where op :: t -> Bool
+ instance C [t] where op x = True
+
+ p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
+ q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
+
+The definitions of p and q differ only in the order of the components in
+the pair on their right-hand sides. And yet:
+
+ ghc and "Typing Haskell in Haskell" reject p, but accept q;
+ Hugs rejects q, but accepts p;
+ hbc rejects both p and q;
+ nhc98 ... (Malcolm, can you fill in the blank for us!).
+
+The type signature for f forces context reduction to take place, and
+the results of this depend on whether or not the type of y is known,
+which in turn depends on which component of the pair the type checker
+analyzes first.
+
+Solution: if y::m a, float out the constraints
+ Monad m, forall c. C (m c)
+When m is later unified with [], we can solve both constraints.
+
+
+ --------------------------------------
Notes on implicit parameters
--------------------------------------
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.
-BOTTOM LINE: you *must* quantify over implicit parameters. See
-isFreeAndInheritable.
+BOTTOM LINE: when *inferring types* you *must* quantify
+over implicit parameters. See the predicate isFreeWhenInferring.
-BUT WATCH OUT: for *expressions*, this isn't right. Consider:
+
+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
tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
and tcSimplifyCheckBind (which does not).
-
-Question 2: type signatures
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-OK, so is it legal to give an explicit, user type signature to f, thus:
+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
Indeed, simply inlining f (at the Haskell source level) would change the
dynamic semantics.
-Conclusion: the above type signature is illegal. You'll get a message
-of the form "could not deduce (?y::Int) from ()".
+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
tcSimplifyInfer
:: SDoc
-> TcTyVarSet -- fv(T); type vars
- -> LIE -- Wanted
+ -> [Inst] -- Wanted
-> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
- LIE, -- Free
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)
- (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
-
- -- Check for non-generalisable insts
- mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
+ wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
- returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
+ extendLIEs frees `thenM_`
+ returnM (qtvs, binds, map instToId irreds)
inferLoop doc tau_tvs wanteds
= -- Step 1
- zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
- mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
- tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
+ zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
+ mappM zonkInst wanteds `thenM` \ wanteds' ->
+ tcGetGlobalTyVars `thenM` \ gbl_tvs ->
let
- preds = predsOfInsts wanteds'
+ preds = fdPredsOfInsts wanteds'
qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
try_me inst
- | isFreeAndInheritable qtvs inst = Free
- | isClassDict inst = DontReduceUnlessConstant -- Dicts
- | otherwise = ReduceMe -- Lits and Methods
+ | isFreeWhenInferring qtvs inst = Free
+ | isClassDict inst = DontReduceUnlessConstant -- Dicts
+ | otherwise = ReduceMe -- 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' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+ reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
-- Step 3
if no_improvement then
- returnTc (varSetElems qtvs, frees, binds, irreds)
+ returnM (varSetElems qtvs, frees, binds, irreds)
else
-- If improvement did some unification, we go round again. There
-- are two subtleties:
--
-- Hence the (irreds ++ frees)
- inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
- returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
+ -- 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]
on both the Lte and If constraints. What we *can't* do is start again
with (Max Z (S x) y)!
-\begin{code}
-isFreeAndInheritable qtvs inst
- = isFree qtvs inst -- Constrains no quantified vars
- && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
- -- (see "Notes on implicit parameters")
+[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.
-isFree qtvs inst
- = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
+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}
:: SDoc
-> [TcTyVar] -- Quantify over these
-> [Inst] -- Given
- -> LIE -- Wanted
- -> TcM (LIE, -- Free
- TcDictBinds) -- Bindings
+ -> [Inst] -- Wanted
+ -> TcM TcDictBinds -- Bindings
--- tcSimplifyCheck is used when checking exprssion type signatures,
+-- tcSimplifyCheck is used when checking expression type signatures,
-- class decls, instance decls etc.
--- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
--- It's important that we can float out non-inheritable predicates
--- Example: (?x :: Int) is ok!
+--
+-- 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
- = tcSimplCheck doc isFree get_qtvs
- givens wanted_lie `thenTc` \ (qtvs', frees, binds) ->
- returnTc (frees, binds)
+ = tcSimplCheck doc get_qtvs
+ givens wanted_lie `thenM` \ (qtvs', binds) ->
+ returnM binds
where
get_qtvs = zonkTcTyVarsAndFV qtvs
:: SDoc
-> TcTyVarSet -- fv(T)
-> [Inst] -- Given
- -> LIE -- Wanted
+ -> [Inst] -- Wanted
-> TcM ([TcTyVar], -- Variables over which to quantify
- LIE, -- Free
TcDictBinds) -- Bindings
tcSimplifyInferCheck doc tau_tvs givens wanted_lie
- = tcSimplCheck doc isFreeAndInheritable get_qtvs givens wanted_lie
+ = tcSimplCheck doc get_qtvs givens wanted_lie
where
-- Figure out which type variables to quantify over
-- You might think it should just be the signature tyvars,
-- f isn't quantified over b.
all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
- get_qtvs = zonkTcTyVarsAndFV all_tvs `thenNF_Tc` \ all_tvs' ->
- tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
+ 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
- returnNF_Tc qtvs
+ returnM qtvs
\end{code}
Here is the workhorse function for all three wrappers.
\begin{code}
-tcSimplCheck doc is_free get_qtvs givens wanted_lie
- = check_loop givens (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
+tcSimplCheck doc get_qtvs givens wanted_lie
+ = check_loop givens wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
-- Complain about any irreducible ones
- complainCheck doc givens irreds `thenNF_Tc_`
+ mappM zonkInst given_dicts_and_ips `thenM` \ givens' ->
+ groupErrs (addNoInstanceErrs (Just doc) givens') irreds `thenM_`
-- Done
- returnTc (qtvs, mkLIE frees, binds)
+ extendLIEs frees `thenM_`
+ returnM (qtvs, 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
- mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
- mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
- get_qtvs `thenNF_Tc` \ qtvs' ->
+ 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 | is_free qtvs' inst = Free
- | otherwise = ReduceMe
+ try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
+ | otherwise = ReduceMe
in
- reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+ reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
-- Step 3
if no_improvement then
- returnTc (varSetElems qtvs', frees, binds, irreds)
+ returnM (varSetElems qtvs', frees, binds, irreds)
else
- check_loop givens' (irreds ++ frees) `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
- returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
+ check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
+ returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
\end{code}
-- i.e. ones subject to the monomorphism restriction
:: SDoc
-> TcTyVarSet -- Free in the type of the RHSs
- -> LIE -- Free in the RHSs
+ -> [Inst] -- Free in the RHSs
-> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
- LIE, -- Free
TcDictBinds) -- Bindings
-tcSimplifyRestricted doc tau_tvs wanted_lie
+tcSimplifyRestricted doc tau_tvs wanteds
= -- First squash out all methods, to find the constrained tyvars
-- We can't just take the free vars of wanted_lie because that'll
-- have methods that may incidentally mention entirely unconstrained variables
-- foo = f (3::Int)
-- We want to infer the polymorphic type
-- foo :: forall b. b -> b
- let
- wanteds = lieToList wanted_lie
- try_me inst = 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.
- in
- simpleReduceLoop doc try_me wanteds `thenTc` \ (_, _, constrained_dicts) ->
+
+ -- '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.
+ simpleReduceLoop doc reduceMe wanteds `thenM` \ (foo_frees, foo_binds, constrained_dicts) ->
-- Next, figure out the tyvars we will quantify over
- zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenNF_Tc` \ tau_tvs' ->
- tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
+ zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
+ tcGetGlobalTyVars `thenM` \ gbl_tvs ->
let
constrained_tvs = tyVarsOfInsts constrained_dicts
- qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
+ qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs)
`minusVarSet` constrained_tvs
in
+ traceTc (text "tcSimplifyRestricted" <+> vcat [
+ pprInsts wanteds, pprInsts foo_frees, pprInsts constrained_dicts,
+ ppr foo_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 knowing the exact
--
-- 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 isFreeAndInheritable) in which we quantify over
+ -- 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.
- mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
+ --
+ -- 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
+ restrict_loop doc qtvs wanteds
+ -- We still need a loop because improvement can take place
+ -- E.g. if we have (C (T a)) and the instance decl
+ -- instance D Int b => C (T a) where ...
+ -- and there's a functional dependency for D. Then we may improve
+ -- the tyep variable 'b'.
+
+restrict_loop doc qtvs wanteds
+ = mappM zonkInst wanteds `thenM` \ wanteds' ->
+ zonkTcTyVarsAndFV (varSetElems qtvs) `thenM` \ qtvs' ->
let
- try_me inst | isFree qtvs inst = Free
- | otherwise = ReduceMe
+ try_me inst | isFreeWrtTyVars qtvs' inst = Free
+ | otherwise = ReduceMe
in
- reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
- ASSERT( no_improvement )
- ASSERT( null irreds )
- -- No need to loop because simpleReduceLoop will have
- -- already done any improvement necessary
-
- returnTc (varSetElems qtvs, mkLIE frees, binds)
+ reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
+ if no_improvement then
+ ASSERT( null irreds )
+ extendLIEs frees `thenM_`
+ returnM (varSetElems qtvs', binds)
+ else
+ restrict_loop doc qtvs' (irreds ++ frees) `thenM` \ (qtvs1, binds1) ->
+ returnM (qtvs1, binds `unionBags` binds1)
\end{code}
Hence "DontReduce NoSCs"
\begin{code}
-tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
-tcSimplifyToDicts wanted_lie
- = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
+tcSimplifyToDicts wanteds
+ = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
-- Since try_me doesn't look at types, we don't need to
-- do any zonking, so it's safe to call reduceContext directly
ASSERT( null frees )
- returnTc (irreds, binds)
+ extendLIEs irreds `thenM_`
+ returnM binds
where
doc = text "tcSimplifyToDicts"
- wanteds = lieToList wanted_lie
-- Reduce methods and lits only; stop as soon as we get a dictionary
- try_me inst | isDict inst = DontReduce NoSCs
+ try_me inst | isDict inst = DontReduce NoSCs -- See notes above for why NoSCs
| otherwise = ReduceMe
\end{code}
+
+tcSimplifyBracket is used when simplifying the constraints arising from
+a Template Haskell bracket [| ... |]. We want to check that there aren't
+any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
+Show instance), but we aren't otherwise interested in the results.
+Nor do we care about ambiguous dictionaries etc. We will type check
+this bracket again at its usage site.
+
+\begin{code}
+tcSimplifyBracket :: [Inst] -> TcM ()
+tcSimplifyBracket wanteds
+ = simpleReduceLoop doc reduceMe wanteds `thenM_`
+ returnM ()
+ where
+ doc = text "tcSimplifyBracket"
+\end{code}
+
+
%************************************************************************
%* *
\subsection{Filtering at a dynamic binding}
\begin{code}
tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
- -> LIE
- -> TcM (LIE, TcDictBinds)
-tcSimplifyIPs given_ips wanted_lie
- = simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
- returnTc (mkLIE frees, binds)
+ -> [Inst] -- Wanted
+ -> TcM TcDictBinds
+tcSimplifyIPs given_ips wanteds
+ = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
+ extendLIEs frees `thenM_`
+ returnM binds
where
- doc = text "tcSimplifyIPs" <+> ppr ip_names
- wanteds = lieToList wanted_lie
- ip_names = map instName given_ips
- ip_set = mkNameSet ip_names
+ doc = text "tcSimplifyIPs" <+> ppr given_ips
+ ip_set = mkNameSet (ipNamesOfInsts given_ips)
-- Simplify any methods that mention the implicit parameter
- try_me inst | inst `instMentionsIPs` ip_set = ReduceMe
- | otherwise = Free
+ try_me inst | isFreeWrtIPs ip_set inst = Free
+ | otherwise = ReduceMe
simpl_loop givens wanteds
- = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
- mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+ = mappM zonkInst givens `thenM` \ givens' ->
+ mappM zonkInst wanteds `thenM` \ wanteds' ->
- reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+ reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
if no_improvement then
ASSERT( null irreds )
- returnTc (frees, binds)
+ returnM (frees, binds)
else
- simpl_loop givens' (irreds ++ frees) `thenTc` \ (frees1, binds1) ->
- returnTc (frees1, binds `AndMonoBinds` binds1)
+ simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
+ returnM (frees1, binds `unionBags` binds1)
\end{code}
@LIE@), as well as the @HsBinds@ generated.
\begin{code}
-bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
+bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM (LHsBinds TcId)
-bindInstsOfLocalFuns init_lie local_ids
+bindInstsOfLocalFuns wanteds local_ids
| null overloaded_ids
-- Common case
- = returnTc (init_lie, EmptyMonoBinds)
+ = extendLIEs wanteds `thenM_`
+ returnM emptyBag
| otherwise
- = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+ = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
ASSERT( null irreds )
- returnTc (mkLIE frees, binds)
+ extendLIEs frees `thenM_`
+ returnM binds
where
doc = text "bindInsts" <+> ppr local_ids
- wanteds = lieToList init_lie
overloaded_ids = filter is_overloaded local_ids
is_overloaded id = isOverloadedTy (idType id)
| Free -- Return as free
+reduceMe :: Inst -> WhatToDo
+reduceMe inst = ReduceMe
+
data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
-- of a predicate when adding it to the avails
\end{code}
\begin{code}
-type RedState = (Avails, -- What's available
- [Inst]) -- Insts for which try_me returned Free
-
type Avails = FiniteMap Inst Avail
data Avail
- = Irred -- Used for irreducible dictionaries,
+ = IsFree -- Used for free Insts
+ | Irred -- Used for irreducible dictionaries,
-- which are going to be lambda bound
- | BoundTo TcId -- Used for dictionaries for which we have a binding
+ | Given TcId -- Used for dictionaries for which we have a binding
-- e.g. those "given" in a signature
+ Bool -- True <=> actually consumed (splittable IPs only)
| NoRhs -- Used for Insts like (CCallable f)
-- where no witness is required.
+ -- ToDo: remove?
| Rhs -- Used when there is a RHS
- TcExpr -- The RHS
+ (LHsExpr TcId) -- The RHS
[Inst] -- Insts free in the RHS; we need these too
-pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
+ | Linear -- Splittable Insts only.
+ Int -- The Int is always 2 or more; indicates how
+ -- many copies are required
+ Inst -- The splitter
+ Avail -- Where the "master copy" is
+
+ | LinRhss -- Splittable Insts only; this is used only internally
+ -- by extractResults, where a Linear
+ -- is turned into an LinRhss
+ [LHsExpr TcId] -- A supply of suitable RHSs
+
+pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
| (inst,avail) <- fmToList avails ]
instance Outputable Avail where
ppr = pprAvail
-pprAvail NoRhs = text "<no rhs>"
-pprAvail Irred = text "Irred"
-pprAvail (BoundTo x) = text "Bound to" <+> ppr x
-pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
+pprAvail NoRhs = text "<no rhs>"
+pprAvail IsFree = text "Free"
+pprAvail Irred = text "Irred"
+pprAvail (Given x b) = text "Given" <+> ppr x <+>
+ if b then text "(used)" else empty
+pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
+pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
\end{code}
Extracting the bindings from a bunch of Avails.
The loop startes
\begin{code}
-bindsAndIrreds :: Avails
+extractResults :: Avails
-> [Inst] -- Wanted
- -> (TcDictBinds, -- Bindings
- [Inst]) -- Irreducible ones
+ -> TcM (TcDictBinds, -- Bindings
+ [Inst], -- Irreducible ones
+ [Inst]) -- Free ones
-bindsAndIrreds avails wanteds
- = go avails EmptyMonoBinds [] wanteds
+extractResults avails wanteds
+ = go avails emptyBag [] [] wanteds
where
- go avails binds irreds [] = (binds, irreds)
+ go avails binds irreds frees []
+ = returnM (binds, irreds, frees)
- go avails binds irreds (w:ws)
+ go avails binds irreds frees (w:ws)
= case lookupFM avails w of
- Nothing -> -- Free guys come out here
- -- (If we didn't do addFree we could use this as the
- -- criterion for free-ness, and pick up the free ones here too)
- go avails binds irreds ws
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go avails binds irreds frees ws
- Just NoRhs -> go avails binds irreds ws
+ Just NoRhs -> go avails binds irreds frees ws
+ Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
+ Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
- Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
-
- Just (BoundTo id) -> go avails new_binds irreds ws
+ Just (Given id _) -> go avails new_binds irreds frees ws
where
- -- For implicit parameters, all occurrences share the same
- -- Id, so there is no need for synonym bindings
- new_binds | new_id == id = binds
- | otherwise = addBind binds new_id (HsVar id)
- new_id = instToId w
+ new_binds | id == instToId w = binds
+ | otherwise = addBind binds w (L (instSpan w) (HsVar id))
+ -- The sought Id can be one of the givens, via a superclass chain
+ -- and then we definitely don't want to generate an x=x binding!
- Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
+ Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
where
- id = instToId w
- avails' = addToFM avails w (BoundTo id)
-
-addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
+ new_binds = addBind binds w rhs
+
+ Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
+ -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
+ split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
+ go (addToFM avails w (LinRhss rhss))
+ (binds `unionBags` binds')
+ irreds' frees' (split_inst : w : ws)
+
+ Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
+ -> go new_avails new_binds irreds frees ws
+ where
+ new_binds = addBind binds w rhs
+ new_avails = addToFM avails w (LinRhss rhss)
+
+ get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
+ get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
+ returnM (w':irreds, frees, instToId w')
+ get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
+ returnM (irreds, w':frees, instToId w')
+
+ add_given avails w
+ | instBindingRequired w = addToFM avails w (Given (instToId w) True)
+ | otherwise = addToFM avails w NoRhs
+ -- NB: make sure that CCallable/CReturnable use NoRhs rather
+ -- than Given, else we end up with bogus bindings.
+
+ add_free avails w | isMethod w = avails
+ | otherwise = add_given avails w
+ -- NB: Hack alert!
+ -- Do *not* replace Free by Given if it's a method.
+ -- The following situation shows why this is bad:
+ -- 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)
+ -- will continue to float out!
+ -- (split n i a) returns: n rhss
+ -- auxiliary bindings
+ -- 1 or 0 insts to add to irreds
+
+
+split :: Int -> TcId -> TcId -> Inst
+ -> TcM (TcDictBinds, [LHsExpr TcId])
+-- (split n split_id root_id wanted) returns
+-- * a list of 'n' expressions, all of which witness 'avail'
+-- * a bunch of auxiliary bindings to support these expressions
+-- * one or zero insts needed to witness the whole lot
+-- (maybe be zero if the initial Inst is a Given)
+--
+-- NB: 'wanted' is just a template
+
+split n split_id root_id wanted
+ = go n
+ where
+ ty = linearInstType wanted
+ pair_ty = mkTyConApp pairTyCon [ty,ty]
+ id = instToId wanted
+ occ = getOccName id
+ loc = getSrcLoc id
+ span = instSpan wanted
+
+ go 1 = returnM (emptyBag, [L span $ HsVar root_id])
+
+ go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
+ expand n rhss `thenM` \ (binds2, rhss') ->
+ returnM (binds1 `unionBags` binds2, rhss')
+
+ -- (expand n rhss)
+ -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
+ -- e.g. expand 3 [rhs1, rhs2]
+ -- = ( { x = split rhs1 },
+ -- [fst x, snd x, rhs2] )
+ expand n rhss
+ | n `rem` 2 == 0 = go rhss -- n is even
+ | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
+ returnM (binds', head rhss : rhss')
+ where
+ go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
+ returnM (listToBag binds', concat rhss')
+
+ do_one rhs = newUnique `thenM` \ uniq ->
+ tcLookupId fstName `thenM` \ fst_id ->
+ tcLookupId sndName `thenM` \ snd_id ->
+ let
+ x = mkUserLocal occ uniq pair_ty loc
+ in
+ returnM (L span (VarBind x (mk_app span split_id rhs)),
+ [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
+
+mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
+
+mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
+
+addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
+ (VarBind (instToId inst) rhs))
+instSpan wanted = instLocSrcSpan (instLoc wanted)
\end{code}
[Inst]) -- Irreducible
simpleReduceLoop doc try_me wanteds
- = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
- reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+ = mappM zonkInst wanteds `thenM` \ wanteds' ->
+ reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
if no_improvement then
- returnTc (frees, binds, irreds)
+ returnM (frees, binds, irreds)
else
- simpleReduceLoop doc try_me (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
- returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
+ simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
+ returnM (frees1, binds `unionBags` binds1, irreds1)
\end{code}
-> (Inst -> WhatToDo)
-> [Inst] -- Given
-> [Inst] -- Wanted
- -> NF_TcM (Bool, -- True <=> improve step did no unification
+ -> TcM (Bool, -- True <=> improve step did no unification
[Inst], -- Free
TcDictBinds, -- Dictionary bindings
[Inst]) -- Irreducible
text "given" <+> ppr givens,
text "wanted" <+> ppr wanteds,
text "----------------------"
- ])) `thenNF_Tc_`
+ ])) `thenM_`
-- Build the Avail mapping from "givens"
- foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
+ foldlM addGiven emptyFM givens `thenM` \ init_state ->
-- Do the real work
- reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ state@(avails, frees) ->
+ reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
-- Do improvement, using everything in avails
-- In particular, avails includes all superclasses of everything
- tcImprove avails `thenTc` \ no_improvement ->
+ tcImprove avails `thenM` \ no_improvement ->
+
+ extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
text "frees" <+> ppr frees,
text "no_improvement =" <+> ppr no_improvement,
text "----------------------"
- ])) `thenNF_Tc_`
- let
- (binds, irreds) = bindsAndIrreds avails wanteds
- in
- returnTc (no_improvement, frees, binds, irreds)
+ ])) `thenM_`
+
+ returnM (no_improvement, frees, binds, irreds)
+tcImprove :: Avails -> TcM Bool -- False <=> no change
+-- Perform improvement using all the predicates in Avails
tcImprove avails
- = tcGetInstEnv `thenTc` \ inst_env ->
+ = tcGetInstEnvs `thenM` \ (home_ie, pkg_ie) ->
let
preds = [ (pred, pp_loc)
| inst <- keysFM avails,
let pp_loc = pprInstLoc (instLoc inst),
- pred <- predsOfInst inst,
- predHasFDs pred
+ pred <- fdPredsOfInst inst
]
-- Avails has all the superclasses etc (good)
-- It also has all the intermediates of the deduction (good)
-- It does not have duplicates (good)
-- NB that (?x::t1) and (?x::t2) will be held separately in avails
-- so that improve will see them separate
- eqns = improve (classInstEnv inst_env) preds
+ eqns = improve get_insts preds
+ get_insts clas = classInstEnv home_ie clas ++ classInstEnv pkg_ie clas
in
if null eqns then
- returnTc True
+ returnM True
else
- traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenNF_Tc_`
- mapTc_ unify eqns `thenTc_`
- returnTc False
+ traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
+ mappM_ unify eqns `thenM_`
+ returnM False
where
unify ((qtvs, t1, t2), doc)
- = tcAddErrCtxt doc $
- tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
+ = addErrCtxt doc $
+ tcInstTyVars VanillaTv (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
unifyTauTy (substTy tenv t1) (substTy tenv t2)
\end{code}
-- along with its depth
-> (Inst -> WhatToDo)
-> [Inst]
- -> RedState
- -> TcM RedState
+ -> Avails
+ -> TcM Avails
\end{code}
@reduce@ is passed
Free return this in "frees"
wanteds: The list of insts to reduce
- state: An accumulating parameter of type RedState
+ state: An accumulating parameter of type Avails
that contains the state of the algorithm
- It returns a RedState.
+ It returns a Avails.
The (n,stack) pair is just used for error reporting.
n is always the depth of the stack.
#endif
go wanteds state
where
- go [] state = returnTc state
- go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenTc` \ state' ->
+ go [] state = returnM state
+ go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
go ws state'
-- Base case: we're done!
-reduce stack try_me wanted state
+reduce stack try_me wanted avails
-- It's the same as an existing inst, or a superclass thereof
- | isAvailable state wanted
- = returnTc state
+ | Just avail <- isAvailable avails wanted
+ = if isLinearInst wanted then
+ addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
+ reduceList stack try_me wanteds' avails'
+ else
+ returnM avails -- No op for non-linear things
| otherwise
= case try_me wanted of {
- DontReduce want_scs -> addIrred want_scs state wanted
+ DontReduce want_scs -> addIrred want_scs avails wanted
; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
-- First, see if the inst can be reduced to a constant in one step
try_simple addFree
; ReduceMe -> -- It should be reduced
- lookupInst wanted `thenNF_Tc` \ lookup_result ->
+ lookupInst wanted `thenM` \ lookup_result ->
case lookup_result of
- GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
- addWanted state' wanted rhs wanteds'
- SimpleInst rhs -> addWanted state wanted rhs []
+ GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
+ reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
+ addWanted avails2 wanted rhs wanteds'
+ -- Experiment with temporarily doing addIrred *before* the reduceList,
+ -- which has the effect of adding the thing we are trying
+ -- to prove to the database before trying to prove the things it
+ -- needs. See note [RECURSIVE DICTIONARIES]
+ -- NB: we must not do an addWanted before, because that adds the
+ -- superclasses too, and thaat can lead to a spurious loop; see
+ -- the examples in [SUPERCLASS-LOOP]
+ -- So we do an addIrred before, and then overwrite it afterwards with addWanted
+
+ SimpleInst rhs -> addWanted avails wanted rhs []
NoInstance -> -- No such instance!
-- Add it and its superclasses
- addIrred AddSCs state wanted
-
+ addIrred AddSCs avails wanted
}
where
try_simple do_this_otherwise
- = lookupInst wanted `thenNF_Tc` \ lookup_result ->
+ = lookupInst wanted `thenM` \ lookup_result ->
case lookup_result of
- SimpleInst rhs -> addWanted state wanted rhs []
- other -> do_this_otherwise state wanted
+ SimpleInst rhs -> addWanted avails wanted rhs []
+ other -> do_this_otherwise avails wanted
\end{code}
\begin{code}
-isAvailable :: RedState -> Inst -> Bool
-isAvailable (avails, _) wanted = wanted `elemFM` avails
- -- NB: the Ord instance of Inst compares by the class/type info
+-------------------------
+isAvailable :: Avails -> Inst -> Maybe Avail
+isAvailable avails wanted = lookupFM avails wanted
+ -- NB 1: the Ord instance of Inst compares by the class/type info
-- *not* by unique. So
-- d1::C Int == d2::C Int
+addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
+addLinearAvailable avails avail wanted
+ -- avails currently maps [wanted -> avail]
+ -- Extend avails to reflect a neeed for an extra copy of avail
+
+ | Just avail' <- split_avail avail
+ = returnM (addToFM avails wanted avail', [])
+
+ | otherwise
+ = tcLookupId splitName `thenM` \ split_id ->
+ tcInstClassOp (instLoc wanted) split_id
+ [linearInstType wanted] `thenM` \ split_inst ->
+ returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
+
+ where
+ split_avail :: Avail -> Maybe Avail
+ -- (Just av) if there's a modified version of avail that
+ -- we can use to replace avail in avails
+ -- Nothing if there isn't, so we need to create a Linear
+ split_avail (Linear n i a) = Just (Linear (n+1) i a)
+ split_avail (Given id used) | not used = Just (Given id True)
+ | otherwise = Nothing
+ split_avail Irred = Nothing
+ split_avail IsFree = Nothing
+ split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
+
-------------------------
-addFree :: RedState -> Inst -> NF_TcM RedState
+addFree :: Avails -> Inst -> TcM Avails
-- When an Inst is tossed upstairs as 'free' we nevertheless add it
-- to avails, so that any other equal Insts will be commoned up right
-- here rather than also being tossed upstairs. This is really just
-- an optimisation, and perhaps it is more trouble that it is worth,
-- as the following comments show!
--
- -- NB1: do *not* add superclasses. If we have
+ -- NB: do *not* add superclasses. If we have
-- df::Floating a
-- dn::Num a
-- but a is not bound here, then we *don't* want to derive
-- dn from df here lest we lose sharing.
--
- -- NB2: do *not* add the Inst to avails at all if it's a method.
- -- The following situation shows why this is bad:
- -- 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)
- -- will continue to float out!
- -- Solution: never put methods in avail till they are captured
- -- in which case addFree isn't used
- --
- -- NB3: make sure that CCallable/CReturnable use NoRhs rather
- -- than BoundTo, else we end up with bogus bindings.
- -- c.f. instBindingRequired in addWanted
-addFree (avails, frees) free
- | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
- | otherwise = returnNF_Tc (avails, free:frees)
- where
- avail | instBindingRequired free = BoundTo (instToId free)
- | otherwise = NoRhs
-
-addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
-addWanted state@(avails, frees) wanted rhs_expr wanteds
--- Do *not* add superclasses as well. Here's an example of why not
--- class Eq a => Foo a b
--- instance Eq a => Foo [a] a
--- If we are reducing
--- (Foo [t] t)
--- we'll first deduce that it holds (via the instance decl). We
--- must not then overwrite the Eq t constraint with a superclass selection!
--- ToDo: this isn't entirely unsatisfactory, because
--- we may also lose some entirely-legitimate sharing this way
-
- = ASSERT( not (isAvailable state wanted) )
- returnNF_Tc (addToFM avails wanted avail, frees)
+addFree avails free = returnM (addToFM avails free IsFree)
+
+addWanted :: Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
+addWanted avails wanted rhs_expr wanteds
+ = addAvailAndSCs avails wanted avail
where
avail | instBindingRequired wanted = Rhs rhs_expr wanteds
| otherwise = ASSERT( null wanteds ) NoRhs
-addGiven :: RedState -> Inst -> NF_TcM RedState
-addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
-
-addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
-addIrred NoSCs (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
-addIrred AddSCs state irred = addAvailAndSCs state irred Irred
-
-addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
-addAvailAndSCs (avails, frees) wanted avail
- = add_avail_and_scs avails wanted avail `thenNF_Tc` \ avails' ->
- returnNF_Tc (avails', frees)
-
----------------------
-add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
-add_avail_and_scs avails wanted avail
- = add_scs (addToFM avails wanted avail) wanted
-
-add_scs :: Avails -> Inst -> NF_TcM Avails
+addGiven :: Avails -> Inst -> TcM Avails
+addGiven avails given = addAvailAndSCs avails given (Given (instToId given) False)
+ -- No ASSERT( not (given `elemFM` avails) ) because in an instance
+ -- decl for Ord t we can add both Ord t and Eq t as 'givens',
+ -- so the assert isn't true
+
+addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
+addIrred NoSCs avails irred = returnM (addToFM avails irred Irred)
+addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
+ addAvailAndSCs avails irred Irred
+
+addAvailAndSCs :: Avails -> Inst -> Avail -> TcM Avails
+addAvailAndSCs avails inst avail
+ | not (isClassDict inst) = returnM avails1
+ | otherwise = traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) `thenM_`
+ addSCs is_loop avails1 inst
+ where
+ avails1 = addToFM avails inst avail
+ is_loop inst = any (`tcEqType` idType (instToId inst)) dep_tys
+ -- Note: this compares by *type*, not by Unique
+ deps = findAllDeps emptyVarSet avail
+ dep_tys = map idType (varSetElems deps)
+
+ findAllDeps :: IdSet -> Avail -> IdSet
+ -- Find all the Insts that this one depends on
+ -- See Note [SUPERCLASS-LOOP]
+ -- Watch out, though. Since the avails may contain loops
+ -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
+ findAllDeps so_far (Rhs _ kids)
+ = foldl findAllDeps
+ (extendVarSetList so_far (map instToId kids)) -- Add the kids to so_far
+ [a | Just a <- map (lookupFM avails) kids] -- Find the kids' Avail
+ findAllDeps so_far other = so_far
+
+
+addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
-- Add all the superclasses of the Inst to Avails
+ -- The first param says "dont do this because the original thing
+ -- depends on this one, so you'd build a loop"
-- Invariant: the Inst is already in Avails.
-add_scs avails dict
- | not (isClassDict dict)
- = returnNF_Tc avails
-
- | otherwise -- It is a dictionary
- = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
- foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
+addSCs is_loop avails dict
+ = newDictsFromOld dict sc_theta' `thenM` \ sc_dicts ->
+ foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
where
(clas, tys) = getDictClassTys dict
(tyvars, sc_theta, sc_sels, _) = classBigSig clas
sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
- = case lookupFM avails sc_dict of
- Just (BoundTo _) -> returnNF_Tc avails -- See Note [SUPER] below
- other -> add_avail_and_scs avails sc_dict avail
+ | add_me sc_dict = addSCs is_loop avails' sc_dict
+ | otherwise = returnM avails
where
- sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
- avail = Rhs sc_sel_rhs [dict]
+ sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
+ avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
+
+ add_me :: Inst -> Bool
+ add_me sc_dict
+ | is_loop sc_dict = False -- See Note [SUPERCLASS-LOOP]
+ | otherwise = case lookupFM avails sc_dict of
+ Just (Given _ _) -> False -- Given is cheaper than superclass selection
+ other -> True
\end{code}
-Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
+Note [SUPERCLASS-LOOP]: Checking for loops
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have to be careful here. If we are *given* d1:Ord a,
and want to deduce (d2:C [a]) where
class Ord a => C a where
Then we'll use the instance decl to deduce C [a] and then add the
superclasses of C [a] to avails. But we must not overwrite the binding
for d1:Ord a (which is given) with a superclass selection or we'll just
-build a loop! Hence looking for BoundTo. Crudely, BoundTo is cheaper
-than a selection.
-
+build a loop!
+
+Here's another variant, immortalised in tcrun020
+ class Monad m => C1 m
+ class C1 m => C2 m x
+ instance C2 Maybe Bool
+For the instance decl we need to build (C1 Maybe), and it's no good if
+we run around and add (C2 Maybe Bool) and its superclasses to the avails
+before we search for C1 Maybe.
+
+Here's another example
+ class Eq b => Foo a b
+ instance Eq a => Foo [a] a
+If we are reducing
+ (Foo [t] t)
+
+we'll first deduce that it holds (via the instance decl). We must not
+then overwrite the Eq t constraint with a superclass selection!
+
+At first I had a gross hack, whereby I simply did not add superclass constraints
+in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
+becuase it lost legitimate superclass sharing, and it still didn't do the job:
+I found a very obscure program (now tcrun021) in which improvement meant the
+simplifier got two bites a the cherry... so something seemed to be an Irred
+first time, but reducible next time.
+
+Now we implement the Right Solution, which is to check for loops directly
+when adding superclasses. It's a bit like the occurs check in unification.
+
+
+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data D r = ZeroD | SuccD (r (D r));
+
+ instance (Eq (r (D r))) => Eq (D r) where
+ ZeroD == ZeroD = True
+ (SuccD a) == (SuccD b) = a == b
+ _ == _ = False;
+
+ equalDC :: D [] -> D [] -> Bool;
+ equalDC = (==);
+
+We need to prove (Eq (D [])). Here's how we go:
+
+ d1 : Eq (D [])
+
+by instance decl, holds if
+ d2 : Eq [D []]
+ where d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+ d3 : D []
+ where d2 = dfEqList d3
+ d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+ d3 = d1
+ d2 = dfEqList d3
+ d1 = dfEqD d2
+
+and it'll even run! The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+
%************************************************************************
%* *
%************************************************************************
-If a dictionary constrains a type variable which is
- * not mentioned in the environment
- * and not mentioned in the type of the expression
-then it is ambiguous. No further information will arise to instantiate
-the type variable; nor will it be generalised and turned into an extra
-parameter to a function.
-
-It is an error for this to occur, except that Haskell provided for
-certain rules to be applied in the special case of numeric types.
-Specifically, if
- * at least one of its classes is a numeric class, and
- * all of its classes are numeric or standard
-then the type variable can be defaulted to the first type in the
-default-type list which is an instance of all the offending classes.
-
-So here is the function which does the work. It takes the ambiguous
-dictionaries and either resolves them (producing bindings) or
-complains. It works by splitting the dictionary list by type
-variable, and using @disambigOne@ to do the real business.
-
@tcSimplifyTop@ is called once per module to simplify all the constant
and ambiguous Insts.
\begin{code}
-tcSimplifyTop :: LIE -> TcM TcDictBinds
-tcSimplifyTop wanted_lie
- = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
+tcSimplifyTop wanteds = tc_simplify_top False {- Not interactive loop -} wanteds
+tcSimplifyInteractive wanteds = tc_simplify_top True {- Interactive loop -} wanteds
+
+
+-- The TcLclEnv should be valid here, solely to improve
+-- error message generation for the monomorphism restriction
+tc_simplify_top is_interactive wanteds
+ = getLclEnv `thenM` \ lcl_env ->
+ traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env)) `thenM_`
+ simpleReduceLoop (text "tcSimplTop") reduceMe wanteds `thenM` \ (frees, binds, irreds) ->
ASSERT( null frees )
let
std_groups = equivClasses cmp_by_tyvar stds
-- Pick the ones which its worth trying to disambiguate
- (std_oks, std_bads) = partition worth_a_try std_groups
-
- -- Have a try at disambiguation
- -- if the type variable isn't bound
+ -- namely, the onese whose type variable isn't bound
-- up with one of the non-standard classes
+ (std_oks, std_bads) = partition worth_a_try std_groups
worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
-- Collect together all the bad guys
- bad_guys = non_stds ++ concat std_bads
+ bad_guys = non_stds ++ concat std_bads
+ (bad_ips, non_ips) = partition isIPDict bad_guys
+ (no_insts, ambigs) = partition no_inst non_ips
+ no_inst d = not (isTyVarDict d)
+ -- Previously, there was a more elaborate no_inst definition:
+ -- no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
+ -- fixed_tvs = oclose (fdPredsOfInsts tidy_dicts) emptyVarSet
+ -- But that seems over-elaborate to me; it only bites for class decls with
+ -- fundeps like this: class C a b | -> b where ...
in
- -- Disambiguate the ones that look feasible
- mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
- -- And complain about the ones that don't
+ -- Report definite errors
+ groupErrs (addNoInstanceErrs Nothing []) no_insts `thenM_`
+ addTopIPErrs bad_ips `thenM_`
+
+ -- Deal with ambiguity errors, but only if
+ -- if there has not been an error so far; errors often
+ -- give rise to spurious ambiguous Insts
+ ifErrsM (returnM []) (
+
+ -- Complain about the ones that don't fall under
+ -- the Haskell rules for disambiguation
-- This group includes both non-existent instances
-- e.g. Num (IO a) and Eq (Int -> Int)
-- and ambiguous dictionaries
-- e.g. Num a
- addTopAmbigErrs bad_guys `thenNF_Tc_`
+ addTopAmbigErrs ambigs `thenM_`
- returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
- where
- wanteds = lieToList wanted_lie
- try_me inst = ReduceMe
+ -- Disambiguate the ones that look feasible
+ mappM (disambigGroup is_interactive) std_oks
+ ) `thenM` \ binds_ambig ->
- d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
+ returnM (binds `unionBags` unionManyBags binds_ambig)
+
+----------------------------------
+d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
get_tv d = case getDictClassTys d of
(clas, [ty]) -> tcGetTyVar "tcSimplify" ty
(clas, [ty]) -> clas
\end{code}
+If a dictionary constrains a type variable which is
+ * not mentioned in the environment
+ * and not mentioned in the type of the expression
+then it is ambiguous. No further information will arise to instantiate
+the type variable; nor will it be generalised and turned into an extra
+parameter to a function.
+
+It is an error for this to occur, except that Haskell provided for
+certain rules to be applied in the special case of numeric types.
+Specifically, if
+ * at least one of its classes is a numeric class, and
+ * all of its classes are numeric or standard
+then the type variable can be defaulted to the first type in the
+default-type list which is an instance of all the offending classes.
+
+So here is the function which does the work. It takes the ambiguous
+dictionaries and either resolves them (producing bindings) or
+complains. It works by splitting the dictionary list by type
+variable, and using @disambigOne@ to do the real business.
+
@disambigOne@ assumes that its arguments dictionaries constrain all
the same type variable.
@void@.
\begin{code}
-disambigGroup :: [Inst] -- All standard classes of form (C a)
+disambigGroup :: Bool -- True <=> simplifying at top-level interactive loop
+ -> [Inst] -- All standard classes of form (C a)
-> TcM TcDictBinds
-disambigGroup dicts
- | any isNumericClass classes -- Guaranteed all standard classes
- -- see comment at the end of function for reasons as to
- -- why the defaulting mechanism doesn't apply to groups that
- -- include CCallable or CReturnable dicts.
- && not (any isCcallishClass classes)
+disambigGroup is_interactive dicts
+ | any std_default_class classes -- Guaranteed all standard classes
= -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
-- SO, TRY DEFAULT TYPES IN ORDER
-- default list which can satisfy all the ambiguous classes.
-- For example, if Real a is reqd, but the only type in the
-- default list is Int.
- tcGetDefaultTys `thenNF_Tc` \ default_tys ->
+ get_default_tys `thenM` \ default_tys ->
let
try_default [] -- No defaults work, so fail
- = failTc
+ = failM
try_default (default_ty : default_tys)
- = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
+ = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
-- default_tys instead
- tcSimplifyCheckThetas [] theta `thenTc` \ _ ->
- returnTc default_ty
+ tcSimplifyDefault theta `thenM` \ _ ->
+ returnM default_ty
where
theta = [mkClassPred clas [default_ty] | clas <- classes]
in
- -- See if any default works, and if so bind the type variable to it
- -- If not, add an AmbigErr
- recoverTc (addAmbigErrs dicts `thenNF_Tc_`
- returnTc EmptyMonoBinds) $
-
- try_default default_tys `thenTc` \ chosen_default_ty ->
-
- -- Bind the type variable and reduce the context, for real this time
- unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
- simpleReduceLoop (text "disambig" <+> ppr dicts)
- try_me dicts `thenTc` \ (frees, binds, ambigs) ->
- WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
- warnDefault dicts chosen_default_ty `thenTc_`
- returnTc binds
-
- | all isCreturnableClass classes
- = -- Default CCall stuff to (); we don't even both to check that () is an
- -- instance of CReturnable, because we know it is.
- unifyTauTy (mkTyVarTy tyvar) unitTy `thenTc_`
- returnTc EmptyMonoBinds
-
- | otherwise -- No defaults
- = addAmbigErrs dicts `thenNF_Tc_`
- returnTc EmptyMonoBinds
+ -- See if any default works
+ tryM (try_default default_tys) `thenM` \ mb_ty ->
+ case mb_ty of
+ Left _ -> bomb_out
+ Right chosen_default_ty -> choose_default chosen_default_ty
+
+ | otherwise -- No defaults
+ = bomb_out
where
- try_me inst = ReduceMe -- This reduce should not fail
- tyvar = get_tv (head dicts) -- Should be non-empty
- classes = map get_clas dicts
+ tyvar = get_tv (head dicts) -- Should be non-empty
+ classes = map get_clas dicts
+
+ std_default_class cls
+ = isNumericClass cls
+ || (is_interactive &&
+ classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+ -- In interactive mode, we default Show a to Show ()
+ -- to avoid graututious errors on "show []"
+
+ choose_default default_ty -- Commit to tyvar = default_ty
+ = -- Bind the type variable
+ unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
+ -- and reduce the context, for real this time
+ simpleReduceLoop (text "disambig" <+> ppr dicts)
+ reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
+ WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
+ warnDefault dicts default_ty `thenM_`
+ returnM binds
+
+ bomb_out = addTopAmbigErrs dicts `thenM_`
+ returnM emptyBag
+
+get_default_tys
+ = do { mb_defaults <- getDefaultTys
+ ; case mb_defaults of
+ Just tys -> return tys
+ Nothing -> -- No use-supplied default;
+ -- use [Integer, Double]
+ do { integer_ty <- tcMetaTy integerTyConName
+ ; return [integer_ty, doubleTy] } }
\end{code}
[Aside - why the defaulting mechanism is turned off when
instance declarations.
\begin{code}
-tcSimplifyThetas :: ThetaType -- Wanted
- -> TcM ThetaType -- Needed
-
-tcSimplifyThetas wanteds
- = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
- reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
+tcSimplifyDeriv :: [TyVar]
+ -> ThetaType -- Wanted
+ -> TcM ThetaType -- Needed
+
+tcSimplifyDeriv tyvars theta
+ = tcInstTyVars VanillaTv tyvars `thenM` \ (tvs, _, tenv) ->
+ -- The main loop may do unification, and that may crash if
+ -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
+ -- ToDo: what if two of them do get unified?
+ newDicts DataDeclOrigin (substTheta tenv theta) `thenM` \ wanteds ->
+ simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
+ ASSERT( null frees ) -- reduceMe never returns Free
+
+ doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
let
- -- For multi-param Haskell, check that the returned dictionaries
- -- don't have any of the form (C Int Bool) for which
- -- we expect an instance here
- -- For Haskell 98, check that all the constraints are of the form C a,
- -- where a is a type variable
- bad_guys | glaExts = [pred | pred <- irreds,
- isEmptyVarSet (tyVarsOfPred pred)]
- | otherwise = [pred | pred <- irreds,
- not (isTyVarClassPred pred)]
+ tv_set = mkVarSet tvs
+ simpl_theta = map dictPred irreds -- reduceMe squashes all non-dicts
+
+ check_pred pred
+ | isEmptyVarSet pred_tyvars -- Things like (Eq T) should be rejected
+ = addErrTc (noInstErr pred)
+
+ | not undecidable_ok && not (isTyVarClassPred pred)
+ -- Check that the returned dictionaries are all of form (C a b)
+ -- (where a, b are type variables).
+ -- We allow this if we had -fallow-undecidable-instances,
+ -- but note that risks non-termination in the 'deriving' context-inference
+ -- fixpoint loop. It is useful for situations like
+ -- data Min h a = E | M a (h a)
+ -- which gives the instance decl
+ -- instance (Eq a, Eq (h a)) => Eq (Min h a)
+ = addErrTc (noInstErr pred)
+
+ | not (pred_tyvars `subVarSet` tv_set)
+ -- Check for a bizarre corner case, when the derived instance decl should
+ -- have form instance C a b => D (T a) where ...
+ -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
+ -- of problems; in particular, it's hard to compare solutions for
+ -- equality when finding the fixpoint. So I just rule it out for now.
+ = addErrTc (badDerivedPred pred)
+
+ | otherwise
+ = returnM ()
+ where
+ pred_tyvars = tyVarsOfPred pred
+
+ rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
+ -- This reverse-mapping is a Royal Pain,
+ -- but the result should mention TyVars not TcTyVars
in
- if null bad_guys then
- returnTc irreds
- else
- mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
- failTc
+
+ mappM check_pred simpl_theta `thenM_`
+ checkAmbiguity tvs simpl_theta tv_set `thenM_`
+ returnM (substTheta rev_env simpl_theta)
+ where
+ doc = ptext SLIT("deriving classes for a data type")
\end{code}
-@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
+@tcSimplifyDefault@ just checks class-type constraints, essentially;
used with \tr{default} declarations. We are only interested in
whether it worked or not.
\begin{code}
-tcSimplifyCheckThetas :: ThetaType -- Given
- -> ThetaType -- Wanted
- -> TcM ()
-
-tcSimplifyCheckThetas givens wanteds
- = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
+tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
+ -> TcM ()
+
+tcSimplifyDefault theta
+ = newDicts DataDeclOrigin theta `thenM` \ wanteds ->
+ simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
+ ASSERT( null frees ) -- try_me never returns Free
+ mappM (addErrTc . noInstErr) irreds `thenM_`
if null irreds then
- returnTc ()
+ returnM ()
else
- mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
- failTc
-\end{code}
-
-
-\begin{code}
-type AvailsSimple = FiniteMap PredType Bool
- -- True => irreducible
- -- False => given, or can be derived from a given or from an irreducible
-
-reduceSimple :: ThetaType -- Given
- -> ThetaType -- Wanted
- -> NF_TcM ThetaType -- Irreducible
-
-reduceSimple givens wanteds
- = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
- returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
- where
- givens_fm = foldl addNonIrred emptyFM givens
-
-reduce_simple :: (Int,ThetaType) -- Stack
- -> AvailsSimple
- -> ThetaType
- -> NF_TcM AvailsSimple
-
-reduce_simple (n,stack) avails wanteds
- = go avails wanteds
+ failM
where
- go avails [] = returnNF_Tc avails
- go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
- go avails' ws
-
-reduce_simple_help stack givens wanted
- | wanted `elemFM` givens
- = returnNF_Tc givens
-
- | Just (clas, tys) <- getClassPredTys_maybe wanted
- = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
- case maybe_theta of
- Nothing -> returnNF_Tc (addSimpleIrred givens wanted)
- Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
-
- | otherwise
- = returnNF_Tc (addSimpleIrred givens wanted)
-
-addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
-addSimpleIrred givens pred
- = addSCs (addToFM givens pred True) pred
-
-addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
-addNonIrred givens pred
- = addSCs (addToFM givens pred False) pred
-
-addSCs givens pred
- | not (isClassPred pred) = givens
- | otherwise = foldl add givens sc_theta
- where
- Just (clas,tys) = getClassPredTys_maybe pred
- (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
- sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
-
- add givens ct
- = case lookupFM givens ct of
- Nothing -> -- Add it and its superclasses
- addSCs (addToFM givens ct False) ct
-
- Just True -> -- Set its flag to False; superclasses already done
- addToFM givens ct False
-
- Just False -> -- Already done
- givens
-
+ doc = ptext SLIT("default declaration")
\end{code}
now?
\begin{code}
-groupInsts :: [Inst] -> [[Inst]]
+groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
+ -> [Inst] -- The offending Insts
+ -> TcM ()
-- Group together insts with the same origin
-- We want to report them together in error messages
-groupInsts [] = []
-groupInsts (inst:insts) = (inst:friends) : groupInsts others
- where
- -- (It may seem a bit crude to compare the error messages,
- -- but it makes sure that we combine just what the user sees,
- -- and it avoids need equality on InstLocs.)
- (friends, others) = partition is_friend insts
- loc_msg = showSDoc (pprInstLoc (instLoc inst))
- is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
+groupErrs report_err []
+ = returnM ()
+groupErrs report_err (inst:insts)
+ = do_one (inst:friends) `thenM_`
+ groupErrs report_err others
-addTopAmbigErrs dicts
- = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts) `thenNF_Tc_`
- mapNF_Tc (addTopIPErrs tidy_env) (groupInsts bad_ips) `thenNF_Tc_`
- mapNF_Tc (addAmbigErr tidy_env) ambigs `thenNF_Tc_`
- returnNF_Tc ()
where
- fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
- (tidy_env, tidy_dicts) = tidyInsts dicts
- (bad_ips, non_ips) = partition is_ip tidy_dicts
- (no_insts, ambigs) = partition no_inst non_ips
- is_ip d = any isIPPred (predsOfInst d)
- no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
+ -- (It may seem a bit crude to compare the error messages,
+ -- but it makes sure that we combine just what the user sees,
+ -- and it avoids need equality on InstLocs.)
+ (friends, others) = partition is_friend insts
+ loc_msg = showSDoc (pprInstLoc (instLoc inst))
+ is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
+ do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
+ -- Add location and context information derived from the Insts
+
+-- Add the "arising from..." part to a message about bunch of dicts
+addInstLoc :: [Inst] -> Message -> Message
+addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
plural [x] = empty
plural xs = char 's'
-addTopIPErrs tidy_env tidy_dicts
- = addInstErrTcM (instLoc (head tidy_dicts))
- (tidy_env,
- ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
+addTopIPErrs dicts
+ = groupErrs report tidy_dicts
+ where
+ (tidy_env, tidy_dicts) = tidyInsts dicts
+ report dicts = addErrTcM (tidy_env, mk_msg dicts)
+ mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
+ plural tidy_dicts <+> pprInsts tidy_dicts)
+
+addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
+ -- Just d => d describes the construct
+ -> [Inst] -- What is given by the context or type sig
+ -> [Inst] -- What is wanted
+ -> TcM ()
+addNoInstanceErrs mb_what givens []
+ = returnM ()
+addNoInstanceErrs mb_what givens dicts
+ = -- Some of the dicts are here because there is no instances
+ -- and some because there are too many instances (overlap)
+ -- The first thing we do is separate them
+ getDOpts `thenM` \ dflags ->
+ tcGetInstEnvs `thenM` \ inst_envs ->
+ let
+ (tidy_env1, tidy_givens) = tidyInsts givens
+ (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
+
+ -- Run through the dicts, generating a message for each
+ -- overlapping one, but simply accumulating all the
+ -- no-instance ones so they can be reported as a group
+ (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
+ check_overlap (overlap_doc, no_inst_dicts) dict
+ | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
+ | otherwise
+ = case lookupInstEnv dflags inst_envs clas tys of
+ res@(ms, _)
+ | length ms > 1 -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
+ | otherwise -> (overlap_doc, dict : no_inst_dicts) -- No match
+ -- NB: there can be exactly one match, in the case where we have
+ -- instance C a where ...
+ -- (In this case, lookupInst doesn't bother to look up,
+ -- unless -fallow-undecidable-instances is set.)
+ -- So we report this as "no instance" rather than "overlap"; the fix is
+ -- to specify -fallow-undecidable-instances, but we leave that to the programmer!
+ where
+ (clas,tys) = getDictClassTys dict
+ in
+ mk_probable_fix tidy_env2 mb_what no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
+ let
+ no_inst_doc | null no_inst_dicts = empty
+ | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
+ heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
+ ptext SLIT("for") <+> pprInsts no_inst_dicts
+ | otherwise = sep [ptext SLIT("Could not deduce") <+> pprInsts no_inst_dicts,
+ nest 2 $ ptext SLIT("from the context") <+> pprInsts tidy_givens]
+ in
+ addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
+
+ where
+ mk_overlap_msg dict (matches, unifiers)
+ = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") <+> ppr dict)),
+ sep [ptext SLIT("Matching instances") <> colon,
+ nest 2 (pprDFuns (dfuns ++ unifiers))],
+ if null unifiers
+ then empty
+ else parens (ptext SLIT("The choice depends on the instantiation of") <+>
+ quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))))]
+ where
+ dfuns = [df | (_, (_,_,df)) <- matches]
+
+ mk_probable_fix tidy_env Nothing dicts -- Top level
+ = mkMonomorphismMsg tidy_env dicts
+ mk_probable_fix tidy_env (Just what) dicts -- Nested (type signatures, instance decls)
+ = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 fix1, nest 2 fix2])
+ where
+ fix1 = sep [ptext SLIT("Add") <+> pprInsts dicts,
+ ptext SLIT("to the") <+> what]
--- Used for top-level irreducibles
-addTopInstanceErrs tidy_env tidy_dicts
- = addInstErrTcM (instLoc (head tidy_dicts))
- (tidy_env,
- ptext SLIT("No instance") <> plural tidy_dicts <+>
- ptext SLIT("for") <+> pprInsts tidy_dicts)
+ fix2 | null instance_dicts = empty
+ | otherwise = ptext SLIT("Or add an instance declaration for")
+ <+> pprInsts instance_dicts
+ instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
+ -- Insts for which it is worth suggesting an adding an instance declaration
+ -- Exclude implicit parameters, and tyvar dicts
-addAmbigErrs dicts
- = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
+
+addTopAmbigErrs dicts
+-- Divide into groups that share a common set of ambiguous tyvars
+ = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
where
(tidy_env, tidy_dicts) = tidyInsts dicts
-addAmbigErr tidy_env tidy_dict
- = addInstErrTcM (instLoc tidy_dict)
- (tidy_env,
- sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
- nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
- where
- ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
+ tvs_of :: Inst -> [TcTyVar]
+ tvs_of d = varSetElems (tyVarsOfInst d)
+ cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
+
+ report :: [(Inst,[TcTyVar])] -> TcM ()
+ report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
+ = mkMonomorphismMsg tidy_env dicts `thenM` \ (tidy_env, mono_msg) ->
+ addSrcSpan (instLocSrcSpan (instLoc inst)) $
+ -- the location of the first one will do for the err message
+ addErrTcM (tidy_env, msg $$ mono_msg)
+ where
+ dicts = map fst pairs
+ msg = sep [text "Ambiguous type variable" <> plural tvs <+>
+ pprQuotedList tvs <+> in_msg,
+ nest 2 (pprInstsInFull dicts)]
+ in_msg | isSingleton dicts = text "in the top-level constraint:"
+ | otherwise = text "in these top-level constraints:"
+
+
+mkMonomorphismMsg :: TidyEnv -> [Inst] -> TcM (TidyEnv, Message)
+-- There's an error with these Insts; if they have free type variables
+-- it's probably caused by the monomorphism restriction.
+-- Try to identify the offending variable
+-- ASSUMPTION: the Insts are fully zonked
+mkMonomorphismMsg tidy_env insts
+ | isEmptyVarSet inst_tvs
+ = returnM (tidy_env, empty)
+ | otherwise
+ = findGlobals inst_tvs tidy_env `thenM` \ (tidy_env, docs) ->
+ returnM (tidy_env, mk_msg docs)
+ where
+ inst_tvs = tyVarsOfInsts insts
+
+ mk_msg [] = empty -- This happens in things like
+ -- f x = show (read "foo")
+ -- whre monomorphism doesn't play any role
+ mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
+ nest 2 (vcat docs),
+ ptext SLIT("Probable fix: give these definition(s) an explicit type signature")]
+
warnDefault dicts default_ty
- = doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
- tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
+ = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
+ addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
where
-- Tidy them first
(_, tidy_dicts) = tidyInsts dicts
- get_loc i = case instLoc i of { (_,loc,_) -> loc }
warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
quotes (ppr default_ty),
pprInstsInFull tidy_dicts]
-complainCheck doc givens irreds
- = mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
- mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds) `thenNF_Tc_`
- returnNF_Tc ()
- where
- given_dicts = filter isDict givens
- -- Filter out methods, which are only added to
- -- the given set as an optimisation
-
-addNoInstanceErrs what_doc givens dicts
- = tcGetInstEnv `thenNF_Tc` \ inst_env ->
- let
- (tidy_env1, tidy_givens) = tidyInsts givens
- (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
-
- doc = vcat [sep [herald <+> pprInsts tidy_dicts,
- nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
- ambig_doc,
- ptext SLIT("Probable fix:"),
- nest 4 fix1,
- nest 4 fix2]
-
- herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
- unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
- | otherwise = empty
-
- -- The error message when we don't find a suitable instance
- -- is complicated by the fact that sometimes this is because
- -- there is no instance, and sometimes it's because there are
- -- too many instances (overlap). See the comments in TcEnv.lhs
- -- with the InstEnv stuff.
-
- ambig_doc
- | not ambig_overlap = empty
- | otherwise
- = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
- nest 4 (ptext SLIT("depends on the instantiation of") <+>
- quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
-
- fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
- ptext SLIT("to the") <+> what_doc]
-
- fix2 | null instance_dicts
- = empty
- | otherwise
- = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
-
- instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
- -- Insts for which it is worth suggesting an adding an instance declaration
- -- Exclude implicit parameters, and tyvar dicts
-
- -- Checks for the ambiguous case when we have overlapping instances
- ambig_overlap = any ambig_overlap1 dicts
- ambig_overlap1 dict
- | isClassDict dict
- = case lookupInstEnv inst_env clas tys of
- NoMatch ambig -> ambig
- other -> False
- | otherwise = False
- where
- (clas,tys) = getDictClassTys dict
- in
- addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
-
-- Used for the ...Thetas variants; all top level
-addNoInstErr pred
- = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
+noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
+
+badDerivedPred pred
+ = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
+ ptext SLIT("type variables that are not data type parameters"),
+ nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
reduceDepthErr n stack
= vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
nest 4 (pprInstsInFull stack)]
reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
-
------------------------------------------------
-addCantGenErr inst
- = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
- nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
\end{code}
projects / ghc-hetmet.git / blobdiff