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