Hurrah! This major commit adds support for scoped kind variables,
[ghc.git] / 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 {-# OPTIONS -fno-warn-tabs #-}
10 -- The above warning supression flag is a temporary kludge.
11 -- While working on this module you are encouraged to remove it and
12 -- detab the module (please do the detabbing in a separate patch). See
13 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
14 -- for details
15
16 module TcRules ( tcRules ) where
17
18 import HsSyn
19 import TcRnMonad
20 import TcSimplify
21 import TcMType
22 import TcType
23 import TcHsType
24 import TcExpr
25 import TcEnv
26 import Id
27 import Name
28 import SrcLoc
29 import Outputable
30 import FastString
31 import Data.List( partition )
32 \end{code}
33
34 Note [Typechecking rules]
35 ~~~~~~~~~~~~~~~~~~~~~~~~~
36 We *infer* the typ of the LHS, and use that type to *check* the type of 
37 the RHS.  That means that higher-rank rules work reasonably well. Here's
38 an example (test simplCore/should_compile/rule2.hs) produced by Roman:
39
40    foo :: (forall m. m a -> m b) -> m a -> m b
41    foo f = ...
42
43    bar :: (forall m. m a -> m a) -> m a -> m a
44    bar f = ...
45
46    {-# RULES "foo/bar" foo = bar #-}
47
48 He wanted the rule to typecheck.
49
50 \begin{code}
51 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
52 tcRules decls = mapM (wrapLocM tcRule) decls
53
54 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
55 tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
56   = addErrCtxt (ruleCtxt name)  $
57     do { traceTc "---- Rule ------" (ppr name)
58
59         -- Note [Typechecking rules]
60        ; vars <- tcRuleBndrs hs_bndrs
61        ; let (id_bndrs, tv_bndrs) = partition isId vars
62        ; (lhs', lhs_lie, rhs', rhs_lie, _rule_ty)
63             <- tcExtendTyVarEnv tv_bndrs $
64                tcExtendIdEnv id_bndrs $
65                do { ((lhs', rule_ty), lhs_lie) <- captureConstraints (tcInferRho lhs)
66                   ; (rhs', rhs_lie) <- captureConstraints (tcMonoExpr rhs rule_ty)
67                   ; return (lhs', lhs_lie, rhs', rhs_lie, rule_ty) }
68
69        ; (lhs_dicts, lhs_ev_binds, rhs_ev_binds) 
70              <- simplifyRule name tv_bndrs lhs_lie rhs_lie
71
72         -- IMPORTANT!  We *quantify* over any dicts that appear in the LHS
73         -- Reason: 
74         --      (a) The particular dictionary isn't important, because its value
75         --         depends only on the type
76         --              e.g     gcd Int $fIntegralInt
77         --         Here we'd like to match against (gcd Int any_d) for any 'any_d'
78         --
79         --      (b) We'd like to make available the dictionaries bound 
80         --          on the LHS in the RHS, so quantifying over them is good
81         --          See the 'lhs_dicts' in tcSimplifyAndCheck for the RHS
82
83         -- We quantify over any tyvars free in *either* the rule
84         --  *or* the bound variables.  The latter is important.  Consider
85         --      ss (x,(y,z)) = (x,z)
86         --      RULE:  forall v. fst (ss v) = fst v
87         -- The type of the rhs of the rule is just a, but v::(a,(b,c))
88         --
89         -- We also need to get the free tyvars of the LHS; but we do that
90         -- during zonking (see TcHsSyn.zonkRule)
91
92        ; let tpl_ids    = lhs_dicts ++ id_bndrs
93 {-
94              forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
95
96              -- Now figure out what to quantify over
97              -- c.f. TcSimplify.simplifyInfer
98        ; zonked_forall_tvs <- zonkTyVarsAndFV forall_tvs
99        ; gbl_tvs           <- tcGetGlobalTyVars      -- Already zonked
100        ; let extra_bound_tvs = zonked_forall_tvs             
101                                `minusVarSet` gbl_tvs
102                                `delVarSetList` tv_bndrs
103        ; qtvs <- zonkQuantifiedTyVars (varSetElems extra_bound_tvs)
104        ; let all_tvs = tv_bndrs ++ qtvs
105        ; (kvs, _kinds) <- kindGeneralizeKinds $ map tyVarKind all_tvs
106 -}
107
108               -- The tv_bndrs are already skolems, so no need to zonk them
109        ; return (HsRule name act
110                     (map (RuleBndr . noLoc) (tv_bndrs ++ tpl_ids))
111                     (mkHsDictLet lhs_ev_binds lhs') fv_lhs
112                     (mkHsDictLet rhs_ev_binds rhs') fv_rhs) }
113
114 tcRuleBndrs :: [RuleBndr Name] -> TcM [Var]
115 tcRuleBndrs [] 
116   = return []
117 tcRuleBndrs (RuleBndr var : rule_bndrs)
118   = do  { ty <- newFlexiTyVarTy openTypeKind
119         ; vars <- tcRuleBndrs rule_bndrs
120         ; return (mkLocalId (unLoc var) ty : vars) }
121 tcRuleBndrs (RuleBndrSig var rn_ty : rule_bndrs)
122 --  e.g         x :: a->a
123 --  The tyvar 'a' is brought into scope first, just as if you'd written
124 --              a::*, x :: a->a
125   = do  { let ctxt = FunSigCtxt (unLoc var)
126         ; (tyvars, ty) <- tcHsPatSigType ctxt rn_ty
127         ; let (subst, skol_tvs) = tcSuperSkolTyVars tyvars
128               id_ty = substTy subst ty
129               id = mkLocalId (unLoc var) id_ty
130
131               -- The type variables scope over subsequent bindings; yuk
132         ; vars <- tcExtendTyVarEnv skol_tvs $ 
133                   tcRuleBndrs rule_bndrs 
134         ; return (skol_tvs ++ id : vars) }
135
136 ruleCtxt :: FastString -> SDoc
137 ruleCtxt name = ptext (sLit "When checking the transformation rule") <+> 
138                 doubleQuotes (ftext name)
139 \end{code}