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) <- getConstraints (tcInferRho lhs)
61 ; (rhs', rhs_lie) <- getConstraints (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 (varSetElems forall_tvs)
93 ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
94 ; qtvs <- zonkQuantifiedTyVars (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 = tcSkolSigTyVars (SigSkol ctxt) 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)