never executed always true always false
1 {-# LANGUAGE TypeFamilies #-}
2
3 {-
4 (c) The University of Glasgow 2006
5 (c) The AQUA Project, Glasgow University, 1993-1998
6
7 -}
8
9 -- | Typechecking rewrite rules
10 module GHC.Tc.Gen.Rule ( tcRules ) where
11
12 import GHC.Prelude
13
14 import GHC.Hs
15 import GHC.Tc.Types
16 import GHC.Tc.Utils.Monad
17 import GHC.Tc.Solver
18 import GHC.Tc.Types.Constraint
19 import GHC.Core.Predicate
20 import GHC.Tc.Types.Origin
21 import GHC.Tc.Utils.TcMType
22 import GHC.Tc.Utils.TcType
23 import GHC.Tc.Gen.HsType
24 import GHC.Tc.Gen.Expr
25 import GHC.Tc.Utils.Env
26 import GHC.Tc.Utils.Unify( buildImplicationFor )
27 import GHC.Tc.Types.Evidence( mkTcCoVarCo )
28 import GHC.Core.Type
29 import GHC.Core.TyCon( isTypeFamilyTyCon )
30 import GHC.Types.Id
31 import GHC.Types.Var( EvVar )
32 import GHC.Types.Var.Set
33 import GHC.Types.Basic ( RuleName, allVarsOfKindDefault )
34 import GHC.Types.SrcLoc
35 import GHC.Utils.Outputable
36 import GHC.Utils.Panic
37 import GHC.Data.FastString
38 import GHC.Data.Bag
39
40 {-
41 Note [Typechecking rules]
42 ~~~~~~~~~~~~~~~~~~~~~~~~~
43 We *infer* the typ of the LHS, and use that type to *check* the type of
44 the RHS. That means that higher-rank rules work reasonably well. Here's
45 an example (test simplCore/should_compile/rule2.hs) produced by Roman:
46
47 foo :: (forall m. m a -> m b) -> m a -> m b
48 foo f = ...
49
50 bar :: (forall m. m a -> m a) -> m a -> m a
51 bar f = ...
52
53 {-# RULES "foo/bar" foo = bar #-}
54
55 He wanted the rule to typecheck.
56
57 Note [TcLevel in type checking rules]
58 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
59 Bringing type variables into scope naturally bumps the TcLevel. Thus, we type
60 check the term-level binders in a bumped level, and we must accordingly bump
61 the level whenever these binders are in scope.
62
63 Note [Re-quantify type variables in rules]
64 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
65 Consider this example from #17710:
66
67 foo :: forall k (a :: k) (b :: k). Proxy a -> Proxy b
68 foo x = Proxy
69 {-# RULES "foo" forall (x :: Proxy (a :: k)). foo x = Proxy #-}
70
71 Written out in more detail, the "foo" rewrite rule looks like this:
72
73 forall k (a :: k). forall (x :: Proxy (a :: k)). foo @k @a @b0 x = Proxy @k @b0
74
75 Where b0 is a unification variable. Where should b0 be quantified? We have to
76 quantify it after k, since (b0 :: k). But generalization usually puts inferred
77 type variables (such as b0) at the /front/ of the telescope! This creates a
78 conflict.
79
80 One option is to simply throw an error, per the principles of
81 Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType. This is what would happen
82 if we were generalising over a normal type signature. On the other hand, the
83 types in a rewrite rule aren't quite "normal", since the notions of specified
84 and inferred type variables aren't applicable.
85
86 A more permissive design (and the design that GHC uses) is to simply requantify
87 all of the type variables. That is, we would end up with this:
88
89 forall k (a :: k) (b :: k). forall (x :: Proxy (a :: k)). foo @k @a @b x = Proxy @k @b
90
91 It's a bit strange putting the generalized variable `b` after the user-written
92 variables `k` and `a`. But again, the notion of specificity is not relevant to
93 rewrite rules, since one cannot "visibly apply" a rewrite rule. This design not
94 only makes "foo" typecheck, but it also makes the implementation simpler.
95
96 See also Note [Generalising in tcTyFamInstEqnGuts] in GHC.Tc.TyCl, which
97 explains a very similar design when generalising over a type family instance
98 equation.
99 -}
100
101 tcRules :: [LRuleDecls GhcRn] -> TcM [LRuleDecls GhcTc]
102 tcRules decls = mapM (wrapLocMA tcRuleDecls) decls
103
104 tcRuleDecls :: RuleDecls GhcRn -> TcM (RuleDecls GhcTc)
105 tcRuleDecls (HsRules { rds_src = src
106 , rds_rules = decls })
107 = do { tc_decls <- mapM (wrapLocMA tcRule) decls
108 ; return $ HsRules { rds_ext = noExtField
109 , rds_src = src
110 , rds_rules = tc_decls } }
111
112 tcRule :: RuleDecl GhcRn -> TcM (RuleDecl GhcTc)
113 tcRule (HsRule { rd_ext = ext
114 , rd_name = rname@(L _ (_,name))
115 , rd_act = act
116 , rd_tyvs = ty_bndrs
117 , rd_tmvs = tm_bndrs
118 , rd_lhs = lhs
119 , rd_rhs = rhs })
120 = addErrCtxt (ruleCtxt name) $
121 do { traceTc "---- Rule ------" (pprFullRuleName rname)
122
123 -- Note [Typechecking rules]
124 ; (tc_lvl, stuff) <- pushTcLevelM $
125 generateRuleConstraints ty_bndrs tm_bndrs lhs rhs
126
127 ; let (id_bndrs, lhs', lhs_wanted
128 , rhs', rhs_wanted, rule_ty) = stuff
129
130 ; traceTc "tcRule 1" (vcat [ pprFullRuleName rname
131 , ppr lhs_wanted
132 , ppr rhs_wanted ])
133
134 ; (lhs_evs, residual_lhs_wanted)
135 <- simplifyRule name tc_lvl lhs_wanted rhs_wanted
136
137 -- SimplfyRule Plan, step 4
138 -- Now figure out what to quantify over
139 -- c.f. GHC.Tc.Solver.simplifyInfer
140 -- We quantify over any tyvars free in *either* the rule
141 -- *or* the bound variables. The latter is important. Consider
142 -- ss (x,(y,z)) = (x,z)
143 -- RULE: forall v. fst (ss v) = fst v
144 -- The type of the rhs of the rule is just a, but v::(a,(b,c))
145 --
146 -- We also need to get the completely-unconstrained tyvars of
147 -- the LHS, lest they otherwise get defaulted to Any; but we do that
148 -- during zonking (see GHC.Tc.Utils.Zonk.zonkRule)
149
150 ; let tpl_ids = lhs_evs ++ id_bndrs
151
152 -- See Note [Re-quantify type variables in rules]
153 ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids)
154 ; qtkvs <- quantifyTyVars allVarsOfKindDefault forall_tkvs
155 ; traceTc "tcRule" (vcat [ pprFullRuleName rname
156 , ppr forall_tkvs
157 , ppr qtkvs
158 , ppr rule_ty
159 , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
160 ])
161
162 -- SimplfyRule Plan, step 5
163 -- Simplify the LHS and RHS constraints:
164 -- For the LHS constraints we must solve the remaining constraints
165 -- (a) so that we report insoluble ones
166 -- (b) so that we bind any soluble ones
167 ; let skol_info = RuleSkol name
168 ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs
169 lhs_evs residual_lhs_wanted
170 ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs
171 lhs_evs rhs_wanted
172
173 ; emitImplications (lhs_implic `unionBags` rhs_implic)
174 ; return $ HsRule { rd_ext = ext
175 , rd_name = rname
176 , rd_act = act
177 , rd_tyvs = ty_bndrs -- preserved for ppr-ing
178 , rd_tmvs = map (noLocA . RuleBndr noAnn . noLocA)
179 (qtkvs ++ tpl_ids)
180 , rd_lhs = mkHsDictLet lhs_binds lhs'
181 , rd_rhs = mkHsDictLet rhs_binds rhs' } }
182
183 generateRuleConstraints :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
184 -> LHsExpr GhcRn -> LHsExpr GhcRn
185 -> TcM ( [TcId]
186 , LHsExpr GhcTc, WantedConstraints
187 , LHsExpr GhcTc, WantedConstraints
188 , TcType )
189 generateRuleConstraints ty_bndrs tm_bndrs lhs rhs
190 = do { ((tv_bndrs, id_bndrs), bndr_wanted) <- captureConstraints $
191 tcRuleBndrs ty_bndrs tm_bndrs
192 -- bndr_wanted constraints can include wildcard hole
193 -- constraints, which we should not forget about.
194 -- It may mention the skolem type variables bound by
195 -- the RULE. c.f. #10072
196
197 ; tcExtendTyVarEnv tv_bndrs $
198 tcExtendIdEnv id_bndrs $
199 do { -- See Note [Solve order for RULES]
200 ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
201 ; (rhs', rhs_wanted) <- captureConstraints $
202 tcCheckMonoExpr rhs rule_ty
203 ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
204 ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
205
206 -- See Note [TcLevel in type checking rules]
207 tcRuleBndrs :: Maybe [LHsTyVarBndr () GhcRn] -> [LRuleBndr GhcRn]
208 -> TcM ([TcTyVar], [Id])
209 tcRuleBndrs (Just bndrs) xs
210 = do { (tybndrs1,(tys2,tms)) <- bindExplicitTKBndrs_Skol bndrs $
211 tcRuleTmBndrs xs
212 ; let tys1 = binderVars tybndrs1
213 ; return (tys1 ++ tys2, tms) }
214
215 tcRuleBndrs Nothing xs
216 = tcRuleTmBndrs xs
217
218 -- See Note [TcLevel in type checking rules]
219 tcRuleTmBndrs :: [LRuleBndr GhcRn] -> TcM ([TcTyVar],[Id])
220 tcRuleTmBndrs [] = return ([],[])
221 tcRuleTmBndrs (L _ (RuleBndr _ (L _ name)) : rule_bndrs)
222 = do { ty <- newOpenFlexiTyVarTy
223 ; (tyvars, tmvars) <- tcRuleTmBndrs rule_bndrs
224 ; return (tyvars, mkLocalId name Many ty : tmvars) }
225 tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs)
226 -- e.g x :: a->a
227 -- The tyvar 'a' is brought into scope first, just as if you'd written
228 -- a::*, x :: a->a
229 -- If there's an explicit forall, the renamer would have already reported an
230 -- error for each out-of-scope type variable used
231 = do { let ctxt = RuleSigCtxt name
232 ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt HM_Sig rn_ty OpenKind
233 ; let id = mkLocalId name Many id_ty
234 -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType
235
236 -- The type variables scope over subsequent bindings; yuk
237 ; (tyvars, tmvars) <- tcExtendNameTyVarEnv tvs $
238 tcRuleTmBndrs rule_bndrs
239 ; return (map snd tvs ++ tyvars, id : tmvars) }
240
241 ruleCtxt :: FastString -> SDoc
242 ruleCtxt name = text "When checking the rewrite rule" <+>
243 doubleQuotes (ftext name)
244
245
246 {-
247 *********************************************************************************
248 * *
249 Constraint simplification for rules
250 * *
251 ***********************************************************************************
252
253 Note [The SimplifyRule Plan]
254 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
255 Example. Consider the following left-hand side of a rule
256 f (x == y) (y > z) = ...
257 If we typecheck this expression we get constraints
258 d1 :: Ord a, d2 :: Eq a
259 We do NOT want to "simplify" to the LHS
260 forall x::a, y::a, z::a, d1::Ord a.
261 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
262 Instead we want
263 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
264 f ((==) d2 x y) ((>) d1 y z) = ...
265
266 Here is another example:
267 fromIntegral :: (Integral a, Num b) => a -> b
268 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
269 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
270 we *dont* want to get
271 forall dIntegralInt.
272 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
273 because the scsel will mess up RULE matching. Instead we want
274 forall dIntegralInt, dNumInt.
275 fromIntegral Int Int dIntegralInt dNumInt = id Int
276
277 Even if we have
278 g (x == y) (y == z) = ..
279 where the two dictionaries are *identical*, we do NOT WANT
280 forall x::a, y::a, z::a, d1::Eq a
281 f ((==) d1 x y) ((>) d1 y z) = ...
282 because that will only match if the dict args are (visibly) equal.
283 Instead we want to quantify over the dictionaries separately.
284
285 In short, simplifyRuleLhs must *only* squash equalities, leaving
286 all dicts unchanged, with absolutely no sharing.
287
288 Also note that we can't solve the LHS constraints in isolation:
289 Example foo :: Ord a => a -> a
290 foo_spec :: Int -> Int
291 {-# RULE "foo" foo = foo_spec #-}
292 Here, it's the RHS that fixes the type variable
293
294 HOWEVER, under a nested implication things are different
295 Consider
296 f :: (forall a. Eq a => a->a) -> Bool -> ...
297 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
298 f b True = ...
299 #-}
300 Here we *must* solve the wanted (Eq a) from the given (Eq a)
301 resulting from skolemising the argument type of g. So we
302 revert to SimplCheck when going under an implication.
303
304
305 --------- So the SimplifyRule Plan is this -----------------------
306
307 * Step 0: typecheck the LHS and RHS to get constraints from each
308
309 * Step 1: Simplify the LHS and RHS constraints all together in one bag
310 We do this to discover all unification equalities
311
312 * Step 2: Zonk the ORIGINAL (unsimplified) LHS constraints, to take
313 advantage of those unifications
314
315 * Setp 3: Partition the LHS constraints into the ones we will
316 quantify over, and the others.
317 See Note [RULE quantification over equalities]
318
319 * Step 4: Decide on the type variables to quantify over
320
321 * Step 5: Simplify the LHS and RHS constraints separately, using the
322 quantified constraints as givens
323
324 Note [Solve order for RULES]
325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
326 In step 1 above, we need to be a bit careful about solve order.
327 Consider
328 f :: Int -> T Int
329 type instance T Int = Bool
330
331 RULE f 3 = True
332
333 From the RULE we get
334 lhs-constraints: T Int ~ alpha
335 rhs-constraints: Bool ~ alpha
336 where 'alpha' is the type that connects the two. If we glom them
337 all together, and solve the RHS constraint first, we might solve
338 with alpha := Bool. But then we'd end up with a RULE like
339
340 RULE: f 3 |> (co :: T Int ~ Bool) = True
341
342 which is terrible. We want
343
344 RULE: f 3 = True |> (sym co :: Bool ~ T Int)
345
346 So we are careful to solve the LHS constraints first, and *then* the
347 RHS constraints. Actually much of this is done by the on-the-fly
348 constraint solving, so the same order must be observed in
349 tcRule.
350
351
352 Note [RULE quantification over equalities]
353 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
354 Deciding which equalities to quantify over is tricky:
355 * We do not want to quantify over insoluble equalities (Int ~ Bool)
356 (a) because we prefer to report a LHS type error
357 (b) because if such things end up in 'givens' we get a bogus
358 "inaccessible code" error
359
360 * But we do want to quantify over things like (a ~ F b), where
361 F is a type function.
362
363 The difficulty is that it's hard to tell what is insoluble!
364 So we see whether the simplification step yielded any type errors,
365 and if so refrain from quantifying over *any* equalities.
366
367 Note [Quantifying over coercion holes]
368 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
369 Equality constraints from the LHS will emit coercion hole Wanteds.
370 These don't have a name, so we can't quantify over them directly.
371 Instead, because we really do want to quantify here, invent a new
372 EvVar for the coercion, fill the hole with the invented EvVar, and
373 then quantify over the EvVar. Not too tricky -- just some
374 impedance matching, really.
375
376 Note [Simplify cloned constraints]
377 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
378 At this stage, we're simplifying constraints only for insolubility
379 and for unification. Note that all the evidence is quickly discarded.
380 We use a clone of the real constraint. If we don't do this,
381 then RHS coercion-hole constraints get filled in, only to get filled
382 in *again* when solving the implications emitted from tcRule. That's
383 terrible, so we avoid the problem by cloning the constraints.
384
385 -}
386
387 simplifyRule :: RuleName
388 -> TcLevel -- Level at which to solve the constraints
389 -> WantedConstraints -- Constraints from LHS
390 -> WantedConstraints -- Constraints from RHS
391 -> TcM ( [EvVar] -- Quantify over these LHS vars
392 , WantedConstraints) -- Residual un-quantified LHS constraints
393 -- See Note [The SimplifyRule Plan]
394 -- NB: This consumes all simple constraints on the LHS, but not
395 -- any LHS implication constraints.
396 simplifyRule name tc_lvl lhs_wanted rhs_wanted
397 = do {
398 -- Note [The SimplifyRule Plan] step 1
399 -- First solve the LHS and *then* solve the RHS
400 -- Crucially, this performs unifications
401 -- Why clone? See Note [Simplify cloned constraints]
402 ; lhs_clone <- cloneWC lhs_wanted
403 ; rhs_clone <- cloneWC rhs_wanted
404 ; setTcLevel tc_lvl $
405 runTcSDeriveds $
406 do { _ <- solveWanteds lhs_clone
407 ; _ <- solveWanteds rhs_clone
408 -- Why do them separately?
409 -- See Note [Solve order for RULES]
410 ; return () }
411
412 -- Note [The SimplifyRule Plan] step 2
413 ; lhs_wanted <- zonkWC lhs_wanted
414 ; let (quant_cts, residual_lhs_wanted) = getRuleQuantCts lhs_wanted
415
416 -- Note [The SimplifyRule Plan] step 3
417 ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
418
419 ; traceTc "simplifyRule" $
420 vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
421 , text "lhs_wanted" <+> ppr lhs_wanted
422 , text "rhs_wanted" <+> ppr rhs_wanted
423 , text "quant_cts" <+> ppr quant_cts
424 , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted
425 ]
426
427 ; return (quant_evs, residual_lhs_wanted) }
428
429 where
430 mk_quant_ev :: Ct -> TcM EvVar
431 mk_quant_ev ct
432 | CtWanted { ctev_dest = dest, ctev_pred = pred } <- ctEvidence ct
433 = case dest of
434 EvVarDest ev_id -> return ev_id
435 HoleDest hole -> -- See Note [Quantifying over coercion holes]
436 do { ev_id <- newEvVar pred
437 ; fillCoercionHole hole (mkTcCoVarCo ev_id)
438 ; return ev_id }
439 mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct)
440
441
442 getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
443 -- Extract all the constraints we can quantify over,
444 -- also returning the depleted WantedConstraints
445 --
446 -- NB: we must look inside implications, because with
447 -- -fdefer-type-errors we generate implications rather eagerly;
448 -- see GHC.Tc.Utils.Unify.implicationNeeded. Not doing so caused #14732.
449 --
450 -- Unlike simplifyInfer, we don't leave the WantedConstraints unchanged,
451 -- and attempt to solve them from the quantified constraints. That
452 -- nearly works, but fails for a constraint like (d :: Eq Int).
453 -- We /do/ want to quantify over it, but the short-cut solver
454 -- (see GHC.Tc.Solver.Interact Note [Shortcut solving]) ignores the quantified
455 -- and instead solves from the top level.
456 --
457 -- So we must partition the WantedConstraints ourselves
458 -- Not hard, but tiresome.
459
460 getRuleQuantCts wc
461 = float_wc emptyVarSet wc
462 where
463 float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
464 float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
465 = ( simple_yes `andCts` implic_yes
466 , emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_holes = holes })
467 where
468 (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples
469 (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)
470 emptyBag implics
471
472 float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
473 float_implic skol_tvs yes1 imp
474 = (yes1 `andCts` yes2, imp { ic_wanted = no })
475 where
476 (yes2, no) = float_wc new_skol_tvs (ic_wanted imp)
477 new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp
478
479 rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
480 rule_quant_ct skol_tvs ct = case classifyPredType (ctPred ct) of
481 EqPred _ t1 t2
482 | not (ok_eq t1 t2)
483 -> False -- Note [RULE quantification over equalities]
484 SpecialPred {}
485 -- RULES must never quantify over special predicates, as that
486 -- would leak internal GHC implementation details to the user.
487 --
488 -- Tests (for Concrete# predicates): RepPolyRule{1,2,3}.
489 -> False
490 _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs
491
492 ok_eq t1 t2
493 | t1 `tcEqType` t2 = False
494 | otherwise = is_fun_app t1 || is_fun_app t2
495
496 is_fun_app ty -- ty is of form (F tys) where F is a type function
497 = case tyConAppTyCon_maybe ty of
498 Just tc -> isTypeFamilyTyCon tc
499 Nothing -> False