compiler/typecheck/TcRules.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The AQUA Project, Glasgow University, 1993-1998
   4 %
   5
   6 TcRules: Typechecking transformation rules
   7
   8 \begin{code}
   9 module TcRules ( tcRules ) where
  10
  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 Id
  20 import Name
  21 import VarSet
  22 import SrcLoc
  23 import Outputable
  24 import FastString
  25 import Data.List( partition )
  26 \end{code}
  27
  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:
  33
  34    foo :: (forall m. m a -> m b) -> m a -> m b
  35    foo f = ...
  36
  37    bar :: (forall m. m a -> m a) -> m a -> m a
  38    bar f = ...
  39
  40    {-# RULES "foo/bar" foo = bar #-}
  41
  42 He wanted the rule to typecheck.
  43
  44 \begin{code}
  45 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
  46 tcRules decls = mapM (wrapLocM tcRule) decls
  47
  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)
  52
  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) }
  62
  63        ; (lhs_dicts, lhs_ev_binds, rhs_ev_binds)
  64              <- simplifyRule name tv_bndrs lhs_lie rhs_lie
  65
  66         -- IMPORTANT!  We *quantify* over any dicts that appear in the LHS
  67         -- Reason:
  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'
  72         --
  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
  76
  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))
  82         --
  83         -- We also need to get the free tyvars of the LHS; but we do that
  84         -- during zonking (see TcHsSyn.zonkRule)
  85
  86        ; let tpl_ids    = lhs_dicts ++ id_bndrs
  87              forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
  88
  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)
  95
  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) }
 100
 101 tcRuleBndrs :: [RuleBndr Name] -> TcM [Var]
 102 tcRuleBndrs []
 103   = return []
 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)
 109 --  e.g         x :: a->a
 110 --  The tyvar 'a' is brought into scope first, just as if you'd written
 111 --              a::*, x :: a->a
 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
 117
 118               -- The type variables scope over subsequent bindings; yuk
 119         ; vars <- tcExtendTyVarEnv skol_tvs $
 120                   tcRuleBndrs rule_bndrs
 121         ; return (skol_tvs ++ id : vars) }
 122
 123 ruleCtxt :: FastString -> SDoc
 124 ruleCtxt name = ptext (sLit "When checking the transformation rule") <+>
 125                 doubleQuotes (ftext name)
 126 \end{code}
 127
 128
 129
 130