tcSimplifyDeriv, tcSimplifyDefault,
bindInstsOfLocalFuns,
+
+ tcSimplifyStagedExpr,
misMatchMsg
) where
import SrcLoc
import DynFlags
import FastString
+
import Control.Monad
import Data.List
\end{code}
The excitement comes when simplifying the bindings for h. Initially
try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
-From this we get t1:=:t2, but also various bindings. We can't forget
+From this we get t1~t2, but also various bindings. We can't forget
the bindings (because of [LOOP]), but in fact t1 is what g is
polymorphic in.
-> [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
+-- constraint for them.
+--
-- 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)
+-- f :: forall qtvs. givens => (ir1, .., irn)
-- qtvs includes coercion variables
--
-- This binding must line up the 'rhs' in reduceImplication
makeImplicationBind loc all_tvs
- givens -- Guaranteed all Dicts
- -- or EqInsts
+ givens -- Guaranteed all Dicts or EqInsts
irreds
| null irreds -- If there are no irreds, we are done
= return ([], emptyBag)
= 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
+ -- extract equality binders
+ eq_cotvs = map eqInstType eq_givens
+
+ -- make the implication constraint instance
+ 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
+ tci_given = eq_givens ++ dict_givens,
+ -- same order as binders
+ tci_wanted = irreds,
+ tci_loc = loc }
+
+ -- create binders for the irreducible dictionaries
+ dict_irreds = filter (not . 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 }
+
+ -- create the binding
+ rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
+ co = mkWpApps (map instToId dict_givens)
+ <.> mkWpTyApps eq_cotvs
+ <.> 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))
}
-> TcM ([Inst], TcDictBinds)
tryHardCheckLoop doc wanteds
- = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds
+ = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds
; return (irreds,binds)
}
where
- try_me _ = ReduceMe AddSCs
+ try_me _ = ReduceMe
-- Here's the try-hard bit
-----------------------------------------------------------
where
env = mkRedEnv (pprInstLoc inst_loc) try_me givens
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ try_me inst | isMethodOrLit inst = ReduceMe
| otherwise = Stop
-- When checking against a given signature
-- we MUST be very gentle: Note [Check gently]
= do { (irreds, binds) <- checkLoop env wanteds
; return (irreds, binds) }
where
- env = mkRedEnv doc try_me []
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ env = mkInferRedEnv doc try_me
+ try_me inst | isMethodOrLit inst = ReduceMe
| otherwise = Stop
\end{code}
ds2 = $p1 dc
And now we've defined the superclass in terms of itself.
-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-
Two more nasty cases are in
tcrun021
tcrun033
+Solution:
+ - Satisfy the superclass context *all by itself*
+ (tcSimplifySuperClasses)
+ - And do so completely; i.e. no left-over constraints
+ to mix with the constraints arising from method declarations
+
+
+Note [Recursive instances and superclases]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this code, which arises in the context of "Scrap Your
+Boilerplate with Class".
+
+ class Sat a
+ class Data ctx a
+ instance Sat (ctx Char) => Data ctx Char
+ instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
+
+ class Data Maybe a => Foo a
+
+ instance Foo t => Sat (Maybe t)
+
+ instance Data Maybe a => Foo a
+ instance Foo a => Foo [a]
+ instance Foo [Char]
+
+In the instance for Foo [a], when generating evidence for the superclasses
+(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
+Using the instance for Data, we therefore need
+ (Sat (Maybe [a], Data Maybe a)
+But we are given (Foo a), and hence its superclass (Data Maybe a).
+So that leaves (Sat (Maybe [a])). Using the instance for Sat means
+we need (Foo [a]). And that is the very dictionary we are bulding
+an instance for! So we must put that in the "givens". So in this
+case we have
+ Given: Foo a, Foo [a]
+ Watend: Data Maybe [a]
+
+BUT we must *not not not* put the *superclasses* of (Foo [a]) in
+the givens, which is what 'addGiven' would normally do. Why? Because
+(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
+by selecting a superclass from Foo [a], which simply makes a loop.
+
+On the other hand we *must* put the superclasses of (Foo a) in
+the givens, as you can see from the derivation described above.
+
+Conclusion: in the very special case of tcSimplifySuperClasses
+we have one 'given' (namely the "this" dictionary) whose superclasses
+must not be added to 'givens' by addGiven.
+
+There is a complication though. Suppose there are equalities
+ instance (Eq a, a~b) => Num (a,b)
+Then we normalise the 'givens' wrt the equalities, so the original
+given "this" dictionary is cast to one of a different type. So it's a
+bit trickier than before to identify the "special" dictionary whose
+superclasses must not be added. See test
+ indexed-types/should_run/EqInInstance
+
+We need a persistent property of the dictionary to record this
+special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
+but cool), which is maintained by dictionary normalisation.
+Specifically, the InstLocOrigin is
+ NoScOrigin
+then the no-superclass thing kicks in. WATCH OUT if you fiddle
+with InstLocOrigin!
+
\begin{code}
-tcSimplifySuperClasses
+tcSimplifySuperClasses
:: InstLoc
+ -> Inst -- The dict whose superclasses
+ -- are being figured out
-> [Inst] -- Given
-> [Inst] -- Wanted
-> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
+tcSimplifySuperClasses loc this givens sc_wanteds
= do { traceTc (text "tcSimplifySuperClasses")
+
+ -- Note [Recursive instances and superclases]
+ ; no_sc_loc <- getInstLoc NoScOrigin
+ ; let no_sc_this = setInstLoc this no_sc_loc
+
+ ; let env = RedEnv { red_doc = pprInstLoc loc,
+ red_try_me = try_me,
+ red_givens = no_sc_this : givens,
+ red_stack = (0,[]),
+ red_improve = False } -- No unification vars
+
+
; (irreds,binds1) <- checkLoop env sc_wanteds
; let (tidy_env, tidy_irreds) = tidyInsts irreds
- ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
+ ; reportNoInstances tidy_env (Just (loc, givens)) [] tidy_irreds
; return binds1 }
where
- env = mkRedEnv (pprInstLoc loc) try_me givens
- try_me _ = ReduceMe NoSCs
- -- Like tryHardCheckLoop, but with NoSCs
+ try_me _ = ReduceMe -- Try hard, so we completely solve the superclass
+ -- constraints right here. See Note [SUPERCLASS-LOOP 1]
\end{code}
tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
-- Zonk everything in sight
= do { traceTc (text "tcSimplifyRestricted")
- ; wanteds' <- zonkInsts wanteds
+ ; wanteds_z <- zonkInsts wanteds
-- 'ReduceMe': Reduce as far as we can. Don't stop at
-- dicts; the idea is to get rid of as many type
-- BUT do no improvement! See Plan D above
-- 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) <- reduceContext env wanteds'
+ ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
+ ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds_z
-- Next, figure out the tyvars we will quantify over
; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
ppr _binds,
ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
+ -- Zonk wanteds again! The first call to reduceContext may have
+ -- instantiated some variables.
+ -- FIXME: If red_improve would work, we could propagate that into
+ -- the equality solver, too, to prevent instantating any
+ -- variables.
+ ; wanteds_zz <- zonkInsts wanteds_z
+
-- The first step may have squashed more methods than
-- necessary, so try again, this time more gently, knowing the exact
-- set of type variables to quantify over.
; let is_nested_group = isNotTopLevel top_lvl
try_me inst | isFreeWrtTyVars qtvs inst,
(is_nested_group || isDict inst) = Stop
- | otherwise = ReduceMe AddSCs
+ | otherwise = ReduceMe
env = mkNoImproveRedEnv doc try_me
- ; (_imp, binds, irreds) <- reduceContext env wanteds'
+ ; (_imp, binds, irreds) <- reduceContext env wanteds_zz
-- See "Notes on implicit parameters, Question 4: top level"
; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
}
-- Sigh: we need to reduce inside implications
- red_env = mkRedEnv doc try_me []
+ red_env = mkInferRedEnv doc try_me
doc = ptext (sLit "Implication constraint in RULE lhs")
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ try_me inst | isMethodOrLit inst = ReduceMe
| otherwise = Stop -- Be gentle
\end{code}
; let env = mkRedEnv doc try_me given_ips'
; (improved, binds, irreds) <- reduceContext env wanteds'
- ; if not improved then
+ ; if null irreds || not improved then
ASSERT( all is_free irreds )
do { extendLIEs irreds
; return binds }
- else
- tcSimplifyIPs given_ips wanteds }
+ 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]
+ { binds1 <- tcSimplifyIPs given_ips' irreds
+ ; return $ binds `unionBags` binds1
+ } }
where
doc = text "tcSimplifyIPs" <+> ppr given_ips
ip_set = mkNameSet (ipNamesOfInsts given_ips)
-- Simplify any methods that mention the implicit parameter
try_me inst | is_free inst = Stop
- | otherwise = ReduceMe NoSCs
+ | otherwise = ReduceMe
\end{code}
, red_try_me :: Inst -> WhatToDo
, red_improve :: Bool -- True <=> do improvement
, red_givens :: [Inst] -- All guaranteed rigid
- -- Always dicts
+ -- Always dicts & equalities
-- but see Note [Rigidity]
+
, red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
-- See Note [RedStack]
}
red_stack = (0,[]),
red_improve = True }
+mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
+-- No givens at all
+mkInferRedEnv doc try_me
+ = RedEnv { red_doc = doc, red_try_me = try_me,
+ red_givens = [],
+ red_stack = (0,[]),
+ red_improve = True }
+
mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
-- Do not do improvement; no givens
mkNoImproveRedEnv doc try_me
red_improve = True }
data WhatToDo
- = ReduceMe WantSCs -- Try to reduce this
- -- 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)!
+ = ReduceMe -- Try to reduce this
+ -- 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)!
| Stop -- Return as irreducible unless it can
-- be reduced to a constant in one step
}
-- Solve the *wanted* *dictionary* constraints (not implications)
- -- This may expose some further equational constraints...
+ -- This may expose some further equational constraints in the course
+ -- of improvement due to functional dependencies if any of the
+ -- involved unifications gets deferred.
; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+ -- The getLIE is reqd because reduceList does improvement
+ -- (via extendAvails) which may in turn do unification
; (dict_binds,
bound_dicts,
dict_irreds) <- extractResults avails wanted_dicts
-- 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 }
+ -- NB: Equality irreds need to be converted, as the recursive
+ -- invocation of the solver will still treat them as wanteds
+ -- otherwise.
+ ; let implic_env = env { red_givens
+ = givens ++ bound_dicts ++
+ map wantedToLocalEqInst dict_irreds }
; (implic_binds_s, implic_irreds_s)
<- mapAndUnzipM (reduceImplication implic_env) wanted_implics
; let implic_binds = unionManyBags implic_binds_s
-- go round again. We do so in either of two cases:
-- (1) If dictionary reduction or equality solving led to
-- improvement (i.e., instantiated type variables).
- -- (2) If we uncovered extra equalities. We will try to solve them
- -- in the next iteration.
+ -- (2) If we reduced dictionaries (i.e., got dictionary bindings),
+ -- they may have exposed further opportunities to normalise
+ -- family applications. See Note [Dictionary Improvement]
+ --
+ -- NB: We do *not* go around for new extra_eqs. Morally, we should,
+ -- but we can't without risking non-termination (see #2688). By
+ -- not going around, we miss some legal programs mixing FDs and
+ -- TFs, but we never claimed to support such programs in the
+ -- current implementation anyway.
; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs
avails_improved = availsImproved avails
improvedFlexible = avails_improved || eq_improved
- extraEqs = (not . null) extra_eqs
- improved = improvedFlexible || extraEqs
+ reduced_dicts = not (isEmptyBag dict_binds)
+ improved = improvedFlexible || reduced_dicts
--
improvedHint = (if avails_improved then " [AVAILS]" else "") ++
- (if eq_improved then " [EQ]" else "") ++
- (if extraEqs then " [EXTRA EQS]" else "")
+ (if eq_improved then " [EQ]" else "")
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
; return (tidy_env, msg) }
\end{code}
+Note [Dictionary Improvement]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reduceContext, we first reduce equalities and then class constraints.
+However, the letter may expose further opportunities for the former. Hence,
+we need to go around again if dictionary reduction produced any dictionary
+bindings. The following example demonstrated the point:
+
+ data EX _x _y (p :: * -> *)
+ data ANY
+
+ class Base p
+
+ class Base (Def p) => Prop p where
+ type Def p
+
+ instance Base ()
+ instance Prop () where
+ type Def () = ()
+
+ instance (Base (Def (p ANY))) => Base (EX _x _y p)
+ instance (Prop (p ANY)) => Prop (EX _x _y p) where
+ type Def (EX _x _y p) = EX _x _y p
+
+ data FOO x
+ instance Prop (FOO x) where
+ type Def (FOO x) = ()
+
+ data BAR
+ instance Prop BAR where
+ type Def BAR = EX () () FOO
+
+During checking the last instance declaration, we need to check the superclass
+cosntraint Base (Def BAR), which family normalisation reduced to
+Base (EX () () FOO). Chasing the instance for Base (EX _x _y p), gives us
+Base (Def (FOO ANY)), which again requires family normalisation of Def to
+Base () before we can finish.
+
+
The main context-reduction function is @reduce@. Here's its game plan.
\begin{code}
-- Base case: we're done!
reduce :: RedEnv -> Inst -> Avails -> TcM Avails
reduce env wanted avails
+
+ -- We don't reduce equalities here (and they must not end up as irreds
+ -- in the Avails!)
+ | isEqInst wanted
+ = return avails
+
-- It's the same as an existing inst, or a superclass thereof
| Just _ <- findAvail avails wanted
= do { traceTc (text "reduce: found " <+> ppr wanted)
Stop -> try_simple (addIrred NoSCs);
-- See Note [No superclasses for Stop]
- ReduceMe want_scs -> do -- It should be reduced
+ ReduceMe -> do -- It should be reduced
{ (avails, lookup_result) <- reduceInst env avails wanted
; case lookup_result of
- NoInstance -> addIrred want_scs avails wanted
+ NoInstance -> addIrred AddSCs avails wanted
-- Add it and its superclasses
- GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+ GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
GenInst wanteds' rhs
-> do { avails1 <- addIrred NoSCs avails wanted
; avails2 <- reduceList env wanteds' avails1
- ; addWanted want_scs avails2 wanted rhs wanteds' } }
+ ; addWanted AddSCs 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
\end{code}
+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data D r = ZeroD | SuccD (r (D r));
+
+ instance (Eq (r (D r))) => Eq (D r) where
+ ZeroD == ZeroD = True
+ (SuccD a) == (SuccD b) = a == b
+ _ == _ = False;
+
+ equalDC :: D [] -> D [] -> Bool;
+ equalDC = (==);
+
+We need to prove (Eq (D [])). Here's how we go:
+
+ d1 : Eq (D [])
+
+by instance decl, holds if
+ d2 : Eq [D []]
+ where d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+ d3 : D []
+ where d2 = dfEqList d3
+ d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+ d3 = d1
+ d2 = dfEqList d3
+ d1 = dfEqD d2
+
+and it'll even run! The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+
Note [SUPERCLASS-LOOP 2]
~~~~~~~~~~~~~~~~~~~~~~~~
-But the above isn't enough. Suppose we are *given* d1:Ord a,
-and want to deduce (d2:C [a]) where
+We need to be careful when adding "the constaint we are trying to prove".
+Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
class Ord a => C a where
instance Ord [a] => C [a] where ...
when adding superclasses. It's a bit like the occurs check in unification.
-Note [RECURSIVE DICTIONARIES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- data D r = ZeroD | SuccD (r (D r));
-
- instance (Eq (r (D r))) => Eq (D r) where
- ZeroD == ZeroD = True
- (SuccD a) == (SuccD b) = a == b
- _ == _ = False;
-
- equalDC :: D [] -> D [] -> Bool;
- equalDC = (==);
-
-We need to prove (Eq (D [])). Here's how we go:
-
- d1 : Eq (D [])
-
-by instance decl, holds if
- d2 : Eq [D []]
- where d1 = dfEqD d2
-
-by instance decl of Eq, holds if
- d3 : D []
- where d2 = dfEqList d3
- d1 = dfEqD d2
-
-But now we can "tie the knot" to give
-
- d3 = d1
- d2 = dfEqList d3
- d1 = dfEqD d2
-
-and it'll even run! The trick is to put the thing we are trying to prove
-(in this case Eq (D []) into the database before trying to prove its
-contributing clauses.
-
%************************************************************************
%* *
--
-- Note on coercion variables:
--
- -- The extra given coercion variables are bound at two different sites:
+ -- 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
+ -- the solved dictionaries use these binders;
-- these binders are generated by reduceImplication
--
+ -- Note [Binders for equalities]
+ -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ -- To reuse the binders of local/given equalities in the binders of
+ -- implication constraints, it is crucial that these given equalities
+ -- always have the form
+ -- cotv :: t1 ~ t2
+ -- where cotv is a simple coercion type variable (and not a more
+ -- complex coercion term). We require that the extra_givens always
+ -- have this form and exploit the special form when generating binders.
reduceImplication env
orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
tci_tyvars = tvs,
- tci_given = extra_givens, tci_wanted = wanteds })
+ tci_given = extra_givens, tci_wanted = wanteds
+ })
= do { -- Solve the sub-problem
- ; let try_me _ = ReduceMe AddSCs -- Note [Freeness and implications]
+ ; let try_me _ = ReduceMe -- Note [Freeness and implications]
env' = env { red_givens = extra_givens ++ red_givens env
, red_doc = sep [ptext (sLit "reduceImplication for")
<+> ppr name,
[ 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])
-- SLPJ Sept 07: what if improvement happened inside the checkLoop?
-- Then we must iterate the outer loop too!
+ ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+ -- we solve wanted eqs by side effect!
+
+ -- Progress is no longer measered by the number of bindings
+ -- If there are any irreds, but no bindings and no solved
+ -- equalities, we back off and do nothing
; let backOff = isEmptyLHsBinds binds && -- no new bindings
(not $ null irreds) && -- but still some irreds
- all (not . isEqInst) wanteds
- -- we may have instantiated a cotv
- -- => must make a new implication constraint!
+ didntSolveWantedEqs -- no instantiated cotv
- ; traceTc $ text "reduceImplication condition" <+> ppr backOff
-
- -- Progress is no longer measered by the number of bindings
; if backOff then -- No progress
- -- If there are any irreds, we back off and do nothing
return (emptyBag, [orig_implic])
else do
{ (simpler_implic_insts, bind)
-- 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)
+ ; let -- extract Id binders for dicts and CoTyVar binders for eqs;
+ -- see Note [Binders for equalities]
+ (extra_eq_givens, extra_dict_givens) = partition isEqInst
+ extra_givens
+ eq_cotvs = map instToVar extra_eq_givens
+ dict_ids = map instToId extra_dict_givens
+
+ -- Note [Always inline implication constraints]
+ wrap_inline | null dict_ids = idHsWrapper
+ | otherwise = WpInline
+ co = wrap_inline
+ <.> mkWpTyLams tvs
+ <.> mkWpTyLams eq_cotvs
+ <.> mkWpLams dict_ids
+ <.> WpLet (binds `unionBags` bind)
+ rhs = mkLHsWrap co payload
+ loc = instLocSpan inst_loc
+ -- wanted equalities are solved by updating their
+ -- cotv; we don't generate bindings for them
+ dict_bndrs = map (L loc . HsVar . instToId)
+ . filter (not . isEqInst)
+ $ wanteds
+ payload = mkBigLHsTup dict_bndrs
; traceTc (vcat [text "reduceImplication" <+> ppr name,
= return (binds, bound_dicts, irreds)
go binds bound_dicts irreds done (w:ws)
+ | isEqInst w
+ = go binds bound_dicts (w:irreds) done' 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
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
+addGiven avails given
+ = addAvailAndSCs want_scs avails given (Given given)
+ where
+ want_scs = case instLocOrigin (instLoc given) of
+ NoScOrigin -> NoSCs
+ _other -> AddSCs
+ -- Conditionally add superclasses for 'given'
+ -- See Note [Recursive instances and superclases]
+
+ -- 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}
; (irreds, _) <- tryHardCheckLoop doc wanteds
; let (tv_dicts, others) = partition ok irreds
- ; addNoInstanceErrs others
+ (tidy_env, tidy_insts) = tidyInsts others
+ ; reportNoInstances tidy_env Nothing [alt_fix] tidy_insts
-- See Note [Exotic derived instance contexts] in TcMType
; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
ok dict | isDict dict = validDerivPred (dictPred dict)
| otherwise = False
+ alt_fix = vcat [ptext (sLit "use a standalone 'deriving instance' declaration instead,"),
+ ptext (sLit "so you can specify the instance context yourself")]
\end{code}
tcSimplifyDefault theta = do
wanteds <- newDictBndrsO DefaultOrigin theta
(irreds, _) <- tryHardCheckLoop doc wanteds
- addNoInstanceErrs irreds
+ addNoInstanceErrs irreds
if null irreds then
return ()
else
doc = ptext (sLit "default declaration")
\end{code}
+@tcSimplifyStagedExpr@ performs a simplification but does so at a new
+stage. This is used when typechecking annotations and splices.
+
+\begin{code}
+
+tcSimplifyStagedExpr :: ThStage -> TcM a -> TcM (a, TcDictBinds)
+-- Type check an expression that runs at a top level stage as if
+-- it were going to be spliced and then simplify it
+tcSimplifyStagedExpr stage tc_action
+ = setStage stage $ do {
+ -- Typecheck the expression
+ (thing', lie) <- getLIE tc_action
+
+ -- Solve the constraints
+ ; const_binds <- tcSimplifyTop lie
+
+ ; return (thing', const_binds) }
+
+\end{code}
+
%************************************************************************
%* *
-> TcM ()
addNoInstanceErrs insts
= do { let (tidy_env, tidy_insts) = tidyInsts insts
- ; reportNoInstances tidy_env Nothing tidy_insts }
+ ; reportNoInstances tidy_env Nothing [] tidy_insts }
reportNoInstances
:: TidyEnv
-- Nothing => top level
-- Just (d,g) => d describes the construct
-- with givens g
+ -> [SDoc] -- Alternative fix for no-such-instance
-> [Inst] -- What is wanted (can include implications)
-> TcM ()
-reportNoInstances tidy_env mb_what insts
- = groupErrs (report_no_instances tidy_env mb_what) insts
+reportNoInstances tidy_env mb_what alt_fix insts
+ = groupErrs (report_no_instances tidy_env mb_what alt_fix) insts
-report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [Inst] -> TcM ()
-report_no_instances tidy_env mb_what insts
+report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [SDoc] -> [Inst] -> TcM ()
+report_no_instances tidy_env mb_what alt_fixes insts
= do { inst_envs <- tcGetInstEnvs
; let (implics, insts1) = partition isImplicInst insts
(insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
complain_implic inst -- Recurse!
= reportNoInstances tidy_env
(Just (tci_loc inst, tci_given inst))
- (tci_wanted inst)
+ alt_fixes (tci_wanted inst)
check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
-- Right msg => overlap message
= 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) ]
+ , show_fixes (fix1 loc : fixes2 ++ alt_fixes) ]
| otherwise -- Top level
= vcat [ addInstLoc insts $
ptext (sLit "No instance") <> plural insts
<+> ptext (sLit "for") <+> pprDictsTheta insts
- , show_fixes fixes2 ]
+ , show_fixes (fixes2 ++ alt_fixes) ]
where
fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts
projects / ghc-hetmet.git / blobdiff