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 Inst
  20 import Id
  21 import Name
  22 import SrcLoc
  23 import Outputable
  24 import FastString
  25 \end{code}
  26
  27 Note [Typechecking rules]
  28 ~~~~~~~~~~~~~~~~~~~~~~~~~
  29 We *infer* the typ of the LHS, and use that type to *check* the type of
  30 the RHS.  That means that higher-rank rules work reasonably well. Here's
  31 an example (test simplCore/should_compile/rule2.hs) produced by Roman:
  32
  33    foo :: (forall m. m a -> m b) -> m a -> m b
  34    foo f = ...
  35
  36    bar :: (forall m. m a -> m a) -> m a -> m a
  37    bar f = ...
  38
  39    {-# RULES "foo/bar" foo = bar #-}
  40
  41 He wanted the rule to typecheck.
  42
  43 \begin{code}
  44 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
  45 tcRules decls = mapM (wrapLocM tcRule) decls
  46
  47 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
  48 tcRule (HsRule name act vars lhs fv_lhs rhs fv_rhs)
  49   = addErrCtxt (ruleCtxt name)                  $ do
  50     traceTc (ptext (sLit "---- Rule ------") <+> ppr name)
  51
  52         -- Deal with the tyvars mentioned in signatures
  53     (ids, lhs', rhs', lhs_lie, rhs_lie, rule_ty) <-
  54       tcRuleBndrs vars $ \ ids -> do
  55                 -- Now LHS and RHS; see Note [Typechecking rules]
  56         ((lhs', rule_ty), lhs_lie) <- getLIE (tcInferRho lhs)
  57         (rhs', rhs_lie) <- getLIE (tcMonoExpr rhs rule_ty)
  58         return (ids, lhs', rhs', lhs_lie, rhs_lie, rule_ty)
  59
  60                 -- Check that LHS has no overloading at all
  61     (lhs_dicts, lhs_binds) <- tcSimplifyRuleLhs lhs_lie
  62
  63         -- Gather the template variables and tyvars
  64     let
  65         tpl_ids = map instToId lhs_dicts ++ ids
  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 initially 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         forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
  88
  89         -- RHS can be a bit more lenient.  In particular,
  90         -- we let constant dictionaries etc float outwards
  91         --
  92         -- NB: tcSimplifyInferCheck zonks the forall_tvs, and
  93         --     knocks out any that are constrained by the environment
  94     loc <- getInstLoc (SigOrigin (RuleSkol name))
  95     (forall_tvs1, rhs_binds) <- tcSimplifyInferCheck loc
  96                                         forall_tvs
  97                                         lhs_dicts rhs_lie
  98
  99     return (HsRule name act
 100                     (map (RuleBndr . noLoc) (forall_tvs1 ++ tpl_ids))   -- yuk
 101                     (mkHsDictLet lhs_binds lhs') fv_lhs
 102                     (mkHsDictLet rhs_binds rhs') fv_rhs)
 103
 104 tcRuleBndrs :: [RuleBndr Name] -> ([Id] -> TcM a) -> TcM a
 105 tcRuleBndrs [] thing_inside = thing_inside []
 106 tcRuleBndrs (RuleBndr var : vars) thing_inside
 107   = do  { ty <- newFlexiTyVarTy openTypeKind
 108         ; let id = mkLocalId (unLoc var) ty
 109         ; tcExtendIdEnv [id] $
 110           tcRuleBndrs vars (\ids -> thing_inside (id:ids)) }
 111 tcRuleBndrs (RuleBndrSig var rn_ty : vars) thing_inside
 112 --  e.g         x :: a->a
 113 --  The tyvar 'a' is brought into scope first, just as if you'd written
 114 --              a::*, x :: a->a
 115   = do  { let ctxt = FunSigCtxt (unLoc var)
 116         ; (tyvars, ty) <- tcHsPatSigType ctxt rn_ty
 117         ; let skol_tvs = tcSkolSigTyVars (SigSkol ctxt) tyvars
 118               id_ty = substTyWith tyvars (mkTyVarTys skol_tvs) ty
 119               id = mkLocalId (unLoc var) id_ty
 120         ; tcExtendTyVarEnv skol_tvs $
 121           tcExtendIdEnv [id] $
 122           tcRuleBndrs vars (\ids -> thing_inside (id:ids)) }
 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