%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
-\section[TcSimplify]{TcSimplify}
-
+TcSimplify
\begin{code}
module TcSimplify (
tcSimplifyRuleLhs, tcSimplifyIPs,
tcSimplifySuperClasses,
tcSimplifyTop, tcSimplifyInteractive,
- tcSimplifyBracket,
+ tcSimplifyBracket, tcSimplifyCheckPat,
tcSimplifyDeriv, tcSimplifyDefault,
- bindInstsOfLocalFuns
+ bindInstsOfLocalFuns,
+
+ misMatchMsg
) where
#include "HsVersions.h"
import {-# SOURCE #-} TcUnify( unifyType )
-import TypeRep ( Type(..) )
-import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
-import TcHsSyn ( mkHsApp, mkHsTyApp, mkHsDictApp )
+import HsSyn
import TcRnMonad
-import Inst ( lookupInst, LookupInstResult(..),
- tyVarsOfInst, fdPredsOfInsts, newDicts,
- isDict, isClassDict, isLinearInst, linearInstType,
- isMethodFor, isMethod,
- instToId, tyVarsOfInsts, cloneDict,
- ipNamesOfInsts, ipNamesOfInst, dictPred,
- fdPredsOfInst,
- newDictsAtLoc, tcInstClassOp,
- getDictClassTys, isTyVarDict, instLoc,
- zonkInst, tidyInsts, tidyMoreInsts,
- pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
- isInheritableInst, pprDictsTheta
- )
-import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
- lclEnvElts, tcMetaTy )
-import InstEnv ( lookupInstEnv, classInstances, pprInstances )
-import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType,
- checkAmbiguity, checkInstTermination )
-import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,
- mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
- mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
- tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )
-import TcIface ( checkWiredInTyCon )
-import Id ( idType, mkUserLocal )
-import Var ( TyVar )
-import TyCon ( TyCon )
-import Name ( Name, getOccName, getSrcLoc )
-import NameSet ( NameSet, mkNameSet, elemNameSet )
-import Class ( classBigSig, classKey )
-import FunDeps ( oclose, grow, improve, pprEquation )
-import PrelInfo ( isNumericClass, isStandardClass )
-import PrelNames ( splitName, fstName, sndName, integerTyConName,
- showClassKey, eqClassKey, ordClassKey )
-import Type ( zipTopTvSubst, substTheta, substTy )
-import TysWiredIn ( pairTyCon, doubleTy, doubleTyCon )
-import ErrUtils ( Message )
-import BasicTypes ( TopLevelFlag, isNotTopLevel )
+import TcHsSyn ( hsLPatType )
+import Inst
+import TcEnv
+import InstEnv
+import TcType
+import TcMType
+import TcIface
+import TcTyFuns
+import DsUtils -- Big-tuple functions
+import Var
+import Name
+import NameSet
+import Class
+import FunDeps
+import PrelInfo
+import PrelNames
+import Type
+import TysWiredIn
+import ErrUtils
+import BasicTypes
import VarSet
-import VarEnv ( TidyEnv )
+import VarEnv
import FiniteMap
import Bag
import Outputable
-import ListSetOps ( equivClasses )
-import Util ( zipEqual, isSingleton )
-import List ( partition )
-import SrcLoc ( Located(..) )
-import DynFlags ( DynFlag(..) )
-import StaticFlags
+import Maybes
+import ListSetOps
+import Util
+import SrcLoc
+import DynFlags
+import FastString
+
+import Control.Monad
+import Data.List
\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...
+Consider this:
+
+ class C a b | a -> b
+ class D a b | a -> b
+
+ instance D a b => C a b -- Undecidable
+ -- (Not sure if it's crucial to this eg)
+ f :: C a b => a -> Bool
+ f _ = True
+
+ g :: C a b => a -> Bool
+ g = f
+
+Here f typechecks, but g does not!! Reason: before doing improvement,
+we reduce the (C a b1) constraint from the call of f to (D a b1).
+
+Here is a more complicated example:
+
+@
+ > 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:
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
- --------------------------------------
-
-Suppose we are about to do a generalisation step.
-We have in our hand
+Note [Choosing which variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are about to do a generalisation step. We have in our hand
G the environment
T the type of the RHS
(A) Q intersect fv(G) = EMPTY limits how big Q can be
(B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
-(A) says we can't quantify over a variable that's free in the
-environment. (B) says we must quantify over all the truly free
-variables in T, else we won't get a sufficiently general type. We do
-not *need* to quantify over any variable that is fixed by the free
-vars of the environment G.
+ (A) says we can't quantify over a variable that's free in the environment.
+ (B) says we must quantify over all the truly free variables in T, else
+ we won't get a sufficiently general type.
+
+We do not *need* to quantify over any variable that is fixed by the
+free vars of the environment G.
BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
So Q can be {c,d}, {b,c,d}
+In particular, it's perfectly OK to quantify over more type variables
+than strictly necessary; there is no need to quantify over 'b', since
+it is determined by 'a' which is free in the envt, but it's perfectly
+OK to do so. However we must not quantify over 'a' itself.
+
Other things being equal, however, we'd like to quantify over as few
variables as possible: smaller types, fewer type applications, more
-constraints can get into Ct instead of Cq.
-
-
------------------------------------------
-We will make use of
-
- fv(T) the free type vars of T
-
- oclose(vs,C) The result of extending the set of tyvars vs
- using the functional dependencies from C
-
- grow(vs,C) The result of extend the set of tyvars vs
- using all conceivable links from C.
-
- E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
- Then grow(vs,C) = {a,b,c}
-
- Note that grow(vs,C) `superset` grow(vs,simplify(C))
- That is, simplfication can only shrink the result of grow.
-
-Notice that
- oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
- grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
-
-
------------------------------------------
-
-Choosing Q
-~~~~~~~~~~
-Here's a good way to choose Q:
+constraints can get into Ct instead of Cq. Here's a good way to
+choose Q:
Q = grow( fv(T), C ) \ oclose( fv(G), C )
T = c->c
C = (Eq (T c d))
- Now oclose(fv(T),C) = {c}, because the functional dependency isn't
- apparent yet, and that's wrong. We must really quantify over d too.
-
+Now oclose(fv(T),C) = {c}, because the functional dependency isn't
+apparent yet, and that's wrong. We must really quantify over d too.
There really isn't any point in quantifying over any more than
grow( fv(T), C ), because the call sites can't possibly influence
- --------------------------------------
- Notes on ambiguity
- --------------------------------------
+-------------------------------------
+ Note [Ambiguity]
+-------------------------------------
It's very hard to be certain when a type is ambiguous. Consider
Notes on implicit parameters
--------------------------------------
-Question 1: can we "inherit" implicit parameters
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Inheriting implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
f x = (x::Int) + ?y
over implicit parameters. See the predicate isFreeWhenInferring.
+Note [Implicit parameters and ambiguity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Only a *class* predicate can give rise to ambiguity
+An *implicit parameter* cannot. For example:
+ foo :: (?x :: [a]) => Int
+ foo = length ?x
+is fine. The call site will suppply a particular 'x'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others. E.g.
+ foo :: (Show a, ?x::[a]) => Int
+ foo = show (?x++?x)
+The type of foo looks ambiguous. But it isn't, because at a call site
+we might have
+ let ?x = 5::Int in foo
+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
:: 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)
+ -> 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_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)
+tcSimplifyInfer doc tau_tvs wanted
+ = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ ; wanted' <- mapM zonkInst wanted -- Zonk before deciding quantified tyvars
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; let preds1 = fdPredsOfInsts wanted'
+ gbl_tvs1 = oclose preds1 gbl_tvs
+ qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
+ -- See Note [Choosing which variables to quantify]
+
+ -- To maximise sharing, remove from consideration any
+ -- constraints that don't mention qtvs at all
+ ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
+ ; extendLIEs free
+
+ -- To make types simple, reduce as much as possible
+ ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$
+ ppr gbl_tvs1 $$ ppr free $$ ppr bound))
+ ; (irreds1, binds1) <- tryHardCheckLoop doc bound
+
+ -- Note [Inference and implication constraints]
+ ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
+ ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
+
+ -- Now work out all over again which type variables to quantify,
+ -- exactly in the same way as before, but starting from irreds2. Why?
+ -- a) By now improvment may have taken place, and we must *not*
+ -- quantify over any variable free in the environment
+ -- tc137 (function h inside g) is an example
+ --
+ -- b) Do not quantify over constraints that *now* do not
+ -- mention quantified type variables, because they are
+ -- simply ambiguous (or might be bound further out). Example:
+ -- f :: Eq b => a -> (a, b)
+ -- g x = fst (f x)
+ -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+ -- We decide to quantify over 'alpha' alone, but free1 does not include f77
+ -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
+ -- constraint (Eq beta), which we dump back into the free set
+ -- See test tcfail181
+ --
+ -- c) irreds may contain type variables not previously mentioned,
+ -- e.g. instance D a x => Foo [a]
+ -- wanteds = Foo [a]
+ -- Then after simplifying we'll get (D a x), and x is fresh
+ -- We must quantify over x else it'll be totally unbound
+ ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
+ ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
+ -- Note that we start from gbl_tvs1
+ -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
+ -- we've already put some of the original preds1 into frees
+ -- E.g. wanteds = C a b (where a->b)
+ -- gbl_tvs = {a}
+ -- tau_tvs = {b}
+ -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
+ -- irreds2 will be empty. But we don't want to generalise over b!
+ ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked
+ qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
+ ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
+ ; extendLIEs free
+
+ -- Turn the quantified meta-type variables into real type variables
+ ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
+
+ -- We can't abstract over any remaining unsolved
+ -- implications so instead just float them outwards. Ugh.
+ ; let (q_dicts0, implics) = partition isAbstractableInst irreds3
+ ; loc <- getInstLoc (ImplicOrigin doc)
+ ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
+
+ -- Prepare equality instances for quantification
+ ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
+ ; q_eqs <- mapM finalizeEqInst q_eqs0
+
+ ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `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.
+
+approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
+-- Note [Inference and implication constraints]
+-- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
+-- - fetching any dicts inside them that are free
+-- - using those dicts as cruder constraints, to solve the implications
+-- - returning the extra ones too
+
+approximateImplications doc want_dict irreds
+ | null extra_dicts
+ = return (irreds, emptyBag)
+ | otherwise
+ = do { extra_dicts' <- mapM cloneDict extra_dicts
+ ; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
+ -- By adding extra_dicts', we make them
+ -- available to solve the implication constraints
+ where
+ extra_dicts = get_dicts (filter isImplicInst irreds)
+
+ get_dicts :: [Inst] -> [Inst] -- Returns only Dicts
+ -- Find the wanted constraints in implication constraints that satisfy
+ -- want_dict, and are not bound by forall's in the constraint itself
+ get_dicts ds = concatMap get_dict ds
+
+ get_dict d@(Dict {}) | want_dict d = [d]
+ | otherwise = []
+ get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+ = [ d | let tv_set = mkVarSet tvs
+ , d <- get_dicts wanteds
+ , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
+ get_dict i@(EqInst {}) | want_dict i = [i]
+ | otherwise = []
+ get_dict other = pprPanic "approximateImplications" (ppr other)
\end{code}
-Example [LOOP]
+Note [Inference and implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have a wanted implication constraint (perhaps arising from
+a nested pattern match) like
+ C a => D [a]
+and we are now trying to quantify over 'a' when inferring the type for
+a function. In principle it's possible that there might be an instance
+ instance (C a, E a) => D [a]
+so the context (E a) would suffice. The Right Thing is to abstract over
+the implication constraint, but we don't do that (a) because it'll be
+surprising to programmers and (b) because we don't have the machinery to deal
+with 'given' implications.
+
+So our best approximation is to make (D [a]) part of the inferred
+context, so we can use that to discharge the implication. Hence
+the strange function get_dicts in approximateImplications.
+
+The common cases are more clear-cut, when we have things like
+ forall a. C a => C b
+Here, abstracting over (C b) is not an approximation at all -- but see
+Note [Freeness and implications].
+
+See Trac #1430 and test tc228.
- 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
+\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
-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)!
+tcSimplifyInferCheck loc tau_tvs givens wanteds
+ = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
-[NO TYVARS]
+ -- 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
+ ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
+ ; 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
\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")
+ = 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 = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
+isFreeWrtTyVars :: VarSet -> Inst -> Bool
+isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
+isFreeWrtIPs :: NameSet -> Inst -> Bool
isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
\end{code}
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.
+tcSimplifyCheck :: InstLoc
+ -> [TcTyVar] -- Quantify over these
+ -> [Inst] -- Given
+ -> [Inst] -- Wanted
+ -> TcM TcDictBinds -- Bindings
+tcSimplifyCheck loc qtvs givens wanteds
+ = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
+ do { traceTc (text "tcSimplifyCheck")
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ ; implic_bind <- bindIrreds loc qtvs givens irreds
+ ; return (binds `unionBags` implic_bind) }
+
+-----------------------------------------------------------
+-- tcSimplifyCheckPat is used for existential pattern match
+tcSimplifyCheckPat :: InstLoc
+ -> [TcTyVar] -- Quantify over these
+ -> [Inst] -- Given
+ -> [Inst] -- Wanted
+ -> TcM TcDictBinds -- Bindings
+tcSimplifyCheckPat loc qtvs givens wanteds
+ = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
+ do { traceTc (text "tcSimplifyCheckPat")
+ ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
+ ; implic_bind <- bindIrredsR loc qtvs givens irreds
+ ; return (binds `unionBags` implic_bind) }
+
+-----------------------------------------------------------
+bindIrreds :: InstLoc -> [TcTyVar]
+ -> [Inst] -> [Inst]
+ -> TcM TcDictBinds
+bindIrreds loc qtvs givens irreds
+ = bindIrredsR loc qtvs givens irreds
+
+bindIrredsR :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds
+-- Make a binding that binds 'irreds', by generating an implication
+-- constraint for them, *and* throwing the constraint into the LIE
+bindIrredsR loc qtvs givens irreds
+ | null irreds
+ = return emptyBag
+ | otherwise
+ = do { let givens' = filter isAbstractableInst givens
+ -- The givens can (redundantly) include methods
+ -- We want to retain both EqInsts and Dicts
+ -- There should be no implicadtion constraints
+ -- See Note [Pruning the givens in an implication constraint]
+
+ -- If there are no 'givens', then it's safe to
+ -- partition the 'wanteds' by their qtvs, thereby trimming irreds
+ -- See Note [Freeness and implications]
+ ; irreds' <- if null givens'
+ then do
+ { let qtv_set = mkVarSet qtvs
+ (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
+ ; extendLIEs frees
+ ; return real_irreds }
+ else return irreds
+
+ ; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds'
+ -- This call does the real work
+ -- If irreds' is empty, it does something sensible
+ ; extendLIEs implics
+ ; return bind }
+
+
+makeImplicationBind :: InstLoc -> [TcTyVar]
+ -> [Inst] -> [Inst]
+ -> TcM ([Inst], TcDictBinds)
+-- Make a binding that binds 'irreds', by generating an implication
+-- constraint for them, *and* throwing the constraint into the LIE
+-- The binding looks like
+-- (ir1, .., irn) = f qtvs givens
+-- where f is (evidence for) the new implication constraint
+-- f :: forall qtvs. {reft} givens => (ir1, .., irn)
+-- qtvs includes coercion variables
--
--- 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 }
+-- This binding must line up the 'rhs' in reduceImplication
+makeImplicationBind loc all_tvs
+ givens -- Guaranteed all Dicts
+ -- or EqInsts
+ irreds
+ | null irreds -- If there are no irreds, we are done
+ = return ([], emptyBag)
+ | otherwise -- Otherwise we must generate a binding
+ = do { uniq <- newUnique
+ ; span <- getSrcSpanM
+ ; let (eq_givens, dict_givens) = partition isEqInst givens
+ eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens)
+ -- Urgh! See line 2187 or thereabouts. I believe that all these
+ -- 'givens' must be a simple CoVar. This MUST be cleaned up.
+
+ ; let name = mkInternalName uniq (mkVarOcc "ic") span
+ implic_inst = ImplicInst { tci_name = name,
+ tci_tyvars = all_tvs,
+ tci_given = (eq_givens ++ dict_givens),
+ tci_wanted = irreds, tci_loc = loc }
+ ; let -- only create binder for dict_irreds
+ (_, dict_irreds) = partition isEqInst irreds
+ dict_irred_ids = map instToId dict_irreds
+ lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
+ rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
+ co = mkWpApps (map instToId dict_givens)
+ <.> mkWpTyApps eq_tyvar_cos
+ <.> mkWpTyApps (mkTyVarTys all_tvs)
+ bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs
+ | otherwise = PatBind { pat_lhs = lpat,
+ pat_rhs = unguardedGRHSs rhs,
+ pat_rhs_ty = hsLPatType lpat,
+ bind_fvs = placeHolderNames }
+ ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
+ ; return ([implic_inst], unitBag (L span bind))
+ }
+
+-----------------------------------------------------------
+tryHardCheckLoop :: SDoc
+ -> [Inst] -- Wanted
+ -> TcM ([Inst], TcDictBinds)
+
+tryHardCheckLoop doc wanteds
+ = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds
+ ; return (irreds,binds)
+ }
where
--- get_qtvs = zonkTcTyVarsAndFV qtvs
- get_qtvs = return (mkVarSet qtvs) -- All skolems
-
+ try_me _ = ReduceMe AddSCs
+ -- Here's the try-hard bit
--- 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
+-----------------------------------------------------------
+gentleCheckLoop :: InstLoc
+ -> [Inst] -- Given
+ -> [Inst] -- Wanted
+ -> TcM ([Inst], TcDictBinds)
-tcSimplifyInferCheck doc tau_tvs givens wanted_lie
- = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
- ; extendLIEs frees
- ; return (qtvs', binds) }
+gentleCheckLoop inst_loc givens wanteds
+ = do { (irreds,binds) <- checkLoop env wanteds
+ ; return (irreds,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
+ env = mkRedEnv (pprInstLoc inst_loc) try_me givens
+
+ try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ | otherwise = Stop
+ -- When checking against a given signature
+ -- we MUST be very gentle: Note [Check gently]
+
+gentleInferLoop :: SDoc -> [Inst]
+ -> TcM ([Inst], TcDictBinds)
+gentleInferLoop doc wanteds
+ = do { (irreds, binds) <- checkLoop env wanteds
+ ; return (irreds, binds) }
+ where
+ env = mkRedEnv doc try_me []
+ try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ | otherwise = Stop
\end{code}
-Here is the workhorse function for all three wrappers.
+Note [Check gently]
+~~~~~~~~~~~~~~~~~~~~
+We have to very careful about not simplifying too vigorously
+Example:
+ data T a where
+ MkT :: a -> T [a]
+
+ f :: Show b => T b -> b
+ f (MkT x) = show [x]
+
+Inside the pattern match, which binds (a:*, x:a), we know that
+ b ~ [a]
+Hence we have a dictionary for Show [a] available; and indeed we
+need it. We are going to build an implication contraint
+ forall a. (b~[a]) => Show [a]
+Later, we will solve this constraint using the knowledge (Show b)
+
+But we MUST NOT reduce (Show [a]) to (Show a), else the whole
+thing becomes insoluble. So we simplify gently (get rid of literals
+and methods only, plus common up equal things), deferring the real
+work until top level, when we solve the implication constraint
+with tryHardCheckLooop.
-\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 ()
+\begin{code}
+-----------------------------------------------------------
+checkLoop :: RedEnv
+ -> [Inst] -- Wanted
+ -> TcM ([Inst], TcDictBinds)
+-- Precondition: givens are completely rigid
+-- Postcondition: returned Insts are zonked
+
+checkLoop env wanteds
+ = go env wanteds (return ())
+ where go env wanteds elim_skolems
+ = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+ ; env' <- zonkRedEnv env
+ ; wanteds' <- zonkInsts wanteds
+
+ ; (improved, binds, irreds, elim_more_skolems)
+ <- reduceContext env' wanteds'
+ ; let elim_skolems' = elim_skolems >> elim_more_skolems
- ; 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)
+ ; if not improved then
+ elim_skolems' >> return (irreds, binds)
+ else do
+
+ -- If improvement did some unification, we go round again.
+ -- 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 Note [LOOP]
+ { (irreds1, binds1) <- go env' irreds elim_skolems'
+ ; return (irreds1, binds `unionBags` binds1) } }
\end{code}
+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables. An example from tc237 in the
+testsuite is
+
+ class Modular s a | s -> a
+
+ wim :: forall a w. Integral a
+ => a -> (forall s. Modular s a => M s w) -> w
+ wim i k = error "urk"
+
+ test5 :: (Modular s a, Integral a) => M s a
+ test5 = error "urk"
+
+ test4 = wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside. When type checking test4, we have to check
+whether the signature of test5 is an instance of
+
+ (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens.
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+Unify.tcUnifyTys, which doesn't know about mutable type variables.
+
+
+Note [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)!
+
+
%************************************************************************
%* *
tcrun033
\begin{code}
-tcSimplifySuperClasses qtvs givens sc_wanteds
- = ASSERT( all isSkolemTyVar qtvs )
- do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
- ; binds2 <- tc_simplify_top doc False NoSCs frees
- ; return (binds1 `unionBags` binds2) }
+tcSimplifySuperClasses
+ :: InstLoc
+ -> [Inst] -- Given
+ -> [Inst] -- Wanted
+ -> TcM TcDictBinds
+tcSimplifySuperClasses loc givens sc_wanteds
+ = do { traceTc (text "tcSimplifySuperClasses")
+ ; (irreds,binds1) <- checkLoop env sc_wanteds
+ ; let (tidy_env, tidy_irreds) = tidyInsts irreds
+ ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
+ ; return binds1 }
where
- get_qtvs = return (mkVarSet qtvs)
- doc = ptext SLIT("instance declaration superclass context")
+ env = mkRedEnv (pprInstLoc loc) try_me givens
+ try_me _ = ReduceMe NoSCs
+ -- Like tryHardCheckLoop, but with NoSCs
\end{code}
-> [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)
+ -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified)
TcDictBinds) -- Bindings
-- tcSimpifyRestricted returns no constraints to
-- quantify over; by definition there are none.
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' ->
+ = do { traceTc (text "tcSimplifyRestricted")
+ ; wanteds' <- zonkInsts wanteds
- -- 'reduceMe': Reduce as far as we can. Don't stop at
+ -- '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) ->
+ -- HOWEVER, some unification may take place, if we instantiate
+ -- a method Inst with an equality constraint
+ ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe AddSCs)
+ ; (_imp, _binds, constrained_dicts, elim_skolems)
+ <- reduceContext env wanteds'
+ ; elim_skolems
-- 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,
+ ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ ; gbl_tvs' <- tcGetGlobalTyVars
+ ; constrained_dicts' <- zonkInsts constrained_dicts
+
+ ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
+ -- As in tcSimplifyInfer
+
+ -- Do not quantify over constrained type variables:
+ -- this is the monomorphism restriction
+ constrained_tvs' = tyVarsOfInsts constrained_dicts'
+ qtvs = qtvs1 `minusVarSet` constrained_tvs'
+ pp_bndrs = pprWithCommas (quotes . ppr) bndrs
+
+ -- Warn in the mono
+ ; warn_mono <- doptM Opt_WarnMonomorphism
+ ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
+ (vcat[ ptext (sLit "the Monomorphism Restriction applies to the binding")
+ <> plural bndrs <+> ptext (sLit "for") <+> pp_bndrs,
+ ptext (sLit "Consider giving a type signature for") <+> pp_bndrs])
+
+ ; traceTc (text "tcSimplifyRestricted" <+> vcat [
+ pprInsts wanteds, pprInsts constrained_dicts',
ppr _binds,
- ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
+ ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
-- The first step may have squashed more methods than
-- necessary, so try again, this time more gently, knowing the exact
--
-- 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 )
+ ; let is_nested_group = isNotTopLevel top_lvl
+ try_me inst | isFreeWrtTyVars qtvs inst,
+ (is_nested_group || isDict inst) = Stop
+ | otherwise = ReduceMe AddSCs
+ env = mkNoImproveRedEnv doc try_me
+ ; (_imp, binds, irreds, elim_skolems) <- reduceContext env wanteds'
+ ; elim_skolems
-- 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)
+ ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
+ if is_nested_group then
+ extendLIEs irreds
+ else do { let (bad_ips, non_ips) = partition isIPDict irreds
+ ; addTopIPErrs bndrs bad_ips
+ ; extendLIEs non_ips }
+
+ ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
+ ; return (qtvs', binds) }
\end{code}
| otherwise
= do { w' <- zonkInst w -- So that (3::Int) does not generate a call
-- to fromInteger; this looks fragile to me
- ; lookup_result <- lookupInst w'
+ ; lookup_result <- lookupSimpleInst w'
; case lookup_result of
- GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
- SimpleInst rhs -> go dicts (addBind binds w rhs) ws
+ GenInst ws' rhs ->
+ go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
}
\end{code}
\begin{code}
tcSimplifyBracket :: [Inst] -> TcM ()
tcSimplifyBracket wanteds
- = simpleReduceLoop doc reduceMe wanteds `thenM_`
- returnM ()
+ = do { tryHardCheckLoop doc wanteds
+ ; return () }
where
doc = text "tcSimplifyBracket"
\end{code}
tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
-> [Inst] -- Wanted
-> TcM TcDictBinds
+ -- We need a loop so that we do improvement, and then
+ -- (next time round) generate a binding to connect the two
+ -- let ?x = e in ?x
+ -- Here the two ?x's have different types, and improvement
+ -- makes them the same.
+
tcSimplifyIPs given_ips wanteds
- = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
- extendLIEs frees `thenM_`
- returnM binds
+ = do { wanteds' <- zonkInsts wanteds
+ ; given_ips' <- zonkInsts given_ips
+ -- Unusually for checking, we *must* zonk the given_ips
+
+ ; let env = mkRedEnv doc try_me given_ips'
+ ; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds'
+ ; elim_skolems
+
+ ; if not improved then
+ ASSERT( all is_free irreds )
+ do { extendLIEs irreds
+ ; return binds }
+ else
+ tcSimplifyIPs given_ips wanteds }
where
- doc = text "tcSimplifyIPs" <+> ppr given_ips
- ip_set = mkNameSet (ipNamesOfInsts given_ips)
+ doc = text "tcSimplifyIPs" <+> ppr given_ips
+ ip_set = mkNameSet (ipNamesOfInsts given_ips)
+ is_free inst = isFreeWrtIPs ip_set inst
-- Simplify any methods that mention the implicit parameter
- try_me inst | isFreeWrtIPs ip_set inst = Free
- | otherwise = ReduceMe NoSCs
-
- simpl_loop givens wanteds
- = mappM zonkInst givens `thenM` \ givens' ->
- mappM zonkInst wanteds `thenM` \ wanteds' ->
-
- reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
-
- if no_improvement then
- ASSERT( null irreds )
- returnM (frees, binds)
- else
- simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
- returnM (frees1, binds `unionBags` binds1)
+ try_me inst | is_free inst = Stop
+ | otherwise = ReduceMe NoSCs
\end{code}
-- arguably a bug in Match.tidyEqnInfo (see notes there)
bindInstsOfLocalFuns wanteds local_ids
- | null overloaded_ids
+ | null overloaded_ids = do
-- Common case
- = extendLIEs wanteds `thenM_`
- returnM emptyLHsBinds
+ extendLIEs wanteds
+ return emptyLHsBinds
| otherwise
- = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
- ASSERT( null irreds )
- extendLIEs not_for_me `thenM_`
- extendLIEs frees `thenM_`
- returnM binds
+ = do { (irreds, binds) <- gentleInferLoop doc for_me
+ ; extendLIEs not_for_me
+ ; extendLIEs irreds
+ ; return binds }
where
doc = text "bindInsts" <+> ppr local_ids
overloaded_ids = filter is_overloaded local_ids
overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
-- so it's worth building a set, so that
-- lookup (in isMethodFor) is faster
- try_me inst | isMethod inst = ReduceMe NoSCs
- | otherwise = Free
\end{code}
The main control over context reduction is here
\begin{code}
+data RedEnv
+ = RedEnv { red_doc :: SDoc -- The context
+ , red_try_me :: Inst -> WhatToDo
+ , red_improve :: Bool -- True <=> do improvement
+ , red_givens :: [Inst] -- All guaranteed rigid
+ -- Always dicts
+ -- but see Note [Rigidity]
+ , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
+ -- See Note [RedStack]
+ }
+
+-- Note [Rigidity]
+-- The red_givens are rigid so far as cmpInst is concerned.
+-- There is one case where they are not totally rigid, namely in tcSimplifyIPs
+-- let ?x = e in ...
+-- Here, the given is (?x::a), where 'a' is not necy a rigid type
+-- But that doesn't affect the comparison, which is based only on mame.
+
+-- Note [RedStack]
+-- The red_stack pair (n,insts) pair is just used for error reporting.
+-- 'n' is always the depth of the stack.
+-- The 'insts' is the stack of Insts being reduced: to produce X
+-- I had to produce Y, to produce Y I had to produce Z, and so on.
+
+
+mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
+mkRedEnv doc try_me givens
+ = RedEnv { red_doc = doc, red_try_me = try_me,
+ red_givens = givens,
+ red_stack = (0,[]),
+ red_improve = True }
+
+mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
+-- Do not do improvement; no givens
+mkNoImproveRedEnv doc try_me
+ = RedEnv { red_doc = doc, red_try_me = try_me,
+ red_givens = [],
+ red_stack = (0,[]),
+ red_improve = True }
+
data WhatToDo
= ReduceMe WantSCs -- Try to reduce this
- -- If there's no instance, behave exactly like
- -- DontReduce: add the inst to the irreductible ones,
- -- but don't produce an error message of any kind.
+ -- If there's no instance, add the inst to the
+ -- irreductible ones, but don't produce an error
+ -- message of any kind.
-- It might be quite legitimate such as (Eq a)!
- | DontReduceUnlessConstant -- Return as irreducible unless it can
- -- be reduced to a constant in one step
-
- | Free -- Return as free
-
-reduceMe :: Inst -> WhatToDo
-reduceMe inst = ReduceMe AddSCs
+ | Stop -- Return as irreducible unless it can
+ -- be reduced to a constant in one step
+ -- Do not add superclasses; see
data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
-- of a predicate when adding it to the avails
-- The reason for this flag is entirely the super-class loop problem
-- Note [SUPER-CLASS LOOP 1]
-\end{code}
-
-
-
-\begin{code}
-type Avails = FiniteMap Inst Avail
-emptyAvails = emptyFM
-
-data Avail
- = IsFree -- Used for free Insts
- | Irred -- Used for irreducible dictionaries,
- -- which are going to be lambda bound
-
- | 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)
-
- | Rhs -- Used when there is a RHS
- (LHsExpr TcId) -- The RHS
- [Inst] -- Insts free in the RHS; we need these too
-
- | 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 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 bindings do *not* come back sorted in dependency order.
-We assume that they'll be wrapped in a big Rec, so that the
-dependency analyser can sort them out later
-The loop startes
-\begin{code}
-extractResults :: Avails
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds, -- Bindings
- [Inst], -- Irreducible ones
- [Inst]) -- Free ones
-
-extractResults avails wanteds
- = go avails emptyBag [] [] wanteds
- where
- go avails binds irreds frees []
- = returnM (binds, irreds, frees)
-
- go avails binds irreds frees (w:ws)
- = case lookupFM avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- 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 (Given id _) -> go avails new_binds irreds frees ws
- where
- 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 (add_given avails w) new_binds irreds frees (ws' ++ ws)
- where
- 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 = addToFM avails w (Given (instToId w) True)
-
- 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 :: 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)
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env
+ = do { givens' <- mapM zonkInst (red_givens env)
+ ; return $ env {red_givens = givens'}
+ }
\end{code}
%* *
%************************************************************************
-When the "what to do" predicate doesn't depend on the quantified type variables,
-matters are easier. We don't need to do any zonking, unless the improvement step
-does something, in which case we zonk before iterating.
-
-The "given" set is always empty.
-
-\begin{code}
-simpleReduceLoop :: SDoc
- -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
- -> [Inst] -- Wanted
- -> TcM ([Inst], -- Free
- TcDictBinds,
- [Inst]) -- Irreducible
-
-simpleReduceLoop doc try_me wanteds
- = mappM zonkInst wanteds `thenM` \ wanteds' ->
- reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
- if no_improvement then
- returnM (frees, binds, irreds)
- else
- simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
- returnM (frees1, binds `unionBags` binds1, irreds1)
-\end{code}
+Note [Ancestor Equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+During context reduction, we add to the wanted equalities also those
+equalities that (transitively) occur in superclass contexts of wanted
+class constraints. Consider the following code
+ class a ~ Int => C a
+ instance C Int
+If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
+substituting Int for a. Hence, we ultimately want (C Int), which we
+discharge with the explicit instance.
\begin{code}
-reduceContext :: SDoc
- -> (Inst -> WhatToDo)
- -> [Inst] -- Given
+reduceContext :: RedEnv
-> [Inst] -- Wanted
- -> TcM (Bool, -- True <=> improve step did no unification
- [Inst], -- Free
- TcDictBinds, -- Dictionary bindings
- [Inst]) -- Irreducible
-
-reduceContext doc try_me givens wanteds
- =
- traceTc (text "reduceContext" <+> (vcat [
- text "----------------------",
- doc,
- text "given" <+> ppr givens,
- text "wanted" <+> ppr wanteds,
- text "----------------------"
- ])) `thenM_`
-
- -- Build the Avail mapping from "givens"
- foldlM addGiven emptyAvails givens `thenM` \ init_state ->
-
- -- Do the real work
- 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 `thenM` \ no_improvement ->
-
- extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
-
- traceTc (text "reduceContext end" <+> (vcat [
- text "----------------------",
- doc,
- text "given" <+> ppr givens,
- text "wanted" <+> ppr wanteds,
- text "----",
- text "avails" <+> pprAvails avails,
- text "frees" <+> ppr frees,
- text "no_improvement =" <+> ppr no_improvement,
- text "----------------------"
- ])) `thenM_`
-
- returnM (no_improvement, frees, binds, irreds)
+ -> TcM (ImprovementDone,
+ TcDictBinds, -- Dictionary bindings
+ [Inst], -- Irreducible
+ TcM ()) -- Undo skolems from SkolemOccurs
--- reduceContextWithoutImprovement differs from reduceContext
--- (a) no improvement
--- (b) 'givens' is assumed empty
-reduceContextWithoutImprovement doc try_me wanteds
- =
- traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
+reduceContext env wanteds
+ = do { traceTc (text "reduceContext" <+> (vcat [
text "----------------------",
- doc,
+ red_doc env,
+ text "given" <+> ppr (red_givens env),
text "wanted" <+> ppr wanteds,
text "----------------------"
- ])) `thenM_`
-
- -- Do the real work
- reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
- extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
-
- traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
+ ]))
+
+
+ ; let givens = red_givens env
+ (given_eqs0, given_dicts0) = partition isEqInst givens
+ (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds
+ (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs
+
+ -- We want to add as wanted equalities those that (transitively)
+ -- occur in superclass contexts of wanted class constraints.
+ -- See Note [Ancestor Equalities]
+ ; ancestor_eqs <- ancestorEqualities wanted_dicts
+ ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
+ ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
+
+ -- 1. Normalise the *given* *equality* constraints
+ ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
+
+ -- 2. Normalise the *given* *dictionary* constraints
+ -- wrt. the toplevel and given equations
+ ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
+ given_dicts0
+
+ -- 5. Build the Avail mapping from "given_dicts"
+ ; (init_state, _) <- getLIE $ do
+ { init_state <- foldlM addGiven emptyAvails given_dicts
+ ; return init_state
+ }
+
+ -- !!! ToDo: what to do with the "extra_givens"? For the
+ -- moment I'm simply discarding them, which is probably wrong
+
+ -- 6. Solve the *wanted* *dictionary* constraints (not implications)
+ -- This may expose some further equational constraints...
+ ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+ ; (dict_binds, bound_dicts, dict_irreds)
+ <- extractResults avails wanted_dicts
+ ; traceTc $ text "reduceContext extractresults" <+> vcat
+ [ppr avails, ppr wanted_dicts, ppr dict_binds]
+
+ -- Solve the wanted *implications*. In doing so, we can provide
+ -- as "given" all the dicts that were originally given,
+ -- *or* for which we now have bindings,
+ -- *or* which are now irreds
+ ; let implic_env = env { red_givens = givens ++ bound_dicts
+ ++ dict_irreds }
+ ; (implic_binds_s, implic_irreds_s)
+ <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0
+ ; let implic_binds = unionManyBags implic_binds_s
+ implic_irreds = concat implic_irreds_s
+
+ -- Normalise the wanted equality constraints
+ ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs)
+
+ -- Normalise the wanted dictionaries
+ ; let irreds = dict_irreds ++ implic_irreds
+ eqs = eq_irreds ++ given_eqs
+ ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds
+
+ -- Figure out whether we should go round again. We do so in either
+ -- two cases:
+ -- (1) If any of the mutable tyvars in givens or irreds has been
+ -- filled in by improvement, there is merit in going around
+ -- again, because we may make further progress.
+ -- (2) If we managed to normalise any dicts, there is merit in going
+ -- around gain, because reduceList may be able to get further.
+ --
+ -- ToDo: We may have exposed new
+ -- equality constraints and should probably go round again
+ -- then as well. But currently we are dropping them on the
+ -- floor anyway.
+
+ ; let all_irreds = norm_irreds ++ eq_irreds
+ ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $
+ tyVarsOfInsts (givens ++ all_irreds)
+ ; let improvedDicts = not $ isEmptyBag normalise_binds
+ improved = improvedMetaTy || improvedDicts
+
+ -- The old plan (fragile)
+ -- improveed = availsImproved avails
+ -- || (not $ isEmptyBag normalise_binds1)
+ -- || (not $ isEmptyBag normalise_binds2)
+ -- || (any isEqInst irreds)
+
+ ; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
- doc,
+ red_doc env,
+ text "given" <+> ppr givens,
+ text "given_eqs" <+> ppr given_eqs,
text "wanted" <+> ppr wanteds,
+ text "wanted_dicts" <+> ppr wanted_dicts,
text "----",
text "avails" <+> pprAvails avails,
- text "frees" <+> ppr frees,
+ text "improved =" <+> ppr improved,
+ text "(all) irreds = " <+> ppr all_irreds,
+ text "dict-binds = " <+> ppr dict_binds,
+ text "implic-binds = " <+> ppr implic_binds,
text "----------------------"
- ])) `thenM_`
-
- returnM (frees, binds, irreds)
-
-tcImprove :: Avails -> TcM Bool -- False <=> no change
--- Perform improvement using all the predicates in Avails
-tcImprove avails
- = tcGetInstEnvs `thenM` \ inst_envs ->
- let
- preds = [ (pred, pp_loc)
- | (inst, avail) <- fmToList avails,
- pred <- get_preds inst avail,
- let pp_loc = pprInstLoc (instLoc inst)
- ]
+ ]))
+
+ ; return (improved,
+ given_binds `unionBags` normalise_binds
+ `unionBags` dict_binds
+ `unionBags` implic_binds,
+ all_irreds,
+ eliminate_skolems)
+ }
+
+tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
+tcImproveOne avails inst
+ | not (isDict inst) = return False
+ | otherwise
+ = do { inst_envs <- tcGetInstEnvs
+ ; let eqns = improveOne (classInstances inst_envs)
+ (dictPred inst, pprInstArising inst)
+ [ (dictPred p, pprInstArising p)
+ | p <- availsInsts avails, isDict p ]
-- 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
-
- -- For free Methods, we want to take predicates from their context,
- -- but for Methods that have been squished their context will already
- -- be in Avails, and we don't want duplicates. Hence this rather
- -- horrid get_preds function
- get_preds inst IsFree = fdPredsOfInst inst
- get_preds inst other | isDict inst = [dictPred inst]
- | otherwise = []
-
- eqns = improve get_insts preds
- get_insts clas = classInstances inst_envs clas
- in
- if null eqns then
- returnM True
- else
- traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
- mappM_ unify eqns `thenM_`
- returnM False
+ ; traceTc (text "improveOne" <+> ppr inst)
+ ; unifyEqns eqns }
+
+unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))]
+ -> TcM ImprovementDone
+unifyEqns [] = return False
+unifyEqns eqns
+ = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
+ ; mapM_ unify eqns
+ ; return True }
where
unify ((qtvs, pairs), what1, what2)
- = addErrCtxtM (mkEqnMsg what1 what2) $
- tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
- mapM_ (unif_pr tenv) pairs
+ = addErrCtxtM (mkEqnMsg what1 what2) $ do
+ (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+ mapM_ (unif_pr tenv) pairs
unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
+pprEquationDoc (eqn, (p1, _), (p2, _)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+ -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
= do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
- ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
+ ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
; return (tidy_env, msg) }
The main context-reduction function is @reduce@. Here's its game plan.
\begin{code}
-reduceList :: (Int,[Inst]) -- Stack (for err msgs)
- -- along with its depth
- -> (Inst -> WhatToDo)
- -> [Inst]
- -> Avails
- -> TcM Avails
-\end{code}
-
-@reduce@ is passed
- try_me: given an inst, this function returns
- Reduce reduce this
- DontReduce return this in "irreds"
- Free return this in "frees"
-
- wanteds: The list of insts to reduce
- state: An accumulating parameter of type Avails
- that contains the state of the algorithm
-
- It returns a Avails.
-
-The (n,stack) pair is just used for error reporting.
-n is always the depth of the stack.
-The stack is the stack of Insts being reduced: to produce X
-I had to produce Y, to produce Y I had to produce Z, and so on.
-
-\begin{code}
-reduceList (n,stack) try_me wanteds state
- | n > opt_MaxContextReductionDepth
- = failWithTc (reduceDepthErr n stack)
-
- | otherwise
- =
-#ifdef DEBUG
- (if n > 8 then
- pprTrace "Interesting! Context reduction stack deeper than 8:"
- (int n $$ ifPprDebug (nest 2 (pprStack stack)))
- else (\x->x))
-#endif
- go wanteds state
+reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
+reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
+ = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
+ ; dopts <- getDOpts
+ ; when (debugIsOn && (n > 8)) $ do
+ debugDumpTcRn (hang (ptext (sLit "Interesting! Context reduction stack depth") <+> int n)
+ 2 (ifPprDebug (nest 2 (pprStack stk))))
+ ; if n >= ctxtStkDepth dopts then
+ failWithTc (reduceDepthErr n stk)
+ else
+ go wanteds state }
where
- go [] state = returnM state
- go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
- go ws state'
+ go [] state = return state
+ go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
+ ; go ws state' }
-- Base case: we're done!
-reduce stack try_me wanted avails
+reduce :: RedEnv -> Inst -> Avails -> TcM Avails
+reduce env wanted avails
-- It's the same as an existing inst, or a superclass thereof
- | 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
+ | Just _ <- findAvail avails wanted
+ = do { traceTc (text "reduce: found " <+> ppr wanted)
+ ; return avails
+ }
| otherwise
- = case try_me wanted of {
-
- ; 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 (addIrred AddSCs) -- Assume want superclasses
-
- ; Free -> -- It's free so just chuck it upstairs
- -- First, see if the inst can be reduced to a constant in one step
- try_simple addFree
-
- ; ReduceMe want_scs -> -- It should be reduced
- lookupInst wanted `thenM` \ lookup_result ->
- case lookup_result of
- GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
- reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
- addWanted want_scs avails2 wanted rhs wanteds'
- -- Experiment with temporarily doing addIrred *before* the reduceList,
+ = do { traceTc (text "reduce" <+> ppr wanted $$ ppr avails)
+ ; case red_try_me env wanted of {
+ Stop -> try_simple (addIrred NoSCs);
+ -- See Note [No superclasses for Stop]
+
+ ReduceMe want_scs -> do -- It should be reduced
+ { (avails, lookup_result) <- reduceInst env avails wanted
+ ; case lookup_result of
+ NoInstance -> addIrred want_scs avails wanted
+ -- Add it and its superclasses
+
+ GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+
+ GenInst wanteds' rhs
+ -> do { avails1 <- addIrred NoSCs avails wanted
+ ; avails2 <- reduceList env wanteds' avails1
+ ; addWanted want_scs avails2 wanted rhs wanteds' } }
+ -- Temporarily do 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
+ -- superclasses too, and that 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 want_scs avails wanted rhs []
-
- NoInstance -> -- No such instance!
- -- Add it and its superclasses
- addIrred want_scs avails wanted
- }
+ } }
where
+ -- First, see if the inst can be reduced to a constant in one step
+ -- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
+ -- Don't bother for implication constraints, which take real work
try_simple do_this_otherwise
- = lookupInst wanted `thenM` \ lookup_result ->
- case lookup_result of
- SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
- other -> do_this_otherwise avails wanted
+ = do { res <- lookupSimpleInst wanted
+ ; case res of
+ GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
+ _ -> do_this_otherwise avails wanted }
\end{code}
-\begin{code}
--------------------------
-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 :: 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!
- --
- -- 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.
- --
-addFree avails free = returnM (addToFM avails free IsFree)
-
-addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
-addWanted want_scs avails wanted rhs_expr wanteds
- = addAvailAndSCs want_scs avails wanted avail
- where
- avail = Rhs rhs_expr wanteds
-
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
- -- Always add superclasses for 'givens'
- --
- -- 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 want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
- addAvailAndSCs want_scs avails irred Irred
-
-addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
-addAvailAndSCs want_scs avails inst avail
- | not (isClassDict inst) = return avails_with_inst
- | NoSCs <- want_scs = return avails_with_inst
- | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
- ; addSCs is_loop avails_with_inst inst }
- where
- avails_with_inst = addToFM avails inst avail
-
- is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
- -- Note: this compares by *type*, not by Unique
- deps = findAllDeps (unitVarSet (instToId inst)) avail
- dep_tys = map idType (varSetElems deps)
-
- findAllDeps :: IdSet -> Avail -> IdSet
- -- Find all the Insts that this one depends on
- -- See Note [SUPERCLASS-LOOP 2]
- -- 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 find_all so_far kids
- findAllDeps so_far other = so_far
-
- find_all :: IdSet -> Inst -> IdSet
- find_all so_far kid
- | kid_id `elemVarSet` so_far = so_far
- | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
- | otherwise = so_far'
- where
- so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
- kid_id = instToId kid
-
-addSCs :: (TcPredType -> 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.
-
-addSCs is_loop avails dict
- = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
- ; 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 (zipTopTvSubst tyvars tys) sc_theta
-
- add_sc avails (sc_dict, sc_sel)
- | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
- | is_given sc_dict = return avails
- | otherwise = addSCs is_loop avails' sc_dict
- where
- sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
- avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
-
- is_given :: Inst -> Bool
- is_given sc_dict = case lookupFM avails sc_dict of
- Just (Given _ _) -> True -- Given is cheaper than superclass selection
- other -> False
-\end{code}
-
Note [SUPERCLASS-LOOP 2]
~~~~~~~~~~~~~~~~~~~~~~~~
But the above isn't enough. Suppose we are *given* d1:Ord a,
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
+simplifier got two bites a the cherry... so something seemed to be an Stop
first time, but reducible next time.
Now we implement the Right Solution, which is to check for loops directly
%************************************************************************
%* *
+ Reducing a single constraint
+%* *
+%************************************************************************
+
+\begin{code}
+---------------------------------------------
+reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
+reduceInst _ avails other_inst
+ = do { result <- lookupSimpleInst other_inst
+ ; return (avails, result) }
+\end{code}
+
+Note [Equational Constraints in Implication Constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+An implication constraint is of the form
+ Given => Wanted
+where Given and Wanted may contain both equational and dictionary
+constraints. The delay and reduction of these two kinds of constraints
+is distinct:
+
+-) In the generated code, wanted Dictionary constraints are wrapped up in an
+ implication constraint that is created at the code site where the wanted
+ dictionaries can be reduced via a let-binding. This let-bound implication
+ constraint is deconstructed at the use-site of the wanted dictionaries.
+
+-) While the reduction of equational constraints is also delayed, the delay
+ is not manifest in the generated code. The required evidence is generated
+ in the code directly at the use-site. There is no let-binding and deconstruction
+ necessary. The main disadvantage is that we cannot exploit sharing as the
+ same evidence may be generated at multiple use-sites. However, this disadvantage
+ is limited because it only concerns coercions which are erased.
+
+The different treatment is motivated by the different in representation. Dictionary
+constraints require manifest runtime dictionaries, while equations require coercions
+which are types.
+
+\begin{code}
+---------------------------------------------
+reduceImplication :: RedEnv
+ -> Inst
+ -> TcM (TcDictBinds, [Inst])
+\end{code}
+
+Suppose we are simplifying the constraint
+ forall bs. extras => wanted
+in the context of an overall simplification problem with givens 'givens'.
+
+Note that
+ * The 'givens' need not mention any of the quantified type variables
+ e.g. forall {}. Eq a => Eq [a]
+ forall {}. C Int => D (Tree Int)
+
+ This happens when you have something like
+ data T a where
+ T1 :: Eq a => a -> T a
+
+ f :: T a -> Int
+ f x = ...(case x of { T1 v -> v==v })...
+
+\begin{code}
+ -- ToDo: should we instantiate tvs? I think it's not necessary
+ --
+ -- Note on coercion variables:
+ --
+ -- The extra given coercion variables are bound at two different sites:
+ -- -) in the creation context of the implication constraint
+ -- the solved equational constraints use these binders
+ --
+ -- -) at the solving site of the implication constraint
+ -- the solved dictionaries use these binders
+ -- these binders are generated by reduceImplication
+ --
+reduceImplication env
+ orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
+ tci_tyvars = tvs,
+ tci_given = extra_givens, tci_wanted = wanteds })
+ = do { -- Solve the sub-problem
+ ; let try_me _ = ReduceMe AddSCs -- Note [Freeness and implications]
+ env' = env { red_givens = extra_givens ++ red_givens env
+ , red_doc = sep [ptext (sLit "reduceImplication for")
+ <+> ppr name,
+ nest 2 (parens $ ptext (sLit "within")
+ <+> red_doc env)]
+ , red_try_me = try_me }
+
+ ; traceTc (text "reduceImplication" <+> vcat
+ [ ppr (red_givens env), ppr extra_givens,
+ ppr wanteds])
+ ; (irreds, binds) <- checkLoop env' wanteds
+ ; let (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
+ -- SLPJ Sept 07: I think this is bogus; currently
+ -- there are no Eqinsts in extra_givens
+ dict_ids = map instToId extra_dict_givens
+
+ -- Note [Reducing implication constraints]
+ -- Tom -- update note, put somewhere!
+
+ ; traceTc (text "reduceImplication result" <+> vcat
+ [ppr irreds, ppr binds])
+
+ ; -- extract superclass binds
+ -- (sc_binds,_) <- extractResults avails []
+-- ; traceTc (text "reduceImplication sc_binds" <+> vcat
+-- [ppr sc_binds, ppr avails])
+--
+
+ -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
+ -- Then we must iterate the outer loop too!
+
+ ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
+
+-- Progress is no longer measered by the number of bindings
+ ; if (isEmptyLHsBinds binds) && (not $ null irreds) then -- No progress
+ -- If there are any irreds, we back off and do nothing
+ return (emptyBag, [orig_implic])
+ else do
+ { (simpler_implic_insts, bind)
+ <- makeImplicationBind inst_loc tvs extra_givens irreds
+ -- This binding is useless if the recursive simplification
+ -- made no progress; but currently we don't try to optimise that
+ -- case. After all, we only try hard to reduce at top level, or
+ -- when inferring types.
+
+ ; let dict_wanteds = filter (not . isEqInst) wanteds
+ -- TOMDO: given equational constraints bug!
+ -- we need a different evidence for given
+ -- equations depending on whether we solve
+ -- dictionary constraints or equational constraints
+
+ eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
+ -- SLPJ Sept07: this looks Utterly Wrong to me, but I think
+ -- that current extra_givens has no EqInsts, so
+ -- it makes no difference
+ co = wrap_inline -- Note [Always inline implication constraints]
+ <.> mkWpTyLams tvs
+ <.> mkWpLams eq_tyvars
+ <.> mkWpLams dict_ids
+ <.> WpLet (binds `unionBags` bind)
+ wrap_inline | null dict_ids = idHsWrapper
+ | otherwise = WpInline
+ rhs = mkLHsWrap co payload
+ loc = instLocSpan inst_loc
+ payload = mkBigLHsTup (map (L loc . HsVar . instToId) dict_wanteds)
+
+
+ ; traceTc (vcat [text "reduceImplication" <+> ppr name,
+ ppr simpler_implic_insts,
+ text "->" <+> ppr rhs])
+ ; return (unitBag (L loc (VarBind (instToId orig_implic) rhs)),
+ simpler_implic_insts)
+ }
+ }
+reduceImplication _ i = pprPanic "reduceImplication" (ppr i)
+\end{code}
+
+Note [Always inline implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose an implication constraint floats out of an INLINE function.
+Then although the implication has a single call site, it won't be
+inlined. And that is bad because it means that even if there is really
+*no* overloading (type signatures specify the exact types) there will
+still be dictionary passing in the resulting code. To avert this,
+we mark the implication constraints themselves as INLINE, at least when
+there is no loss of sharing as a result.
+
+Note [Freeness and implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's hard to say when an implication constraint can be floated out. Consider
+ forall {} Eq a => Foo [a]
+The (Foo [a]) doesn't mention any of the quantified variables, but it
+still might be partially satisfied by the (Eq a).
+
+There is a useful special case when it *is* easy to partition the
+constraints, namely when there are no 'givens'. Consider
+ forall {a}. () => Bar b
+There are no 'givens', and so there is no reason to capture (Bar b).
+We can let it float out. But if there is even one constraint we
+must be much more careful:
+ forall {a}. C a b => Bar (m b)
+because (C a b) might have a superclass (D b), from which we might
+deduce (Bar [b]) when m later gets instantiated to []. Ha!
+
+Here is an even more exotic example
+ class C a => D a b
+Now consider the constraint
+ forall b. D Int b => C Int
+We can satisfy the (C Int) from the superclass of D, so we don't want
+to float the (C Int) out, even though it mentions no type variable in
+the constraints!
+
+One more example: the constraint
+ class C a => D a b
+ instance (C a, E c) => E (a,c)
+
+ constraint: forall b. D Int b => E (Int,c)
+
+You might think that the (D Int b) can't possibly contribute
+to solving (E (Int,c)), since the latter mentions 'c'. But
+in fact it can, because solving the (E (Int,c)) constraint needs
+dictionaries
+ C Int, E c
+and the (C Int) can be satisfied from the superclass of (D Int b).
+So we must still not float (E (Int,c)) out.
+
+To think about: special cases for unary type classes?
+
+Note [Pruning the givens in an implication constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are about to form the implication constraint
+ forall tvs. Eq a => Ord b
+The (Eq a) cannot contribute to the (Ord b), because it has no access to
+the type variable 'b'. So we could filter out the (Eq a) from the givens.
+But BE CAREFUL of the examples above in [Freeness and implications].
+
+Doing so would be a bit tidier, but all the implication constraints get
+simplified away by the optimiser, so it's no great win. So I don't take
+advantage of that at the moment.
+
+If you do, BE CAREFUL of wobbly type variables.
+
+
+%************************************************************************
+%* *
+ Avails and AvailHow: the pool of evidence
+%* *
+%************************************************************************
+
+
+\begin{code}
+data Avails = Avails !ImprovementDone !AvailEnv
+
+type ImprovementDone = Bool -- True <=> some unification has happened
+ -- so some Irreds might now be reducible
+ -- keys that are now
+
+type AvailEnv = FiniteMap Inst AvailHow
+data AvailHow
+ = IsIrred -- Used for irreducible dictionaries,
+ -- which are going to be lambda bound
+
+ | Given Inst -- Used for dictionaries for which we have a binding
+ -- e.g. those "given" in a signature
+
+ | Rhs -- Used when there is a RHS
+ (LHsExpr TcId) -- The RHS
+ [Inst] -- Insts free in the RHS; we need these too
+
+instance Outputable Avails where
+ ppr = pprAvails
+
+pprAvails :: Avails -> SDoc
+pprAvails (Avails imp avails)
+ = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
+ , nest 2 $ braces $
+ vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)]
+ | (inst,avail) <- fmToList avails ]]
+
+instance Outputable AvailHow where
+ ppr = pprAvail
+
+-------------------------
+pprAvail :: AvailHow -> SDoc
+pprAvail IsIrred = text "Irred"
+pprAvail (Given x) = text "Given" <+> ppr x
+pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs,
+ nest 2 (ppr rhs)]
+
+-------------------------
+extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
+extendAvailEnv env inst avail = addToFM env inst avail
+
+findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow
+findAvailEnv env wanted = lookupFM env wanted
+ -- NB 1: the Ord instance of Inst compares by the class/type info
+ -- *not* by unique. So
+ -- d1::C Int == d2::C Int
+
+emptyAvails :: Avails
+emptyAvails = Avails False emptyFM
+
+findAvail :: Avails -> Inst -> Maybe AvailHow
+findAvail (Avails _ avails) wanted = findAvailEnv avails wanted
+
+elemAvails :: Inst -> Avails -> Bool
+elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
+
+extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
+-- Does improvement
+extendAvails avails@(Avails imp env) inst avail
+ = do { imp1 <- tcImproveOne avails inst -- Do any improvement
+ ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
+
+availsInsts :: Avails -> [Inst]
+availsInsts (Avails _ avails) = keysFM avails
+
+_availsImproved :: Avails -> ImprovementDone
+_availsImproved (Avails imp _) = imp
+\end{code}
+
+Extracting the bindings from a bunch of Avails.
+The bindings do *not* come back sorted in dependency order.
+We assume that they'll be wrapped in a big Rec, so that the
+dependency analyser can sort them out later
+
+\begin{code}
+type DoneEnv = FiniteMap Inst [Id]
+-- Tracks which things we have evidence for
+
+extractResults :: Avails
+ -> [Inst] -- Wanted
+ -> TcM (TcDictBinds, -- Bindings
+ [Inst], -- The insts bound by the bindings
+ [Inst]) -- Irreducible ones
+ -- Note [Reducing implication constraints]
+
+extractResults (Avails _ avails) wanteds
+ = go emptyBag [] [] emptyFM wanteds
+ where
+ go :: TcDictBinds -- Bindings for dicts
+ -> [Inst] -- Bound by the bindings
+ -> [Inst] -- Irreds
+ -> DoneEnv -- Has an entry for each inst in the above three sets
+ -> [Inst] -- Wanted
+ -> TcM (TcDictBinds, [Inst], [Inst])
+ go binds bound_dicts irreds _ []
+ = return (binds, bound_dicts, irreds)
+
+ go binds bound_dicts irreds done (w:ws)
+ | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
+ = if w_id `elem` done_ids then
+ go binds bound_dicts irreds done ws
+ else
+ go (add_bind (nlHsVar done_id)) bound_dicts irreds
+ (addToFM done w (done_id : w_id : rest_done_ids)) ws
+
+ | otherwise -- Not yet done
+ = case findAvailEnv avails w of
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go binds bound_dicts irreds done ws
+
+ Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
+
+ Just (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
+
+ Just (Given g) -> go binds' bound_dicts irreds (addToFM done w [g_id]) ws
+ where
+ g_id = instToId g
+ binds' | w_id == g_id = binds
+ | otherwise = add_bind (nlHsVar g_id)
+ where
+ w_id = instToId w
+ done' = addToFM done w [w_id]
+ add_bind rhs = addInstToDictBind binds w rhs
+\end{code}
+
+
+Note [No superclasses for Stop]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
+add it to avails, so that any other equal Insts will be commoned up
+right here. However, we 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.
+
+\begin{code}
+addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
+addWanted want_scs avails wanted rhs_expr wanteds
+ = addAvailAndSCs want_scs avails wanted avail
+ where
+ avail = Rhs rhs_expr wanteds
+
+addGiven :: Avails -> Inst -> TcM Avails
+addGiven avails given = addAvailAndSCs AddSCs avails given (Given given)
+ -- Always add superclasses for 'givens'
+ --
+ -- No ASSERT( not (given `elemAvails` 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
+\end{code}
+
+\begin{code}
+addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
+addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
+ addAvailAndSCs want_scs avails irred IsIrred
+
+addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
+addAvailAndSCs want_scs avails inst avail
+ | not (isClassDict inst) = extendAvails avails inst avail
+ | NoSCs <- want_scs = extendAvails avails inst avail
+ | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
+ ; avails' <- extendAvails avails inst avail
+ ; addSCs is_loop avails' inst }
+ where
+ is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
+ -- Note: this compares by *type*, not by Unique
+ deps = findAllDeps (unitVarSet (instToVar inst)) avail
+ dep_tys = map idType (varSetElems deps)
+
+ findAllDeps :: IdSet -> AvailHow -> IdSet
+ -- Find all the Insts that this one depends on
+ -- See Note [SUPERCLASS-LOOP 2]
+ -- 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 find_all so_far kids
+ findAllDeps so_far _ = so_far
+
+ find_all :: IdSet -> Inst -> IdSet
+ find_all so_far kid
+ | isEqInst kid = so_far
+ | kid_id `elemVarSet` so_far = so_far
+ | Just avail <- findAvail avails kid = findAllDeps so_far' avail
+ | otherwise = so_far'
+ where
+ so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
+ kid_id = instToId kid
+
+addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
+ -- Add all the superclasses of the Inst to Avails
+ -- The first param says "don't do this because the original thing
+ -- depends on this one, so you'd build a loop"
+ -- Invariant: the Inst is already in Avails.
+
+addSCs is_loop avails dict
+ = ASSERT( isDict dict )
+ do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
+ ; 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' = filter (not . isEqPred) $
+ substTheta (zipTopTvSubst tyvars tys) sc_theta
+
+ add_sc avails (sc_dict, sc_sel)
+ | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
+ | is_given sc_dict = return avails
+ | otherwise = do { avails' <- extendAvails avails sc_dict (Rhs sc_sel_rhs [dict])
+ ; addSCs is_loop avails' sc_dict }
+ where
+ sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
+ co_fn = WpApp (instToVar dict) <.> mkWpTyApps tys
+
+ is_given :: Inst -> Bool
+ is_given sc_dict = case findAvail avails sc_dict of
+ Just (Given _) -> True -- Given is cheaper than superclass selection
+ _ -> False
+
+-- From the a set of insts obtain all equalities that (transitively) occur in
+-- superclass contexts of class constraints (aka the ancestor equalities).
+--
+ancestorEqualities :: [Inst] -> TcM [Inst]
+ancestorEqualities
+ = mapM mkWantedEqInst -- turn only equality predicates..
+ . filter isEqPred -- ..into wanted equality insts
+ . bagToList
+ . addAEsToBag emptyBag -- collect the superclass constraints..
+ . map dictPred -- ..of all predicates in a bag
+ . filter isClassDict
+ where
+ addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
+ addAEsToBag bag [] = bag
+ addAEsToBag bag (pred:preds)
+ | pred `elemBag` bag = addAEsToBag bag preds
+ | isEqPred pred = addAEsToBag bagWithPred preds
+ | isClassPred pred = addAEsToBag bagWithPred predsWithSCs
+ | otherwise = addAEsToBag bag preds
+ where
+ bagWithPred = bag `snocBag` pred
+ predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
+ --
+ (tyvars, sc_theta, _, _) = classBigSig clas
+ (clas, tys) = getClassPredTys pred
+\end{code}
+
+
+%************************************************************************
+%* *
\section{tcSimplifyTop: defaulting}
%* *
%************************************************************************
\begin{code}
tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
tcSimplifyTop wanteds
- = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
+ = tc_simplify_top doc False wanteds
where
doc = text "tcSimplifyTop"
tcSimplifyInteractive wanteds
- = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
+ = tc_simplify_top doc True wanteds
where
- doc = text "tcSimplifyTop"
+ doc = text "tcSimplifyInteractive"
-- The TcLclEnv should be valid here, solely to improve
-- error message generation for the monomorphism restriction
-tc_simplify_top doc is_interactive want_scs wanteds
- = do { lcl_env <- getLclEnv
- ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
-
- ; let try_me inst = ReduceMe want_scs
- ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
-
- ; let
- -- First get rid of implicit parameters
- (non_ips, bad_ips) = partition isClassDict irreds
-
- -- All the non-tv or multi-param ones are definite errors
- (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips
- bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
-
- -- Group by type variable
- tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts
-
- -- Pick the ones which its worth trying to disambiguate
- -- namely, the ones whose type variable isn't bound
- -- up with one of the non-tyvar classes
- (default_gps, non_default_gps) = partition defaultable_group tv_groups
- defaultable_group ds
- = not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
- && defaultable_classes (map get_clas ds)
- defaultable_classes clss
- | is_interactive = any isInteractiveClass clss
- | otherwise = all isStandardClass clss && any isNumericClass clss
-
- isInteractiveClass cls = isNumericClass cls
- || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
- -- In interactive mode, we default Show a to Show ()
- -- to avoid graututious errors on "show []"
-
-
- -- Collect together all the bad guys
- bad_guys = non_tvs ++ concat non_default_gps
- (ambigs, no_insts) = partition isTyVarDict bad_guys
- -- If the dict has no type constructors involved, it must be ambiguous,
- -- except I suppose that another error with fundeps maybe should have
- -- constrained those type variables
-
- -- Report definite errors
- ; ASSERT( null frees )
- groupErrs (addNoInstanceErrs Nothing []) no_insts
- ; strangeTopIPErrs bad_ips
-
- -- Deal with ambiguity errors, but only if
- -- if there has not been an error so far:
- -- errors often give rise to spurious ambiguous Insts.
- -- For example:
- -- f = (*) -- Monomorphic
- -- g :: Num a => a -> a
- -- g x = f x x
- -- Here, we get a complaint when checking the type signature for g,
- -- that g isn't polymorphic enough; but then we get another one when
- -- dealing with the (Num a) context arising from f's definition;
- -- we try to unify a with Int (to default it), but find that it's
- -- already been unified with the rigid variable from g's type sig
- ; binds_ambig <- ifErrsM (returnM []) $
- do { -- 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 ambigs
-
- -- Disambiguate the ones that look feasible
- ; mappM disambigGroup default_gps }
-
- ; return (binds `unionBags` unionManyBags binds_ambig) }
-
-----------------------------------
-d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
-
-is_unary_tyvar_dict :: Inst -> Bool -- Dicts of form (C a)
- -- Invariant: argument is a ClassDict, not IP or method
-is_unary_tyvar_dict d = case getDictClassTys d of
- (_, [ty]) -> tcIsTyVarTy ty
- other -> False
-
-get_tv d = case getDictClassTys d of
- (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
-get_clas d = case getDictClassTys d of
- (clas, _) -> clas
+tc_simplify_top :: SDoc -> Bool -> [Inst] -> TcM (Bag (LHsBind TcId))
+tc_simplify_top doc interactive wanteds
+ = do { dflags <- getDOpts
+ ; wanteds <- zonkInsts wanteds
+ ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
+
+ ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
+ ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
+-- ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
+ ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
+ ; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1
+ ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
+
+ -- Use the defaulting rules to do extra unification
+ -- NB: irreds2 are already zonked
+ ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
+
+ -- Deal with implicit parameters
+ ; let (bad_ips, non_ips) = partition isIPDict irreds3
+ (ambigs, others) = partition isTyVarDict non_ips
+
+ ; topIPErrs bad_ips -- Can arise from f :: Int -> Int
+ -- f x = x + ?y
+ ; addNoInstanceErrs others
+ ; addTopAmbigErrs ambigs
+
+ ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
+ where
+ doc1 = doc <+> ptext (sLit "(first round)")
+ doc2 = doc <+> ptext (sLit "(approximate)")
+ doc3 = doc <+> ptext (sLit "(disambiguate)")
\end{code}
If a dictionary constrains a type variable which is
@void@.
\begin{code}
-disambigGroup :: [Inst] -- All standard classes of form (C a)
- -> TcM TcDictBinds
+disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
+ -- Just does unification to fix the default types
+ -- The Insts are assumed to be pre-zonked
+disambiguate doc interactive dflags insts
+ | null insts
+ = return (insts, emptyBag)
-disambigGroup dicts
- = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
- -- SO, TRY DEFAULT TYPES IN ORDER
-
- -- Failure here is caused by there being no type in the
- -- 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.
- get_default_tys `thenM` \ default_tys ->
- let
- try_default [] -- No defaults work, so fail
- = failM
-
- try_default (default_ty : default_tys)
- = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
- -- default_tys instead
- tcSimplifyDefault theta `thenM` \ _ ->
- returnM default_ty
- where
- theta = [mkClassPred clas [default_ty] | clas <- classes]
- in
- -- 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
- where
- tyvar = get_tv (head dicts) -- Should be non-empty
- classes = map get_clas dicts
-
- choose_default default_ty -- Commit to tyvar = default_ty
- = -- Bind the type variable
- unifyType 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
- ; checkWiredInTyCon doubleTyCon
- ; return [integer_ty, doubleTy] } }
-\end{code}
+ | null defaultable_groups
+ = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups])
+ ; return (insts, emptyBag) }
+
+ | otherwise
+ = do { -- Figure out what default types to use
+ default_tys <- getDefaultTys extended_defaulting ovl_strings
-[Aside - why the defaulting mechanism is turned off when
- dealing with arguments and results to ccalls.
+ ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ ; mapM_ (disambigGroup default_tys) defaultable_groups
-When typechecking _ccall_s, TcExpr ensures that the external
-function is only passed arguments (and in the other direction,
-results) of a restricted set of 'native' types.
+ -- disambigGroup does unification, hence try again
+ ; tryHardCheckLoop doc insts }
-The interaction between the defaulting mechanism for numeric
-values and CC & CR can be a bit puzzling to the user at times.
-For example,
+ where
+ extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
+ ovl_strings = dopt Opt_OverloadedStrings dflags
- x <- _ccall_ f
- if (x /= 0) then
- _ccall_ g x
- else
- return ()
+ unaries :: [(Inst, Class, TcTyVar)] -- (C tv) constraints
+ bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
+ (unaries, bad_tvs_s) = partitionWith find_unary insts
+ bad_tvs = unionVarSets bad_tvs_s
-What type has 'x' got here? That depends on the default list
-in operation, if it is equal to Haskell 98's default-default
-of (Integer, Double), 'x' has type Double, since Integer
-is not an instance of CR. If the default list is equal to
-Haskell 1.4's default-default of (Int, Double), 'x' has type
-Int.
+ -- Finds unary type-class constraints
+ find_unary d@(Dict {tci_pred = ClassP cls [ty]})
+ | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
+ find_unary inst = Right (tyVarsOfInst inst)
-End of aside]
+ -- Group by type variable
+ defaultable_groups :: [[(Inst,Class,TcTyVar)]]
+ defaultable_groups = filter defaultable_group (equivClasses cmp_tv unaries)
+ cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
+
+ defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
+ defaultable_group ds@((_,_,tv):_)
+ = isTyConableTyVar tv -- Note [Avoiding spurious errors]
+ && not (tv `elemVarSet` bad_tvs)
+ && defaultable_classes [c | (_,c,_) <- ds]
+ defaultable_group [] = panic "defaultable_group"
+
+ defaultable_classes clss
+ | extended_defaulting = any isInteractiveClass clss
+ | otherwise = all is_std_class clss && (any is_num_class clss)
+
+ -- In interactive mode, or with -XExtendedDefaultRules,
+ -- we default Show a to Show () to avoid graututious errors on "show []"
+ isInteractiveClass cls
+ = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+
+ is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
+ -- is_num_class adds IsString to the standard numeric classes,
+ -- when -foverloaded-strings is enabled
+
+ is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
+ -- Similarly is_std_class
+
+-----------------------
+disambigGroup :: [Type] -- The default types
+ -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
+ -> TcM () -- Just does unification, to fix the default types
+
+disambigGroup default_tys dicts
+ = try_default default_tys
+ where
+ (_,_,tyvar) = ASSERT(not (null dicts)) head dicts -- Should be non-empty
+ classes = [c | (_,c,_) <- dicts]
+
+ try_default [] = return ()
+ try_default (default_ty : default_tys)
+ = tryTcLIE_ (try_default default_tys) $
+ do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
+ -- This may fail; then the tryTcLIE_ kicks in
+ -- Failure here is caused by there being no type in the
+ -- 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.
+
+ -- After this we can't fail
+ ; warnDefault dicts default_ty
+ ; unifyType default_ty (mkTyVarTy tyvar)
+ ; return () -- TOMDO: do something with the coercion
+ }
+
+
+-----------------------
+getDefaultTys :: Bool -> Bool -> TcM [Type]
+getDefaultTys extended_deflts ovl_strings
+ = do { mb_defaults <- getDeclaredDefaultTys
+ ; case mb_defaults of {
+ Just tys -> return tys ; -- User-supplied defaults
+ Nothing -> do
+
+ -- No use-supplied default
+ -- Use [Integer, Double], plus modifications
+ { integer_ty <- tcMetaTy integerTyConName
+ ; checkWiredInTyCon doubleTyCon
+ ; string_ty <- tcMetaTy stringTyConName
+ ; return (opt_deflt extended_deflts unitTy
+ -- Note [Default unitTy]
+ ++
+ [integer_ty,doubleTy]
+ ++
+ opt_deflt ovl_strings string_ty) } } }
+ where
+ opt_deflt True ty = [ty]
+ opt_deflt False _ = []
+\end{code}
+
+Note [Default unitTy]
+~~~~~~~~~~~~~~~~~~~~~
+In interative mode (or with -XExtendedDefaultRules) we add () as the first type we
+try when defaulting. This has very little real impact, except in the following case.
+Consider:
+ Text.Printf.printf "hello"
+This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't
+want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to
+default the 'a' to (), rather than to Integer (which is what would otherwise happen;
+and then GHCi doesn't attempt to print the (). So in interactive mode, we add
+() to the list of defaulting types. See Trac #1200.
+
+Note [Avoiding spurious errors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When doing the unification for defaulting, we check for skolem
+type variables, and simply don't default them. For example:
+ f = (*) -- Monomorphic
+ g :: Num a => a -> a
+ g x = f x x
+Here, we get a complaint when checking the type signature for g,
+that g isn't polymorphic enough; but then we get another one when
+dealing with the (Num a) context arising from f's definition;
+we try to unify a with Int (to default it), but find that it's
+already been unified with the rigid variable from g's type sig
%************************************************************************
instance declarations.
\begin{code}
-tcSimplifyDeriv :: TyCon
+tcSimplifyDeriv :: InstOrigin
-> [TyVar]
-> ThetaType -- Wanted
-> TcM ThetaType -- Needed
+-- Given instance (wanted) => C inst_ty
+-- Simplify 'wanted' as much as possible
-tcSimplifyDeriv tc tyvars theta
- = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
+tcSimplifyDeriv orig tyvars theta
+ = do { (tvs, _, tenv) <- tcInstTyVars tyvars
-- 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 DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
- simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
- ASSERT( null frees ) -- reduceMe never returns Free
-
- doptM Opt_GlasgowExts `thenM` \ gla_exts ->
- doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
- let
- tv_set = mkVarSet tvs
-
- (bad_insts, ok_insts) = partition is_bad_inst irreds
- is_bad_inst dict
- = let pred = dictPred dict -- reduceMe squashes all non-dicts
- in isEmptyVarSet (tyVarsOfPred pred)
- -- Things like (Eq T) are bad
- || (not gla_exts && not (isTyVarClassPred pred))
-
- simpl_theta = map dictPred ok_insts
- weird_preds = [pred | pred <- simpl_theta
- , not (tyVarsOfPred pred `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.
-
- rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
- -- This reverse-mapping is a Royal Pain,
- -- but the result should mention TyVars not TcTyVars
-
- head_ty = TyConApp tc (map TyVarTy tvs)
- in
-
- addNoInstanceErrs Nothing [] bad_insts `thenM_`
- mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
- checkAmbiguity tvs simpl_theta tv_set `thenM_`
- -- Check instance termination as for user-declared instances.
- -- unless we had -fallow-undecidable-instances (which risks
- -- non-termination in the 'deriving' context-inference fixpoint
- -- loop).
- ifM (gla_exts && not undecidable_ok)
- (checkInstTermination simpl_theta [head_ty]) `thenM_`
- returnM (substTheta rev_env simpl_theta)
+ ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
+ ; (irreds, _) <- tryHardCheckLoop doc wanteds
+
+ ; let (tv_dicts, others) = partition ok irreds
+ ; addNoInstanceErrs others
+ -- See Note [Exotic derived instance contexts] in TcMType
+
+ ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+ simpl_theta = substTheta rev_env (map dictPred tv_dicts)
+ -- This reverse-mapping is a pain, but the result
+ -- should mention the original TyVars not TcTyVars
+
+ ; return simpl_theta }
where
- doc = ptext SLIT("deriving classes for a data type")
+ doc = ptext (sLit "deriving classes for a data type")
+
+ ok dict | isDict dict = validDerivPred (dictPred dict)
+ | otherwise = False
\end{code}
+
@tcSimplifyDefault@ just checks class-type constraints, essentially;
used with \tr{default} declarations. We are only interested in
whether it worked or not.
tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
-> TcM ()
-tcSimplifyDefault theta
- = newDicts DefaultOrigin theta `thenM` \ wanteds ->
- simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
- ASSERT( null frees ) -- try_me never returns Free
- addNoInstanceErrs Nothing [] irreds `thenM_`
+tcSimplifyDefault theta = do
+ wanteds <- newDictBndrsO DefaultOrigin theta
+ (irreds, _) <- tryHardCheckLoop doc wanteds
+ addNoInstanceErrs irreds
if null irreds then
- returnM ()
- else
- failM
+ return ()
+ else
+ traceTc (ptext (sLit "tcSimplifyDefault failing")) >> failM
where
- doc = ptext SLIT("default declaration")
+ doc = ptext (sLit "default declaration")
\end{code}
-- Group together insts with the same origin
-- We want to report them together in error messages
-groupErrs report_err []
- = returnM ()
-groupErrs report_err (inst:insts)
- = do_one (inst:friends) `thenM_`
- groupErrs report_err others
-
+groupErrs _ []
+ = return ()
+groupErrs report_err (inst:insts)
+ = do { do_one (inst:friends)
+ ; groupErrs report_err 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,
-- 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)))
+addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs bndrs []
+addTopIPErrs _ []
= return ()
addTopIPErrs bndrs ips
- = addErrTcM (tidy_env, mk_msg tidy_ips)
+ = do { dflags <- getDOpts
+ ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
where
(tidy_env, tidy_ips) = tidyInsts ips
- mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
- nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
+ mk_msg dflags ips
+ = vcat [sep [ptext (sLit "Implicit parameters escape from"),
+ nest 2 (ptext (sLit "the monomorphic top-level binding")
+ <> plural bndrs <+> ptext (sLit "of")
<+> pprBinders bndrs <> colon)],
- nest 2 (vcat (map ppr_ip ips)),
- monomorphism_fix]
- ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
+ nest 2 (vcat (map ppr_ip ips)),
+ monomorphism_fix dflags]
+ ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
-strangeTopIPErrs :: [Inst] -> TcM ()
-strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
+topIPErrs :: [Inst] -> TcM ()
+topIPErrs 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") <>
+ mk_msg dicts = addInstLoc dicts (ptext (sLit "Unbound implicit parameter") <>
plural tidy_dicts <+> pprDictsTheta 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
+addNoInstanceErrs :: [Inst] -- Wanted (can include implications)
-> 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)
- 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 inst_envs clas tys of
- -- The case of exactly one match and no unifiers means
- -- a successful lookup. That can't happen here, becuase
- -- dicts only end up here if they didn't match in Inst.lookupInst
-#ifdef DEBUG
- ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
-#endif
- ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
- res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
- where
- (clas,tys) = getDictClassTys dict
- in
-
- -- Now generate a good message for the no-instance bunch
- mk_probable_fix tidy_env2 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") <+> pprDictsTheta no_inst_dicts
- | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
- nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
- in
- -- And emit both the non-instance and overlap messages
- addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
+addNoInstanceErrs insts
+ = do { let (tidy_env, tidy_insts) = tidyInsts insts
+ ; reportNoInstances tidy_env Nothing tidy_insts }
+
+reportNoInstances
+ :: TidyEnv
+ -> Maybe (InstLoc, [Inst]) -- Context
+ -- Nothing => top level
+ -- Just (d,g) => d describes the construct
+ -- with givens g
+ -> [Inst] -- What is wanted (can include implications)
+ -> TcM ()
+
+reportNoInstances tidy_env mb_what insts
+ = groupErrs (report_no_instances tidy_env mb_what) insts
+
+report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [Inst] -> TcM ()
+report_no_instances tidy_env mb_what insts
+ = do { inst_envs <- tcGetInstEnvs
+ ; let (implics, insts1) = partition isImplicInst insts
+ (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
+ (eqInsts, insts3) = partition isEqInst insts2
+ ; traceTc (text "reportNoInstances" <+> vcat
+ [ppr insts, ppr implics, ppr insts1, ppr insts2])
+ ; mapM_ complain_implic implics
+ ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
+ ; groupErrs complain_no_inst insts3
+ ; mapM_ (addErrTcM . mk_eq_err) eqInsts
+ }
where
+ complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
+
+ complain_implic inst -- Recurse!
+ = reportNoInstances tidy_env
+ (Just (tci_loc inst, tci_given inst))
+ (tci_wanted inst)
+
+ check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
+ -- Right msg => overlap message
+ -- Left inst => no instance
+ check_overlap inst_envs wanted
+ | not (isClassDict wanted) = Left wanted
+ | otherwise
+ = case lookupInstEnv inst_envs clas tys of
+ ([], _) -> Left wanted -- No match
+ -- The case of exactly one match and no unifiers means a
+ -- successful lookup. That can't happen here, because dicts
+ -- only end up here if they didn't match in Inst.lookupInst
+ ([_],[])
+ | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
+ res -> Right (mk_overlap_msg wanted res)
+ where
+ (clas,tys) = getDictClassTys wanted
+
mk_overlap_msg dict (matches, unifiers)
- = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
+ = ASSERT( not (null matches) )
+ vcat [ addInstLoc [dict] ((ptext (sLit "Overlapping instances for")
<+> pprPred (dictPred dict))),
- sep [ptext SLIT("Matching instances") <> colon,
+ sep [ptext (sLit "Matching instances") <> colon,
nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
- ASSERT( not (null matches) )
if not (isSingleton matches)
then -- Two or more matches
empty
else -- One match, plus some unifiers
ASSERT( not (null unifiers) )
- parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
+ parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
- ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
+ ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
+ ptext (sLit "when compiling the other instance declarations")])]
where
- ispecs = [ispec | (_, ispec) <- matches]
+ ispecs = [ispec | (ispec, _) <- matches]
+
+ mk_eq_err :: Inst -> (TidyEnv, SDoc)
+ mk_eq_err inst = misMatchMsg tidy_env (eqInstTys inst)
+
+ mk_no_inst_err insts
+ | null insts = empty
+
+ | Just (loc, givens) <- mb_what, -- Nested (type signatures, instance decls)
+ not (isEmptyVarSet (tyVarsOfInsts insts))
+ = vcat [ addInstLoc insts $
+ sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts
+ , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens]
+ , show_fixes (fix1 loc : fixes2) ]
+
+ | otherwise -- Top level
+ = vcat [ addInstLoc insts $
+ ptext (sLit "No instance") <> plural insts
+ <+> ptext (sLit "for") <+> pprDictsTheta insts
+ , show_fixes fixes2 ]
- mk_probable_fix tidy_env dicts
- = returnM (tidy_env, sep [ptext SLIT("Possible fix:"), nest 2 (vcat fixes)])
where
- fixes = add_ors (fix1 ++ fix2)
-
- fix1 = case mb_what of
- Nothing -> [] -- Top level
- Just what -> -- Nested (type signatures, instance decls)
- [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
- ptext SLIT("to the") <+> what] ]
-
- fix2 | null instance_dicts = []
- | otherwise = [ ptext SLIT("add an instance declaration for")
- <+> pprDictsTheta instance_dicts ]
- instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
+ fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts
+ <+> ptext (sLit "to the context of"),
+ nest 2 (ppr (instLocOrigin loc)) ]
+ -- I'm not sure it helps to add the location
+ -- nest 2 (ptext (sLit "at") <+> ppr (instLocSpan loc)) ]
+
+ fixes2 | null instance_dicts = []
+ | otherwise = [sep [ptext (sLit "add an instance declaration for"),
+ pprDictsTheta instance_dicts]]
+ instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)]
-- Insts for which it is worth suggesting an adding an instance declaration
-- Exclude implicit parameters, and tyvar dicts
- add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
- add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
- add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
+ show_fixes :: [SDoc] -> SDoc
+ show_fixes [] = empty
+ show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"),
+ nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
+addTopAmbigErrs :: [Inst] -> TcRn ()
addTopAmbigErrs dicts
-- Divide into groups that share a common set of ambiguous tyvars
- = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
+ = ifErrsM (return ()) $ -- Only report ambiguity if no other errors happened
+ -- See Note [Avoiding spurious errors]
+ mapM_ report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
where
(tidy_env, tidy_dicts) = tidyInsts dicts
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 tvs `thenM` \ (tidy_env, mono_msg) ->
- setSrcSpan (instLocSrcSpan (instLoc inst)) $
+ report pairs@((inst,tvs) : _) = do -- The pairs share a common set of ambiguous tyvars
+ (tidy_env, mono_msg) <- mkMonomorphismMsg tidy_env tvs
+ setSrcSpan (instSpan inst) $
-- the location of the first one will do for the err message
- addErrTcM (tidy_env, msg $$ mono_msg)
+ 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 (pprDictsInFull dicts)]
in_msg = text "in the constraint" <> plural dicts <> colon
+ report [] = panic "addTopAmbigErrs"
mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
-- Try to identify the offending variable
-- ASSUMPTION: the Insts are fully zonked
mkMonomorphismMsg tidy_env inst_tvs
- = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
- returnM (tidy_env, mk_msg docs)
+ = do { dflags <- getDOpts
+ ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
+ ; return (tidy_env, mk_msg dflags docs) }
where
- mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
+ mk_msg _ _ | any isRuntimeUnk inst_tvs
+ = vcat [ptext (sLit "Cannot resolve unknown runtime types:") <+>
+ (pprWithCommas ppr inst_tvs),
+ ptext (sLit "Use :print or :force to determine these types")]
+ mk_msg _ [] = ptext (sLit "Probable fix: add a type signature that fixes these type variable(s)")
-- 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),
- monomorphism_fix
- ]
-monomorphism_fix :: SDoc
-monomorphism_fix = ptext SLIT("Probable fix:") <+>
- (ptext SLIT("give these definition(s) an explicit type signature")
- $$ ptext SLIT("or use -fno-monomorphism-restriction"))
+ -- where monomorphism doesn't play any role
+ mk_msg dflags docs
+ = vcat [ptext (sLit "Possible cause: the monomorphism restriction applied to the following:"),
+ nest 2 (vcat docs),
+ monomorphism_fix dflags]
+
+monomorphism_fix :: DynFlags -> SDoc
+monomorphism_fix dflags
+ = ptext (sLit "Probable fix:") <+> vcat
+ [ptext (sLit "give these definition(s) an explicit type signature"),
+ if dopt Opt_MonomorphismRestriction dflags
+ then ptext (sLit "or use -XNoMonomorphismRestriction")
+ else empty] -- Only suggest adding "-XNoMonomorphismRestriction"
+ -- if it is not already set!
-warnDefault dicts default_ty
- = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
- addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
+warnDefault :: [(Inst, Class, Var)] -> Type -> TcM ()
+warnDefault ups default_ty = do
+ warn_flag <- doptM Opt_WarnTypeDefaults
+ addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
where
+ dicts = [d | (d,_,_) <- ups]
+
-- Tidy them first
(_, tidy_dicts) = tidyInsts dicts
- warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
+ warn_msg = vcat [ptext (sLit "Defaulting the following constraint(s) to type") <+>
quotes (ppr default_ty),
pprDictsInFull tidy_dicts]
--- Used for the ...Thetas variants; all top level
-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 :: Int -> [Inst] -> SDoc
reduceDepthErr n stack
- = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
- ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
+ = vcat [ptext (sLit "Context reduction stack overflow; size =") <+> int n,
+ ptext (sLit "Use -fcontext-stack=N to increase stack size to N"),
nest 4 (pprStack stack)]
+pprStack :: [Inst] -> SDoc
pprStack stack = vcat (map pprInstInFull stack)
\end{code}
projects / ghc-hetmet.git / blobdiff