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