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