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