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