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
26 import Data.List( partition )
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
38 bar :: (forall m. m a -> m a) -> m a -> m a
41 {-# RULES "foo/bar" foo = bar #-}
43 He wanted the rule to typecheck.
46 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
47 tcRules decls = mapM (wrapLocM tcRule) decls
49 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
50 tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
51 = addErrCtxt (ruleCtxt name) $
52 do { traceTc "---- Rule ------" (ppr name)
54 -- Note [Typechecking rules]
55 ; vars <- tcRuleBndrs hs_bndrs
56 ; let (id_bndrs, tv_bndrs) = partition isId vars
57 ; (lhs', lhs_lie, rhs', rhs_lie, rule_ty)
58 <- tcExtendTyVarEnv tv_bndrs $
59 tcExtendIdEnv id_bndrs $
60 do { ((lhs', rule_ty), lhs_lie) <- captureConstraints (tcInferRho lhs)
61 ; (rhs', rhs_lie) <- captureConstraints (tcMonoExpr rhs rule_ty)
62 ; return (lhs', lhs_lie, rhs', rhs_lie, rule_ty) }
64 ; (lhs_dicts, lhs_ev_binds, rhs_ev_binds)
65 <- simplifyRule name tv_bndrs lhs_lie rhs_lie
67 -- IMPORTANT! We *quantify* over any dicts that appear in the LHS
69 -- (a) The particular dictionary isn't important, because its value
70 -- depends only on the type
71 -- e.g gcd Int $fIntegralInt
72 -- Here we'd like to match against (gcd Int any_d) for any 'any_d'
74 -- (b) We'd like to make available the dictionaries bound
75 -- on the LHS in the RHS, so quantifying over them is good
76 -- See the 'lhs_dicts' in tcSimplifyAndCheck for the RHS
78 -- We quantify over any tyvars free in *either* the rule
79 -- *or* the bound variables. The latter is important. Consider
80 -- ss (x,(y,z)) = (x,z)
81 -- RULE: forall v. fst (ss v) = fst v
82 -- The type of the rhs of the rule is just a, but v::(a,(b,c))
84 -- We also need to get the free tyvars of the LHS; but we do that
85 -- during zonking (see TcHsSyn.zonkRule)
87 ; let tpl_ids = lhs_dicts ++ id_bndrs
88 forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
90 -- Now figure out what to quantify over
91 -- c.f. TcSimplify.simplifyInfer
92 ; zonked_forall_tvs <- zonkTcTyVarsAndFV forall_tvs
93 ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
94 ; qtvs <- zonkQuantifiedTyVars $
95 varSetElems (zonked_forall_tvs `minusVarSet` gbl_tvs)
97 ; return (HsRule name act
98 (map (RuleBndr . noLoc) (qtvs ++ tpl_ids)) -- yuk
99 (mkHsDictLet lhs_ev_binds lhs') fv_lhs
100 (mkHsDictLet rhs_ev_binds rhs') fv_rhs) }
102 tcRuleBndrs :: [RuleBndr Name] -> TcM [Var]
105 tcRuleBndrs (RuleBndr var : rule_bndrs)
106 = do { ty <- newFlexiTyVarTy openTypeKind
107 ; vars <- tcRuleBndrs rule_bndrs
108 ; return (mkLocalId (unLoc var) ty : vars) }
109 tcRuleBndrs (RuleBndrSig var rn_ty : rule_bndrs)
111 -- The tyvar 'a' is brought into scope first, just as if you'd written
113 = do { let ctxt = FunSigCtxt (unLoc var)
114 ; (tyvars, ty) <- tcHsPatSigType ctxt rn_ty
115 ; let skol_tvs = tcSuperSkolTyVars tyvars
116 id_ty = substTyWith tyvars (mkTyVarTys skol_tvs) ty
117 id = mkLocalId (unLoc var) id_ty
119 -- The type variables scope over subsequent bindings; yuk
120 ; vars <- tcExtendTyVarEnv skol_tvs $
121 tcRuleBndrs rule_bndrs
122 ; return (skol_tvs ++ id : vars) }
124 ruleCtxt :: FastString -> SDoc
125 ruleCtxt name = ptext (sLit "When checking the transformation rule") <+>
126 doubleQuotes (ftext name)