2 % (c) The University of Glasgow 2006
3 % (c) The AQUA Project, Glasgow University, 1993-1998
6 TcRules: Typechecking transformation rules
9 module TcRules ( tcRules ) where
25 import Data.List( partition )
28 Note [Typechecking rules]
29 ~~~~~~~~~~~~~~~~~~~~~~~~~
30 We *infer* the typ of the LHS, and use that type to *check* the type of
31 the RHS. That means that higher-rank rules work reasonably well. Here's
32 an example (test simplCore/should_compile/rule2.hs) produced by Roman:
34 foo :: (forall m. m a -> m b) -> m a -> m b
37 bar :: (forall m. m a -> m a) -> m a -> m a
40 {-# RULES "foo/bar" foo = bar #-}
42 He wanted the rule to typecheck.
45 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
46 tcRules decls = mapM (wrapLocM tcRule) decls
48 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
49 tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
50 = addErrCtxt (ruleCtxt name) $
51 do { traceTc "---- Rule ------" (ppr name)
53 -- Note [Typechecking rules]
54 ; vars <- tcRuleBndrs hs_bndrs
55 ; let (id_bndrs, tv_bndrs) = partition isId vars
56 ; (lhs', lhs_lie, rhs', rhs_lie, rule_ty)
57 <- tcExtendTyVarEnv tv_bndrs $
58 tcExtendIdEnv id_bndrs $
59 do { ((lhs', rule_ty), lhs_lie) <- captureConstraints (tcInferRho lhs)
60 ; (rhs', rhs_lie) <- captureConstraints (tcMonoExpr rhs rule_ty)
61 ; return (lhs', lhs_lie, rhs', rhs_lie, rule_ty) }
63 ; (lhs_dicts, lhs_ev_binds, rhs_ev_binds)
64 <- simplifyRule name tv_bndrs lhs_lie rhs_lie
66 -- IMPORTANT! We *quantify* over any dicts that appear in the LHS
68 -- (a) The particular dictionary isn't important, because its value
69 -- depends only on the type
70 -- e.g gcd Int $fIntegralInt
71 -- Here we'd like to match against (gcd Int any_d) for any 'any_d'
73 -- (b) We'd like to make available the dictionaries bound
74 -- on the LHS in the RHS, so quantifying over them is good
75 -- See the 'lhs_dicts' in tcSimplifyAndCheck for the RHS
77 -- We quantify over any tyvars free in *either* the rule
78 -- *or* the bound variables. The latter is important. Consider
79 -- ss (x,(y,z)) = (x,z)
80 -- RULE: forall v. fst (ss v) = fst v
81 -- The type of the rhs of the rule is just a, but v::(a,(b,c))
83 -- We also need to get the free tyvars of the LHS; but we do that
84 -- during zonking (see TcHsSyn.zonkRule)
86 ; let tpl_ids = lhs_dicts ++ id_bndrs
87 forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
89 -- Now figure out what to quantify over
90 -- c.f. TcSimplify.simplifyInfer
91 ; zonked_forall_tvs <- zonkTcTyVarsAndFV forall_tvs
92 ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
93 ; qtvs <- zonkQuantifiedTyVars $
94 varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)
96 ; return (HsRule name act
97 (map (RuleBndr . noLoc) (qtvs ++ tpl_ids)) -- yuk
98 (mkHsDictLet lhs_ev_binds lhs') fv_lhs
99 (mkHsDictLet rhs_ev_binds rhs') fv_rhs) }
101 tcRuleBndrs :: [RuleBndr Name] -> TcM [Var]
104 tcRuleBndrs (RuleBndr var : rule_bndrs)
105 = do { ty <- newFlexiTyVarTy openTypeKind
106 ; vars <- tcRuleBndrs rule_bndrs
107 ; return (mkLocalId (unLoc var) ty : vars) }
108 tcRuleBndrs (RuleBndrSig var rn_ty : rule_bndrs)
110 -- The tyvar 'a' is brought into scope first, just as if you'd written
112 = do { let ctxt = FunSigCtxt (unLoc var)
113 ; (tyvars, ty) <- tcHsPatSigType ctxt rn_ty
114 ; let skol_tvs = tcSuperSkolTyVars tyvars
115 id_ty = substTyWith tyvars (mkTyVarTys skol_tvs) ty
116 id = mkLocalId (unLoc var) id_ty
118 -- The type variables scope over subsequent bindings; yuk
119 ; vars <- tcExtendTyVarEnv skol_tvs $
120 tcRuleBndrs rule_bndrs
121 ; return (skol_tvs ++ id : vars) }
123 ruleCtxt :: FastString -> SDoc
124 ruleCtxt name = ptext (sLit "When checking the transformation rule") <+>
125 doubleQuotes (ftext name)