1 %
2 % (c) The University of Glasgow 2006
3 % (c) The AQUA Project, Glasgow University, 1993-1998
4 %
6 TcRules: Typechecking transformation rules
8 \begin{code}
9 module TcRules ( tcRules ) where
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 Name
23 import SrcLoc
24 import Outputable
25 import FastString
26 import Data.List( partition )
27 \end{code}
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) = ...
64 Instead we want
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
121 \begin{code}
122 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
123 tcRules decls = mapM (wrapLocM tcRule) decls
125 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
126 tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
127   = addErrCtxt (ruleCtxt $unLoc name)$
128     do { traceTc "---- Rule ------" (ppr name)
130         -- Note [Typechecking rules]
131        ; vars <- tcRuleBndrs hs_bndrs
132        ; let (id_bndrs, tv_bndrs) = partition isId vars
133        ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
134             <- tcExtendTyVarEnv tv_bndrs $135 tcExtendIdEnv id_bndrs$
136                do { ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
137                   ; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
138                   ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
140        ; (lhs_evs, other_lhs_wanted) <- simplifyRule (unLoc name) lhs_wanted
141                                                      rhs_wanted
143         -- Now figure out what to quantify over
144         -- c.f. TcSimplify.simplifyInfer
145         -- We quantify over any tyvars free in *either* the rule
146         --  *or* the bound variables.  The latter is important.  Consider
147         --      ss (x,(y,z)) = (x,z)
148         --      RULE:  forall v. fst (ss v) = fst v
149         -- The type of the rhs of the rule is just a, but v::(a,(b,c))
150         --
151         -- We also need to get the completely-uconstrained tyvars of
152         -- the LHS, lest they otherwise get defaulted to Any; but we do that
153         -- during zonking (see TcHsSyn.zonkRule)
155        ; let tpl_ids    = lhs_evs ++ id_bndrs
156              forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
157        ; gbls  <- tcGetGlobalTyVars   -- Even though top level, there might be top-level
158                                       -- monomorphic bindings from the MR; test tc111
159        ; qtkvs <- quantifyTyVars gbls forall_tvs
160        ; traceTc "tcRule" (vcat [ doubleQuotes (ftext $unLoc name) 161 , ppr forall_tvs 162 , ppr qtkvs 163 , ppr rule_ty 164 , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ] 165 ]) 167 -- Simplify the RHS constraints 168 ; lcl_env <- getLclEnv 169 ; rhs_binds_var <- newTcEvBinds 170 ; emitImplication$ Implic { ic_untch  = noUntouchables
171                                   , ic_skols  = qtkvs
172                                   , ic_no_eqs = False
173                                   , ic_given  = lhs_evs
174                                   , ic_wanted = rhs_wanted
175                                   , ic_insol  = insolubleWC rhs_wanted
176                                   , ic_binds  = rhs_binds_var
177                                   , ic_info   = RuleSkol (unLoc name)
178                                   , ic_env    = lcl_env }
180            -- For the LHS constraints we must solve the remaining constraints
181            -- (a) so that we report insoluble ones
182            -- (b) so that we bind any soluble ones
183        ; lhs_binds_var <- newTcEvBinds
184        ; emitImplication $Implic { ic_untch = noUntouchables 185 , ic_skols = qtkvs 186 , ic_no_eqs = False 187 , ic_given = lhs_evs 188 , ic_wanted = other_lhs_wanted 189 , ic_insol = insolubleWC other_lhs_wanted 190 , ic_binds = lhs_binds_var 191 , ic_info = RuleSkol (unLoc name) 192 , ic_env = lcl_env } 194 ; return (HsRule name act 195 (map (noLoc . RuleBndr . noLoc) (qtkvs ++ tpl_ids)) 196 (mkHsDictLet (TcEvBinds lhs_binds_var) lhs') fv_lhs 197 (mkHsDictLet (TcEvBinds rhs_binds_var) rhs') fv_rhs) } 199 tcRuleBndrs :: [LRuleBndr Name] -> TcM [Var] 200 tcRuleBndrs [] 201 = return [] 202 tcRuleBndrs (L _ (RuleBndr (L _ name)) : rule_bndrs) 203 = do { ty <- newFlexiTyVarTy openTypeKind 204 ; vars <- tcRuleBndrs rule_bndrs 205 ; return (mkLocalId name ty : vars) } 206 tcRuleBndrs (L _ (RuleBndrSig (L _ name) rn_ty) : rule_bndrs) 207 -- e.g x :: a->a 208 -- The tyvar 'a' is brought into scope first, just as if you'd written 209 -- a::*, x :: a->a 210 = do { let ctxt = RuleSigCtxt name 211 ; (id_ty, tv_prs, _) <- tcHsPatSigType ctxt rn_ty 212 ; let id = mkLocalId name id_ty 213 tvs = map snd tv_prs 214 -- tcHsPatSigType returns (Name,TyVar) pairs 215 -- for for RuleSigCtxt their Names are not 216 -- cloned, so we get (n, tv-with-name-n) pairs 217 -- See Note [Pattern signature binders] in TcHsType 219 -- The type variables scope over subsequent bindings; yuk 220 ; vars <- tcExtendTyVarEnv tvs$
221                   tcRuleBndrs rule_bndrs
222         ; return (tvs ++ id : vars) }
224 ruleCtxt :: FastString -> SDoc
225 ruleCtxt name = ptext (sLit "When checking the transformation rule") <+>
226                 doubleQuotes (ftext name)
227 \end{code}