1 {-
2 (c) The University of Glasgow 2006
3 (c) The AQUA Project, Glasgow University, 1993-1998
6 TcRules: Typechecking transformation rules
7 -}
9 module TcRules ( tcRules ) where
11 import HsSyn
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 Name
23 import SrcLoc
24 import Outputable
25 import FastString
26 import Data.List( partition )
28 {-
29 Note [Typechecking rules]
30 ~~~~~~~~~~~~~~~~~~~~~~~~~
31 We *infer* the typ of the LHS, and use that type to *check* the type of
32 the RHS. That means that higher-rank rules work reasonably well. Here's
33 an example (test simplCore/should_compile/rule2.hs) produced by Roman:
35 foo :: (forall m. m a -> m b) -> m a -> m b
36 foo f = ...
38 bar :: (forall m. m a -> m a) -> m a -> m a
39 bar f = ...
41 {-# RULES "foo/bar" foo = bar #-}
43 He wanted the rule to typecheck.
45 Note [Simplifying RULE constraints]
46 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
47 On the LHS of transformation rules we only simplify only equalities,
48 but not dictionaries. We want to keep dictionaries unsimplified, to
49 serve as the available stuff for the RHS of the rule. We *do* want to
50 simplify equalities, however, to detect ill-typed rules that cannot be
51 applied.
53 Implementation: the TcSFlags carried by the TcSMonad controls the
54 amount of simplification, so simplifyRuleLhs just sets the flag
55 appropriately.
57 Example. Consider the following left-hand side of a rule
58 f (x == y) (y > z) = ...
59 If we typecheck this expression we get constraints
60 d1 :: Ord a, d2 :: Eq a
61 We do NOT want to "simplify" to the LHS
62 forall x::a, y::a, z::a, d1::Ord a.
63 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
65 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
66 f ((==) d2 x y) ((>) d1 y z) = ...
68 Here is another example:
69 fromIntegral :: (Integral a, Num b) => a -> b
70 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
71 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
72 we *dont* want to get
73 forall dIntegralInt.
74 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
75 because the scsel will mess up RULE matching. Instead we want
76 forall dIntegralInt, dNumInt.
77 fromIntegral Int Int dIntegralInt dNumInt = id Int
79 Even if we have
80 g (x == y) (y == z) = ..
81 where the two dictionaries are *identical*, we do NOT WANT
82 forall x::a, y::a, z::a, d1::Eq a
83 f ((==) d1 x y) ((>) d1 y z) = ...
84 because that will only match if the dict args are (visibly) equal.
85 Instead we want to quantify over the dictionaries separately.
87 In short, simplifyRuleLhs must *only* squash equalities, leaving
88 all dicts unchanged, with absolutely no sharing.
90 Also note that we can't solve the LHS constraints in isolation:
91 Example foo :: Ord a => a -> a
92 foo_spec :: Int -> Int
93 {-# RULE "foo" foo = foo_spec #-}
94 Here, it's the RHS that fixes the type variable
96 HOWEVER, under a nested implication things are different
97 Consider
98 f :: (forall a. Eq a => a->a) -> Bool -> ...
99 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
100 f b True = ...
101 #-}
102 Here we *must* solve the wanted (Eq a) from the given (Eq a)
103 resulting from skolemising the agument type of g. So we
104 revert to SimplCheck when going under an implication.
107 ------------------------ So the plan is this -----------------------
109 * Step 1: Simplify the LHS and RHS constraints all together in one bag
110 We do this to discover all unification equalities
112 * Step 2: Zonk the ORIGINAL lhs constraints, and partition them into
113 the ones we will quantify over, and the others
115 * Step 3: Decide on the type variables to quantify over
117 * Step 4: Simplify the LHS and RHS constraints separately, using the
118 quantified constraints as givens
119 -}
121 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
122 tcRules decls = mapM (wrapLocM tcRule) decls
124 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
125 tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
126 = addErrCtxt (ruleCtxt \$ unLoc name) \$
127 do { traceTc "---- Rule ------" (ppr name)
129 -- Note [Typechecking rules]
130 ; vars <- tcRuleBndrs hs_bndrs
131 ; let (id_bndrs, tv_bndrs) = partition isId vars
132 ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
133 <- tcExtendTyVarEnv tv_bndrs \$
134 tcExtendIdEnv id_bndrs \$
135 do { ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
136 ; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
137 ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
139 ; (lhs_evs, other_lhs_wanted) <- simplifyRule (unLoc name) lhs_wanted
140 rhs_wanted
142 -- Now figure out what to quantify over
143 -- c.f. TcSimplify.simplifyInfer
144 -- We quantify over any tyvars free in *either* the rule
145 -- *or* the bound variables. The latter is important. Consider
146 -- ss (x,(y,z)) = (x,z)
147 -- RULE: forall v. fst (ss v) = fst v
148 -- The type of the rhs of the rule is just a, but v::(a,(b,c))
149 --
150 -- We also need to get the completely-uconstrained tyvars of
151 -- the LHS, lest they otherwise get defaulted to Any; but we do that
152 -- during zonking (see TcHsSyn.zonkRule)
154 ; let tpl_ids = lhs_evs ++ id_bndrs
155 forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
156 ; gbls <- tcGetGlobalTyVars -- Even though top level, there might be top-level
157 -- monomorphic bindings from the MR; test tc111
158 ; qtkvs <- quantifyTyVars gbls forall_tvs
159 ; traceTc "tcRule" (vcat [ doubleQuotes (ftext \$ unLoc name)
160 , ppr forall_tvs
161 , ppr qtkvs
162 , ppr rule_ty
163 , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
164 ])
166 -- Simplify the RHS constraints
167 ; lcl_env <- getLclEnv
168 ; rhs_binds_var <- newTcEvBinds
169 ; emitImplication \$ Implic { ic_tclvl = topTcLevel
170 , ic_skols = qtkvs
171 , ic_no_eqs = False
172 , ic_given = lhs_evs
173 , ic_wanted = rhs_wanted
174 , ic_status = IC_Unsolved
175 , ic_binds = rhs_binds_var
176 , ic_info = RuleSkol (unLoc name)
177 , ic_env = lcl_env }
179 -- For the LHS constraints we must solve the remaining constraints
180 -- (a) so that we report insoluble ones
181 -- (b) so that we bind any soluble ones
182 ; lhs_binds_var <- newTcEvBinds
183 ; emitImplication \$ Implic { ic_tclvl = topTcLevel
184 , ic_skols = qtkvs
185 , ic_no_eqs = False
186 , ic_given = lhs_evs
187 , ic_wanted = other_lhs_wanted
188 , ic_status = IC_Unsolved
189 , ic_binds = lhs_binds_var
190 , ic_info = RuleSkol (unLoc name)
191 , ic_env = lcl_env }
193 ; return (HsRule name act
194 (map (noLoc . RuleBndr . noLoc) (qtkvs ++ tpl_ids))
195 (mkHsDictLet (TcEvBinds lhs_binds_var) lhs') fv_lhs
196 (mkHsDictLet (TcEvBinds rhs_binds_var) rhs') fv_rhs) }
198 tcRuleBndrs :: [LRuleBndr Name] -> TcM [Var]
199 tcRuleBndrs []
200 = return []
201 tcRuleBndrs (L _ (RuleBndr (L _ name)) : rule_bndrs)
202 = do { ty <- newFlexiTyVarTy openTypeKind
203 ; vars <- tcRuleBndrs rule_bndrs
204 ; return (mkLocalId name ty : vars) }
205 tcRuleBndrs (L _ (RuleBndrSig (L _ name) rn_ty) : rule_bndrs)
206 -- e.g x :: a->a
207 -- The tyvar 'a' is brought into scope first, just as if you'd written
208 -- a::*, x :: a->a
209 = do { let ctxt = RuleSigCtxt name
210 ; (id_ty, tv_prs, _) <- tcHsPatSigType ctxt rn_ty
211 ; let id = mkLocalId name id_ty
212 tvs = map snd tv_prs
213 -- tcHsPatSigType returns (Name,TyVar) pairs
214 -- for for RuleSigCtxt their Names are not
215 -- cloned, so we get (n, tv-with-name-n) pairs
216 -- See Note [Pattern signature binders] in TcHsType
218 -- The type variables scope over subsequent bindings; yuk
219 ; vars <- tcExtendTyVarEnv tvs \$
220 tcRuleBndrs rule_bndrs
221 ; return (tvs ++ id : vars) }
223 ruleCtxt :: FastString -> SDoc
224 ruleCtxt name = ptext (sLit "When checking the transformation rule") <+>
225 doubleQuotes (ftext name)