Fix constraint simplification in rules
[ghc.git] / compiler / typecheck / TcRules.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The AQUA Project, Glasgow University, 1993-1998
4
5
6 TcRules: Typechecking transformation rules
7 -}
8
9 {-# LANGUAGE ViewPatterns #-}
10
11 module TcRules ( tcRules ) where
12
13 import HsSyn
14 import TcRnMonad
15 import TcSimplify
16 import TcMType
17 import TcType
18 import TcHsType
19 import TcExpr
20 import TcEnv
21 import TcUnify( buildImplicationFor )
22 import TcEvidence( mkTcCoVarCo )
23 import Type
24 import Id
25 import Var( EvVar )
26 import Name
27 import BasicTypes ( RuleName )
28 import SrcLoc
29 import Outputable
30 import FastString
31 import Bag
32 import Data.List( partition )
33
34 {-
35 Note [Typechecking rules]
36 ~~~~~~~~~~~~~~~~~~~~~~~~~
37 We *infer* the typ of the LHS, and use that type to *check* the type of
38 the RHS. That means that higher-rank rules work reasonably well. Here's
39 an example (test simplCore/should_compile/rule2.hs) produced by Roman:
40
41 foo :: (forall m. m a -> m b) -> m a -> m b
42 foo f = ...
43
44 bar :: (forall m. m a -> m a) -> m a -> m a
45 bar f = ...
46
47 {-# RULES "foo/bar" foo = bar #-}
48
49 He wanted the rule to typecheck.
50 -}
51
52 tcRules :: [LRuleDecls Name] -> TcM [LRuleDecls TcId]
53 tcRules decls = mapM (wrapLocM tcRuleDecls) decls
54
55 tcRuleDecls :: RuleDecls Name -> TcM (RuleDecls TcId)
56 tcRuleDecls (HsRules src decls)
57 = do { tc_decls <- mapM (wrapLocM tcRule) decls
58 ; return (HsRules src tc_decls) }
59
60 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
61 tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
62 = addErrCtxt (ruleCtxt $ snd $ unLoc name) $
63 do { traceTc "---- Rule ------" (pprFullRuleName name)
64
65 -- Note [Typechecking rules]
66 ; (vars, bndr_wanted) <- captureConstraints $
67 tcRuleBndrs hs_bndrs
68 -- bndr_wanted constraints can include wildcard hole
69 -- constraints, which we should not forget about.
70 -- It may mention the skolem type variables bound by
71 -- the RULE. c.f. Trac #10072
72
73 ; let (id_bndrs, tv_bndrs) = partition isId vars
74 ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
75 <- tcExtendTyVarEnv tv_bndrs $
76 tcExtendIdEnv id_bndrs $
77 do { -- See Note [Solve order for RULES]
78 ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
79 ; (rhs', rhs_wanted) <- captureConstraints $
80 tcMonoExpr rhs (mkCheckExpType rule_ty)
81 ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
82
83 ; traceTc "tcRule 1" (vcat [ pprFullRuleName name
84 , ppr lhs_wanted
85 , ppr rhs_wanted ])
86 ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
87 ; (lhs_evs, residual_lhs_wanted) <- simplifyRule (snd $ unLoc name)
88 all_lhs_wanted
89 rhs_wanted
90
91 -- SimplfyRule Plan, step 4
92 -- Now figure out what to quantify over
93 -- c.f. TcSimplify.simplifyInfer
94 -- We quantify over any tyvars free in *either* the rule
95 -- *or* the bound variables. The latter is important. Consider
96 -- ss (x,(y,z)) = (x,z)
97 -- RULE: forall v. fst (ss v) = fst v
98 -- The type of the rhs of the rule is just a, but v::(a,(b,c))
99 --
100 -- We also need to get the completely-uconstrained tyvars of
101 -- the LHS, lest they otherwise get defaulted to Any; but we do that
102 -- during zonking (see TcHsSyn.zonkRule)
103
104 ; let tpl_ids = lhs_evs ++ id_bndrs
105 ; forall_tkvs <- zonkTcTypesAndSplitDepVars $
106 rule_ty : map idType tpl_ids
107 ; gbls <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level
108 -- monomorphic bindings from the MR; test tc111
109 ; qtkvs <- quantifyZonkedTyVars gbls forall_tkvs
110 ; traceTc "tcRule" (vcat [ pprFullRuleName name
111 , ppr forall_tkvs
112 , ppr qtkvs
113 , ppr rule_ty
114 , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
115 ])
116
117 -- SimplfyRule Plan, step 5
118 -- Simplify the LHS and RHS constraints:
119 -- For the LHS constraints we must solve the remaining constraints
120 -- (a) so that we report insoluble ones
121 -- (b) so that we bind any soluble ones
122 ; let skol_info = RuleSkol (snd (unLoc name))
123 ; (lhs_implic, lhs_binds) <- buildImplicationFor topTcLevel skol_info qtkvs
124 lhs_evs residual_lhs_wanted
125 ; (rhs_implic, rhs_binds) <- buildImplicationFor topTcLevel skol_info qtkvs
126 lhs_evs rhs_wanted
127
128 ; emitImplications (lhs_implic `unionBags` rhs_implic)
129 ; return (HsRule name act
130 (map (noLoc . RuleBndr . noLoc) (qtkvs ++ tpl_ids))
131 (mkHsDictLet lhs_binds lhs') fv_lhs
132 (mkHsDictLet rhs_binds rhs') fv_rhs) }
133
134 tcRuleBndrs :: [LRuleBndr Name] -> TcM [Var]
135 tcRuleBndrs []
136 = return []
137 tcRuleBndrs (L _ (RuleBndr (L _ name)) : rule_bndrs)
138 = do { ty <- newOpenFlexiTyVarTy
139 ; vars <- tcRuleBndrs rule_bndrs
140 ; return (mkLocalId name ty : vars) }
141 tcRuleBndrs (L _ (RuleBndrSig (L _ name) rn_ty) : rule_bndrs)
142 -- e.g x :: a->a
143 -- The tyvar 'a' is brought into scope first, just as if you'd written
144 -- a::*, x :: a->a
145 = do { let ctxt = RuleSigCtxt name
146 ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt rn_ty
147 ; let id = mkLocalIdOrCoVar name id_ty
148 -- See Note [Pattern signature binders] in TcHsType
149
150 -- The type variables scope over subsequent bindings; yuk
151 ; vars <- tcExtendTyVarEnv tvs $
152 tcRuleBndrs rule_bndrs
153 ; return (tvs ++ id : vars) }
154
155 ruleCtxt :: FastString -> SDoc
156 ruleCtxt name = text "When checking the transformation rule" <+>
157 doubleQuotes (ftext name)
158
159
160 {-
161 *********************************************************************************
162 * *
163 Constraint simplification for rules
164 * *
165 ***********************************************************************************
166
167 Note [The SimplifyRule Plan]
168 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
169 Example. Consider the following left-hand side of a rule
170 f (x == y) (y > z) = ...
171 If we typecheck this expression we get constraints
172 d1 :: Ord a, d2 :: Eq a
173 We do NOT want to "simplify" to the LHS
174 forall x::a, y::a, z::a, d1::Ord a.
175 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
176 Instead we want
177 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
178 f ((==) d2 x y) ((>) d1 y z) = ...
179
180 Here is another example:
181 fromIntegral :: (Integral a, Num b) => a -> b
182 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
183 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
184 we *dont* want to get
185 forall dIntegralInt.
186 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
187 because the scsel will mess up RULE matching. Instead we want
188 forall dIntegralInt, dNumInt.
189 fromIntegral Int Int dIntegralInt dNumInt = id Int
190
191 Even if we have
192 g (x == y) (y == z) = ..
193 where the two dictionaries are *identical*, we do NOT WANT
194 forall x::a, y::a, z::a, d1::Eq a
195 f ((==) d1 x y) ((>) d1 y z) = ...
196 because that will only match if the dict args are (visibly) equal.
197 Instead we want to quantify over the dictionaries separately.
198
199 In short, simplifyRuleLhs must *only* squash equalities, leaving
200 all dicts unchanged, with absolutely no sharing.
201
202 Also note that we can't solve the LHS constraints in isolation:
203 Example foo :: Ord a => a -> a
204 foo_spec :: Int -> Int
205 {-# RULE "foo" foo = foo_spec #-}
206 Here, it's the RHS that fixes the type variable
207
208 HOWEVER, under a nested implication things are different
209 Consider
210 f :: (forall a. Eq a => a->a) -> Bool -> ...
211 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
212 f b True = ...
213 #-}
214 Here we *must* solve the wanted (Eq a) from the given (Eq a)
215 resulting from skolemising the argument type of g. So we
216 revert to SimplCheck when going under an implication.
217
218
219 --------- So the SimplifyRule Plan is this -----------------------
220
221 * Step 0: typecheck the LHS and RHS to get constraints from each
222
223 * Step 1: Simplify the LHS and RHS constraints all together in one bag
224 We do this to discover all unification equalities
225
226 * Step 2: Zonk the ORIGINAL (unsimplified) LHS constraints, to take
227 advantage of those unifications
228
229 * Setp 3: Partition the LHS constraints into the ones we will
230 quantify over, and the others.
231 See Note [RULE quantification over equalities]
232
233 * Step 4: Decide on the type variables to quantify over
234
235 * Step 5: Simplify the LHS and RHS constraints separately, using the
236 quantified constraints as givens
237
238 Note [Solve order for RULES]
239 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
240 In step 1 above, we need to be a bit careful about solve order.
241 Consider
242 f :: Int -> T Int
243 type instance T Int = Bool
244
245 RULE f 3 = True
246
247 From the RULE we get
248 lhs-constraints: T Int ~ alpha
249 rhs-constraints: Bool ~ alpha
250 where 'alpha' is the type that connects the two. If we glom them
251 all together, and solve the RHS constraint first, we might solve
252 with alpha := Bool. But then we'd end up with a RULE like
253
254 RULE: f 3 |> (co :: T Int ~ Booo) = True
255
256 which is terrible. We want
257
258 RULE: f 3 = True |> (sym co :: Bool ~ T Int)
259
260 So we are careful to solve the LHS constraints first, and *then* the
261 RHS constraints. Actually much of this is done by the on-the-fly
262 constraint solving, so the same order must be observed in
263 tcRule.
264
265
266 Note [RULE quantification over equalities]
267 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
268 Deciding which equalities to quantify over is tricky:
269 * We do not want to quantify over insoluble equalities (Int ~ Bool)
270 (a) because we prefer to report a LHS type error
271 (b) because if such things end up in 'givens' we get a bogus
272 "inaccessible code" error
273
274 * But we do want to quantify over things like (a ~ F b), where
275 F is a type function.
276
277 The difficulty is that it's hard to tell what is insoluble!
278 So we see whether the simplification step yielded any type errors,
279 and if so refrain from quantifying over *any* equalities.
280
281 Note [Quantifying over coercion holes]
282 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
283 Equality constraints from the LHS will emit coercion hole Wanteds.
284 These don't have a name, so we can't quantify over them directly.
285 Instead, because we really do want to quantify here, invent a new
286 EvVar for the coercion, fill the hole with the invented EvVar, and
287 then quantify over the EvVar. Not too tricky -- just some
288 impedence matching, really.
289
290 Note [Simplify cloned constraints]
291 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
292 At this stage, we're simplifying constraints only for insolubility
293 and for unification. Note that all the evidence is quickly discarded.
294 We use a clone of the real constraint. If we don't do this,
295 then RHS coercion-hole constraints get filled in, only to get filled
296 in *again* when solving the implications emitted from tcRule. That's
297 terrible, so we avoid the problem by cloning the constraints.
298
299 -}
300
301 simplifyRule :: RuleName
302 -> WantedConstraints -- Constraints from LHS
303 -> WantedConstraints -- Constraints from RHS
304 -> TcM ( [EvVar] -- Quantify over these LHS vars
305 , WantedConstraints) -- Residual un-quantified LHS constraints
306 -- See Note [The SimplifyRule Plan]
307 -- NB: This consumes all simple constraints on the LHS, but not
308 -- any LHS implication constraints.
309 simplifyRule name lhs_wanted rhs_wanted
310 = do { -- We allow ourselves to unify environment
311 -- variables: runTcS runs with topTcLevel
312 ; lhs_clone <- cloneWC lhs_wanted
313 ; rhs_clone <- cloneWC rhs_wanted
314
315 -- Note [The SimplifyRule Plan] step 1
316 -- First solve the LHS and *then* solve the RHS
317 -- Crucially, this performs unifications
318 -- See Note [Solve order for RULES]
319 -- See Note [Simplify cloned constraints]
320 ; insoluble <- runTcSDeriveds $
321 do { lhs_resid <- solveWanteds lhs_clone
322 ; rhs_resid <- solveWanteds rhs_clone
323 ; return ( insolubleWC lhs_resid ||
324 insolubleWC rhs_resid ) }
325
326 -- Note [The SimplifyRule Plan] step 2
327 ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
328
329 -- Note [The SimplifyRule Plan] step 3
330 ; let (quant_cts, no_quant_cts) = partitionBag (quantify_ct insoluble)
331 zonked_lhs_simples
332
333 ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
334
335 ; traceTc "simplifyRule" $
336 vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
337 , text "lhs_wanted" <+> ppr lhs_wanted
338 , text "rhs_wanted" <+> ppr rhs_wanted
339 , text "zonked_lhs_simples" <+> ppr zonked_lhs_simples
340 , text "quant_cts" <+> ppr quant_cts
341 , text "no_quant_cts" <+> ppr no_quant_cts
342 ]
343
344 ; return (quant_evs, lhs_wanted { wc_simple = no_quant_cts }) }
345
346 where
347 quantify_ct :: Bool -> Ct -> Bool
348 quantify_ct insol ct
349 | EqPred _ t1 t2 <- classifyPredType (ctPred ct)
350 = not (insol || t1 `tcEqType` t2)
351 -- Note [RULE quantification over equalities]
352
353 | otherwise
354 = True
355
356 mk_quant_ev :: Ct -> TcM EvVar
357 mk_quant_ev ct
358 | CtWanted { ctev_dest = dest, ctev_pred = pred } <- ctEvidence ct
359 = case dest of
360 EvVarDest ev_id -> return ev_id
361 HoleDest hole -> -- See Note [Quantifying over coercion holes]
362 do { ev_id <- newEvVar pred
363 ; fillCoercionHole hole (mkTcCoVarCo ev_id)
364 ; return ev_id }
365 mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct)