Commit 5aa1ae24 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Simplify the typechecking of RULES

Not only does this fix Trac #5853, but it also eliminate
the horrid SimplEqsOnly part of the constraint simplifier.

The new plan is described in TcRules
 Note [Simplifying RULE constraints]
parent 68b4a098
......@@ -233,12 +233,9 @@ lookupInInertsStage :: SimplifierStage
lookupInInertsStage ct
| isWantedCt ct
= do { is <- getTcSInerts
; ctxt <- getTcSContext
; case lookupInInerts is (ctPred ct) of
Just ct_cached
| (not $ isDerivedCt ct) && (not $ simplEqsOnly ctxt)
-- Don't share if we are simplifying a RULE
-- see Note [Simplifying RULE lhs constraints]
| not (isDerivedCt ct)
-> setEvBind (ctId ct) (EvId (ctId ct_cached)) >>
return Stop
_ -> continueWith ct }
......@@ -682,15 +679,10 @@ interactWithInertsStage :: WorkItem -> TcS StopOrContinue
-- Precondition: if the workitem is a CTyEqCan then it will not be able to
-- react with anything at this stage.
interactWithInertsStage wi
= do { ctxt <- getTcSContext
; if simplEqsOnly ctxt && not (isCFunEqCan wi) then
-- Why not just "simplEqsOnly"? See Note [SimplEqsOnly and InteractWithInerts]
return (ContinueWith wi)
else
do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
; rels <- extractRelevantInerts wi
; traceTcS "relevant inerts are:" $ ppr rels
; foldlBagM interact_next (ContinueWith wi) rels } }
= do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
; rels <- extractRelevantInerts wi
; traceTcS "relevant inerts are:" $ ppr rels
; foldlBagM interact_next (ContinueWith wi) rels }
where interact_next Stop atomic_inert
= updInertSetTcS atomic_inert >> return Stop
......@@ -719,33 +711,6 @@ interactWithInertsStage wi
\end{code}
Note [SimplEqsOnly and InteractWithInerts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It may be possible when we are simplifying a RULE that we have two wanted constraints
of the form:
[W] c1 : F Int ~ Bool
[W] c2 : F Int ~ alpha
When we simplify RULES we only do equality reactions (simplEqsOnly). So the question is:
are we allowed to do type family interactions? We definitely do not want to apply top-level
family and dictionary instances but what should we do with the constraint set above?
Suppose that c1 gets processed first and enters the inert. Remember that he will enter a
CtFamHead map with (F Int) as the index. Now c2 comes along, we can't add him to the inert
set since it has exactly the same key, so we'd better react him with the inert c1. In fact
one might think that we should react him anyway to learn that (alpha ~ Bool). This is why
we allow CFunEqCan's to perform reactions with the inerts.
If we don't allow this, we will try to add both elements to the inert set and will panic!
The relevant example that fails when we don't allow such family reactions is:
indexed_types/should_compile/T2291.hs
NB: In previous versions of TcInteract the extra guard (not (isCFunEqCan wi)) was not there
but family reactions were actually happening earlier, during canonicalization. So the behaviour
has not changed -- previously this tricky point was completely lost and worked by accident.
\begin{code}
--------------------------------------------
......@@ -1441,12 +1406,8 @@ topReactionsStage workItem
tryTopReact :: WorkItem -> TcS StopOrContinue
tryTopReact wi
= do { inerts <- getTcSInerts
; ctxt <- getTcSContext
; if simplEqsOnly ctxt then
return (ContinueWith wi)
else
do { tir <- doTopReact inerts wi
; case tir of
; tir <- doTopReact inerts wi
; case tir of
NoTopInt
-> return (ContinueWith wi)
SomeTopInt rule what_next
......@@ -1455,7 +1416,7 @@ tryTopReact wi
vcat [ ptext (sLit "Top react:") <+> text rule
, text "WorkItem =" <+> ppr wi ]
; return what_next }
} }
}
data TopInteractResult
= NoTopInt
......
......@@ -23,8 +23,10 @@ import TcType
import TcHsType
import TcExpr
import TcEnv
import TcEvidence( TcEvBinds(..) )
import Type
import Id
import NameEnv( emptyNameEnv )
import Name
import Var
import VarSet
......@@ -50,6 +52,82 @@ an example (test simplCore/should_compile/rule2.hs) produced by Roman:
He wanted the rule to typecheck.
Note [Simplifying RULE constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
On the LHS of transformation rules we only simplify only equalities,
but not dictionaries. We want to keep dictionaries unsimplified, to
serve as the available stuff for the RHS of the rule. We *do* want to
simplify equalities, however, to detect ill-typed rules that cannot be
applied.
Implementation: the TcSFlags carried by the TcSMonad controls the
amount of simplification, so simplifyRuleLhs just sets the flag
appropriately.
Example. Consider the following left-hand side of a rule
f (x == y) (y > z) = ...
If we typecheck this expression we get constraints
d1 :: Ord a, d2 :: Eq a
We do NOT want to "simplify" to the LHS
forall x::a, y::a, z::a, d1::Ord a.
f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
Instead we want
forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
f ((==) d2 x y) ((>) d1 y z) = ...
Here is another example:
fromIntegral :: (Integral a, Num b) => a -> b
{-# RULES "foo" fromIntegral = id :: Int -> Int #-}
In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
we *dont* want to get
forall dIntegralInt.
fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
because the scsel will mess up RULE matching. Instead we want
forall dIntegralInt, dNumInt.
fromIntegral Int Int dIntegralInt dNumInt = id Int
Even if we have
g (x == y) (y == z) = ..
where the two dictionaries are *identical*, we do NOT WANT
forall x::a, y::a, z::a, d1::Eq a
f ((==) d1 x y) ((>) d1 y z) = ...
because that will only match if the dict args are (visibly) equal.
Instead we want to quantify over the dictionaries separately.
In short, simplifyRuleLhs must *only* squash equalities, leaving
all dicts unchanged, with absolutely no sharing.
Also note that we can't solve the LHS constraints in isolation:
Example foo :: Ord a => a -> a
foo_spec :: Int -> Int
{-# RULE "foo" foo = foo_spec #-}
Here, it's the RHS that fixes the type variable
HOWEVER, under a nested implication things are different
Consider
f :: (forall a. Eq a => a->a) -> Bool -> ...
{-# RULES "foo" forall (v::forall b. Eq b => b->b).
f b True = ...
#-}
Here we *must* solve the wanted (Eq a) from the given (Eq a)
resulting from skolemising the agument type of g. So we
revert to SimplCheck when going under an implication.
------------------------ So the plan is this -----------------------
* Step 1: Simplify the LHS and RHS constraints all together in one bag
We do this to discover all unification equalities
* Step 2: Zonk the ORIGINAL lhs constraints, and partition them into
the ones we will quantify over, and the others
* Step 3: Decide on the type varialbes to quantify over
* Step 4: Simplify the LHS and RHS constraints separately, using the
quantified constraint sas givens
\begin{code}
tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
tcRules decls = mapM (wrapLocM tcRule) decls
......@@ -62,52 +140,71 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
-- Note [Typechecking rules]
; vars <- tcRuleBndrs hs_bndrs
; let (id_bndrs, tv_bndrs) = partition (isId . snd) vars
; (lhs', lhs_lie, rhs', rhs_lie, rule_ty)
; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
<- tcExtendTyVarEnv2 tv_bndrs $
tcExtendIdEnv2 id_bndrs $
do { ((lhs', rule_ty), lhs_lie) <- captureConstraints (tcInferRho lhs)
; (rhs', rhs_lie) <- captureConstraints (tcMonoExpr rhs rule_ty)
; return (lhs', lhs_lie, rhs', rhs_lie, rule_ty) }
; (lhs_dicts, lhs_ev_binds, rhs_ev_binds)
<- simplifyRule name (map snd tv_bndrs) lhs_lie rhs_lie
-- IMPORTANT! We *quantify* over any dicts that appear in the LHS
-- Reason:
-- (a) The particular dictionary isn't important, because its value
-- depends only on the type
-- e.g gcd Int $fIntegralInt
-- Here we'd like to match against (gcd Int any_d) for any 'any_d'
--
-- (b) We'd like to make available the dictionaries bound
-- on the LHS in the RHS, so quantifying over them is good
-- See the 'lhs_dicts' in tcSimplifyAndCheck for the RHS
do { ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
; (lhs_evs, other_lhs_wanted) <- simplifyRule name lhs_wanted rhs_wanted
-- Now figure out what to quantify over
-- c.f. TcSimplify.simplifyInfer
-- We quantify over any tyvars free in *either* the rule
-- *or* the bound variables. The latter is important. Consider
-- ss (x,(y,z)) = (x,z)
-- RULE: forall v. fst (ss v) = fst v
-- The type of the rhs of the rule is just a, but v::(a,(b,c))
--
-- We also need to get the free tyvars of the LHS; but we do that
-- We also need to get the completely-uconstrained tyvars of
-- the LHS, lest they otherwise get defaulted to Any; but we do that
-- during zonking (see TcHsSyn.zonkRule)
; let tpl_ids = lhs_dicts ++ map snd id_bndrs
; let tpl_ids = lhs_evs ++ map snd id_bndrs
forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
-- Now figure out what to quantify over
-- c.f. TcSimplify.simplifyInfer
; zonked_forall_tvs <- zonkTyVarsAndFV forall_tvs
; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
; let tvs_to_quantify = varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)
; qkvs <- kindGeneralize $ tyVarsOfTypes (map tyVarKind tvs_to_quantify)
; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
; let qtkvs = qkvs ++ qtvs
; traceTc "tcRule" (vcat [ doubleQuotes (ftext name)
, ppr forall_tvs
, ppr qtvs
, ppr rule_ty
, vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
])
-- Simplify the RHS constraints
; loc <- getCtLoc (RuleSkol name)
; rhs_binds_var <- newTcEvBinds
; emitImplication $ Implic { ic_untch = NoUntouchables
, ic_env = emptyNameEnv
, ic_skols = qtkvs
, ic_given = lhs_evs
, ic_wanted = rhs_wanted
, ic_insol = insolubleWC rhs_wanted
, ic_binds = rhs_binds_var
, ic_loc = loc }
-- For the LHS constraints we must solve the remaining constraints
-- (a) so that we report insoluble ones
-- (b) so that we bind any soluble ones
; lhs_binds_var <- newTcEvBinds
; emitImplication $ Implic { ic_untch = NoUntouchables
, ic_env = emptyNameEnv
, ic_skols = qtkvs
, ic_given = lhs_evs
, ic_wanted = other_lhs_wanted
, ic_insol = insolubleWC other_lhs_wanted
, ic_binds = lhs_binds_var
, ic_loc = loc }
-- The tv_bndrs are already skolems, so no need to zonk them
; return (HsRule name act
(map (RuleBndr . noLoc) (qkvs ++ qtvs ++ tpl_ids))
(mkHsDictLet lhs_ev_binds lhs') fv_lhs
(mkHsDictLet rhs_ev_binds rhs') fv_rhs) }
(map (RuleBndr . noLoc) (qtkvs ++ tpl_ids))
(mkHsDictLet (TcEvBinds lhs_binds_var) lhs') fv_lhs
(mkHsDictLet (TcEvBinds rhs_binds_var) rhs') fv_rhs) }
tcRuleBndrs :: [RuleBndr Name] -> TcM [(Name, Var)]
tcRuleBndrs []
......
......@@ -39,7 +39,7 @@ module TcSMonad (
tryTcS, nestImplicTcS, recoverTcS,
wrapErrTcS, wrapWarnTcS,
SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
SimplContext(..), isInteractive, performDefaulting,
-- Getting and setting the flattening cache
getFlatCache, updFlatCache, addToSolved,
......@@ -803,30 +803,20 @@ type TcsUntouchables = (Untouchables,TcTyVarSet)
\begin{code}
data SimplContext
= SimplInfer SDoc -- Inferring type of a let-bound thing
| SimplRuleLhs RuleName -- Inferring type of a RULE lhs
| SimplInteractive -- Inferring type at GHCi prompt
| SimplCheck SDoc -- Checking a type signature or RULE rhs
instance Outputable SimplContext where
ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
ppr SimplInteractive = ptext (sLit "SimplInteractive")
isInteractive :: SimplContext -> Bool
isInteractive SimplInteractive = True
isInteractive _ = False
simplEqsOnly :: SimplContext -> Bool
-- Simplify equalities only, not dictionaries
-- This is used for the LHS of rules; ee
-- Note [Simplifying RULE lhs constraints] in TcSimplify
simplEqsOnly (SimplRuleLhs {}) = True
simplEqsOnly _ = False
performDefaulting :: SimplContext -> Bool
performDefaulting (SimplInfer {}) = False
performDefaulting (SimplRuleLhs {}) = False
performDefaulting SimplInteractive = True
performDefaulting (SimplCheck {}) = True
......@@ -960,7 +950,7 @@ nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
, tcs_untch = inner_untch
, tcs_count = count
, tcs_ic_depth = idepth+1
, tcs_context = ctxtUnderImplic ctxt
, tcs_context = ctxt
, tcs_inerts = new_inert_var
, tcs_worklist = wl_var
-- NB: worklist is going to be empty anyway,
......@@ -974,12 +964,6 @@ recoverTcS (TcS recovery_code) (TcS thing_inside)
= TcS $ \ env ->
TcM.recoverM (recovery_code env) (thing_inside env)
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
<+> doubleQuotes (ftext n))
ctxtUnderImplic ctxt = ctxt
tryTcS :: TcS a -> TcS a
-- Like runTcS, but from within the TcS monad
-- Completely afresh inerts and worklist, be careful!
......
......@@ -22,13 +22,13 @@ import TcSMonad
import TcInteract
import Inst
import Unify ( niFixTvSubst, niSubstTvSet )
import Type ( classifyPredType, PredTree(..) )
import Var
import VarSet
import VarEnv
import TcEvidence
import TypeRep
import Name
import NameEnv ( emptyNameEnv )
import Bag
import ListSetOps
import Util
......@@ -527,150 +527,59 @@ over implicit parameters. See the predicate isFreeWhenInferring.
* *
***********************************************************************************
Note [Simplifying RULE lhs constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
On the LHS of transformation rules we only simplify only equalities,
but not dictionaries. We want to keep dictionaries unsimplified, to
serve as the available stuff for the RHS of the rule. We *do* want to
simplify equalities, however, to detect ill-typed rules that cannot be
applied.
Implementation: the TcSFlags carried by the TcSMonad controls the
amount of simplification, so simplifyRuleLhs just sets the flag
appropriately.
Example. Consider the following left-hand side of a rule
f (x == y) (y > z) = ...
If we typecheck this expression we get constraints
d1 :: Ord a, d2 :: Eq a
We do NOT want to "simplify" to the LHS
forall x::a, y::a, z::a, d1::Ord a.
f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
Instead we want
forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
f ((==) d2 x y) ((>) d1 y z) = ...
See note [Simplifying RULE consraints] in TcRule
Here is another example:
fromIntegral :: (Integral a, Num b) => a -> b
{-# RULES "foo" fromIntegral = id :: Int -> Int #-}
In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
we *dont* want to get
forall dIntegralInt.
fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
because the scsel will mess up RULE matching. Instead we want
forall dIntegralInt, dNumInt.
fromIntegral Int Int dIntegralInt dNumInt = id Int
Even if we have
g (x == y) (y == z) = ..
where the two dictionaries are *identical*, we do NOT WANT
forall x::a, y::a, z::a, d1::Eq a
f ((==) d1 x y) ((>) d1 y z) = ...
because that will only match if the dict args are (visibly) equal.
Instead we want to quantify over the dictionaries separately.
In short, simplifyRuleLhs must *only* squash equalities, leaving
all dicts unchanged, with absolutely no sharing.
HOWEVER, under a nested implication things are different
Consider
f :: (forall a. Eq a => a->a) -> Bool -> ...
{-# RULES "foo" forall (v::forall b. Eq b => b->b).
f b True = ...
#-}
Here we *must* solve the wanted (Eq a) from the given (Eq a)
resulting from skolemising the agument type of g. So we
revert to SimplCheck when going under an implication.
Note [RULE quanfification over equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Decideing which equalities to quantify over is tricky:
* We do not want to quantify over insoluble equalities (Int ~ Bool)
(a) because we prefer to report a LHS type error
(b) because if such things end up in 'givens' we get a bogus
"inaccessible code" error
* But we do want to quantify over things like (a ~ F b), where
F is a type function.
The difficulty is that it's hard to tell what is insoluble!
So we see whether the simplificaiotn step yielded any type errors,
and if so refrain from quantifying over *any* equalites.
\begin{code}
simplifyRule :: RuleName
-> [TcTyVar] -- Explicit skolems
-> WantedConstraints -- Constraints from LHS
-> WantedConstraints -- Constraints from RHS
-> TcM ([EvVar], -- LHS dicts
TcEvBinds, -- Evidence for LHS
TcEvBinds) -- Evidence for RHS
-- See Note [Simplifying RULE lhs constraints]
simplifyRule name tv_bndrs lhs_wanted rhs_wanted
= do { loc <- getCtLoc (RuleSkol name)
-> TcM ([EvVar], WantedConstraints) -- LHS evidence varaibles
-- See Note [Simplifying RULE constraints] in TcRule
simplifyRule name lhs_wanted rhs_wanted
= do { zonked_all <- zonkWC (lhs_wanted `andWC` rhs_wanted)
; let doc = ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
untch = NoUntouchables
-- We allow ourselves to unify environment
-- variables; hence NoUntouchables
; (resid_wanted, _) <- runTcS (SimplInfer doc) untch emptyInert emptyWorkList $
solveWanteds zonked_all
; zonked_lhs <- zonkWC lhs_wanted
; let untch = NoUntouchables
-- We allow ourselves to unify environment
-- variables; hence *no untouchables*
-- DV: SPJ and I discussed a new plan here:
-- Step 1: Simplify everything in the same bag
-- Step 2: zonk away the lhs constraints and get only the non-trivial ones
-- Step 3: do the implications with these constraints
-- This will have the advantage that (i) we no longer need simplEqsOnly flag
-- and (ii) will fix problems appearing from touchable unification variables
-- in the givens, manifested by #5853
-- TODO ...
; (lhs_results, lhs_binds)
<- runTcS (SimplRuleLhs name) untch emptyInert emptyWorkList $
solveWanteds zonked_lhs
; let (q_cts, non_q_cts) = partitionBag quantify_me (wc_flat zonked_lhs)
quantify_me -- Note [RULE quantification over equalities]
| insolubleWC resid_wanted = quantify_insol
| otherwise = quantify_normal
quantify_insol ct = not (isEqPred (ctPred ct))
quantify_normal ct
| EqPred t1 t2 <- classifyPredType (ctPred ct)
= not (t1 `eqType` t2)
| otherwise
= True
; traceTc "simplifyRule" $
vcat [ text "zonked_lhs" <+> ppr zonked_lhs
, text "lhs_results" <+> ppr lhs_results
, text "lhs_binds" <+> ppr lhs_binds
, text "rhs_wanted" <+> ppr rhs_wanted ]
-- Don't quantify over equalities (judgement call here)
; let (eqs, dicts) = partitionBag (isEqPred . ctPred)
(wc_flat lhs_results)
lhs_dicts = map ctId (bagToList dicts)
-- Dicts and implicit parameters
-- NB: dicts come from lhs_results which
-- are all Wanted, hence have ids, hence
-- it's fine to call ctId on them
-- Fail if we have not got down to unsolved flats
; ev_binds_var <- newTcEvBinds
; emitImplication $ Implic { ic_untch = untch
, ic_env = emptyNameEnv
, ic_skols = tv_bndrs
, ic_given = lhs_dicts
, ic_wanted = lhs_results { wc_flat = eqs }
, ic_insol = insolubleWC lhs_results
, ic_binds = ev_binds_var
, ic_loc = loc }
-- Notice that we simplify the RHS with only the explicitly
-- introduced skolems, allowing the RHS to constrain any
-- unification variables.
-- Then, and only then, we call zonkQuantifiedTypeVariables
-- Example foo :: Ord a => a -> a
-- foo_spec :: Int -> Int
-- {-# RULE "foo" foo = foo_spec #-}
-- Here, it's the RHS that fixes the type variable
-- So we don't want to make untouchable the type
-- variables in the envt of the RHS, because they include
-- the template variables of the RULE
-- Hence the rather painful ad-hoc treatement here
; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
; rhs_binds1 <- simplifyCheck (SimplCheck doc) $
WC { wc_flat = emptyBag
, wc_insol = emptyBag
, wc_impl = unitBag $
Implic { ic_untch = NoUntouchables
, ic_env = emptyNameEnv
, ic_skols = tv_bndrs
, ic_given = lhs_dicts
, ic_wanted = rhs_wanted
, ic_insol = insolubleWC rhs_wanted
, ic_binds = rhs_binds_var
, ic_loc = loc } }
; rhs_binds2 <- readTcRef evb_ref
; return ( lhs_dicts
, EvBinds lhs_binds
, EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
vcat [ text "zonked_lhs" <+> ppr zonked_lhs
, text "q_cts" <+> ppr q_cts ]
; return (map ctId (bagToList q_cts), zonked_lhs { wc_flat = non_q_cts }) }
\end{code}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment