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