Implement Partial Type Signatures
[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 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 TcEvidence( TcEvBinds(..) )
20 import Type
21 import Id
22 import Name
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 Note [Simplifying RULE constraints]
46 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
47 On the LHS of transformation rules we only simplify only equalities,
48 but not dictionaries.  We want to keep dictionaries unsimplified, to
49 serve as the available stuff for the RHS of the rule.  We *do* want to
50 simplify equalities, however, to detect ill-typed rules that cannot be
51 applied.
52
53 Implementation: the TcSFlags carried by the TcSMonad controls the
54 amount of simplification, so simplifyRuleLhs just sets the flag
55 appropriately.
56
57 Example.  Consider the following left-hand side of a rule
58         f (x == y) (y > z) = ...
59 If we typecheck this expression we get constraints
60         d1 :: Ord a, d2 :: Eq a
61 We do NOT want to "simplify" to the LHS
62         forall x::a, y::a, z::a, d1::Ord a.
63           f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
64 Instead we want
65         forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
66           f ((==) d2 x y) ((>) d1 y z) = ...
67
68 Here is another example:
69         fromIntegral :: (Integral a, Num b) => a -> b
70         {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
71 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
72 we *dont* want to get
73         forall dIntegralInt.
74            fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
75 because the scsel will mess up RULE matching.  Instead we want
76         forall dIntegralInt, dNumInt.
77           fromIntegral Int Int dIntegralInt dNumInt = id Int
78
79 Even if we have
80         g (x == y) (y == z) = ..
81 where the two dictionaries are *identical*, we do NOT WANT
82         forall x::a, y::a, z::a, d1::Eq a
83           f ((==) d1 x y) ((>) d1 y z) = ...
84 because that will only match if the dict args are (visibly) equal.
85 Instead we want to quantify over the dictionaries separately.
86
87 In short, simplifyRuleLhs must *only* squash equalities, leaving
88 all dicts unchanged, with absolutely no sharing.
89
90 Also note that we can't solve the LHS constraints in isolation:
91 Example   foo :: Ord a => a -> a
92           foo_spec :: Int -> Int
93           {-# RULE "foo"  foo = foo_spec #-}
94 Here, it's the RHS that fixes the type variable
95
96 HOWEVER, under a nested implication things are different
97 Consider
98   f :: (forall a. Eq a => a->a) -> Bool -> ...
99   {-# RULES "foo" forall (v::forall b. Eq b => b->b).
100        f b True = ...
101     #-}
102 Here we *must* solve the wanted (Eq a) from the given (Eq a)
103 resulting from skolemising the agument type of g.  So we
104 revert to SimplCheck when going under an implication.
105
106
107 ------------------------ So the plan is this -----------------------
108
109 * Step 1: Simplify the LHS and RHS constraints all together in one bag
110           We do this to discover all unification equalities
111
112 * Step 2: Zonk the ORIGINAL lhs constraints, and partition them into
113           the ones we will quantify over, and the others
114
115 * Step 3: Decide on the type variables to quantify over
116
117 * Step 4: Simplify the LHS and RHS constraints separately, using the
118           quantified constraints as givens
119
120
121 \begin{code}
122 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
123 tcRules decls = mapM (wrapLocM tcRule) decls
124
125 tcRule :: RuleDecl Name -> TcM (RuleDecl TcId)
126 tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
127   = addErrCtxt (ruleCtxt $ unLoc name)  $
128     do { traceTc "---- Rule ------" (ppr name)
129
130         -- Note [Typechecking rules]
131        ; vars <- tcRuleBndrs hs_bndrs
132        ; let (id_bndrs, tv_bndrs) = partition isId vars
133        ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
134             <- tcExtendTyVarEnv tv_bndrs $
135                tcExtendIdEnv    id_bndrs $
136                do { ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
137                   ; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
138                   ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
139
140        ; (lhs_evs, other_lhs_wanted) <- simplifyRule (unLoc name) lhs_wanted
141                                                      rhs_wanted
142
143         -- Now figure out what to quantify over
144         -- c.f. TcSimplify.simplifyInfer
145         -- We quantify over any tyvars free in *either* the rule
146         --  *or* the bound variables.  The latter is important.  Consider
147         --      ss (x,(y,z)) = (x,z)
148         --      RULE:  forall v. fst (ss v) = fst v
149         -- The type of the rhs of the rule is just a, but v::(a,(b,c))
150         --
151         -- We also need to get the completely-uconstrained tyvars of
152         -- the LHS, lest they otherwise get defaulted to Any; but we do that
153         -- during zonking (see TcHsSyn.zonkRule)
154
155        ; let tpl_ids    = lhs_evs ++ id_bndrs
156              forall_tvs = tyVarsOfTypes (rule_ty : map idType tpl_ids)
157        ; gbls  <- tcGetGlobalTyVars   -- Even though top level, there might be top-level
158                                       -- monomorphic bindings from the MR; test tc111
159        ; qtkvs <- quantifyTyVars gbls forall_tvs
160        ; traceTc "tcRule" (vcat [ doubleQuotes (ftext $ unLoc name)
161                                 , ppr forall_tvs
162                                 , ppr qtkvs
163                                 , ppr rule_ty
164                                 , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
165                   ])
166
167            -- Simplify the RHS constraints
168        ; lcl_env <- getLclEnv
169        ; rhs_binds_var <- newTcEvBinds
170        ; emitImplication $ Implic { ic_untch  = noUntouchables
171                                   , ic_skols  = qtkvs
172                                   , ic_no_eqs = False
173                                   , ic_given  = lhs_evs
174                                   , ic_wanted = rhs_wanted
175                                   , ic_insol  = insolubleWC rhs_wanted
176                                   , ic_binds  = rhs_binds_var
177                                   , ic_info   = RuleSkol (unLoc name)
178                                   , ic_env    = lcl_env }
179
180            -- For the LHS constraints we must solve the remaining constraints
181            -- (a) so that we report insoluble ones
182            -- (b) so that we bind any soluble ones
183        ; lhs_binds_var <- newTcEvBinds
184        ; emitImplication $ Implic { ic_untch  = noUntouchables
185                                   , ic_skols  = qtkvs
186                                   , ic_no_eqs = False
187                                   , ic_given  = lhs_evs
188                                   , ic_wanted = other_lhs_wanted
189                                   , ic_insol  = insolubleWC other_lhs_wanted
190                                   , ic_binds  = lhs_binds_var
191                                   , ic_info   = RuleSkol (unLoc name)
192                                   , ic_env    = lcl_env }
193
194        ; return (HsRule name act
195                     (map (noLoc . RuleBndr . noLoc) (qtkvs ++ tpl_ids))
196                     (mkHsDictLet (TcEvBinds lhs_binds_var) lhs') fv_lhs
197                     (mkHsDictLet (TcEvBinds rhs_binds_var) rhs') fv_rhs) }
198
199 tcRuleBndrs :: [LRuleBndr Name] -> TcM [Var]
200 tcRuleBndrs []
201   = return []
202 tcRuleBndrs (L _ (RuleBndr (L _ name)) : rule_bndrs)
203   = do  { ty <- newFlexiTyVarTy openTypeKind
204         ; vars <- tcRuleBndrs rule_bndrs
205         ; return (mkLocalId name ty : vars) }
206 tcRuleBndrs (L _ (RuleBndrSig (L _ name) rn_ty) : rule_bndrs)
207 --  e.g         x :: a->a
208 --  The tyvar 'a' is brought into scope first, just as if you'd written
209 --              a::*, x :: a->a
210   = do  { let ctxt = RuleSigCtxt name
211         ; (id_ty, tv_prs, _) <- tcHsPatSigType ctxt rn_ty
212         ; let id  = mkLocalId name id_ty
213               tvs = map snd tv_prs
214                     -- tcHsPatSigType returns (Name,TyVar) pairs
215                     -- for for RuleSigCtxt their Names are not
216                     -- cloned, so we get (n, tv-with-name-n) pairs
217                     -- See Note [Pattern signature binders] in TcHsType
218
219               -- The type variables scope over subsequent bindings; yuk
220         ; vars <- tcExtendTyVarEnv tvs $
221                   tcRuleBndrs rule_bndrs
222         ; return (tvs ++ id : vars) }
223
224 ruleCtxt :: FastString -> SDoc
225 ruleCtxt name = ptext (sLit "When checking the transformation rule") <+>
226                 doubleQuotes (ftext name)
227 \end{code}