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