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