Merge branch 'master' of http://darcs.haskell.org/ghc
[ghc.git] / compiler / types / OptCoercion.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 module OptCoercion ( optCoercion ) where 
7
8 #include "HsVersions.h"
9
10 import Coercion
11 import Type hiding( substTyVarBndr, substTy, extendTvSubst )
12 import TyCon
13 import Var
14 import VarSet
15 import VarEnv
16 import StaticFlags      ( opt_NoOptCoercion )
17 import Outputable
18 import Pair
19 import Maybes( allMaybes )
20 import FastString
21 \end{code}
22
23 %************************************************************************
24 %*                                                                      *
25                  Optimising coercions                                                                   
26 %*                                                                      *
27 %************************************************************************
28
29 Note [Subtle shadowing in coercions]
30 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
31 Supose we optimising a coercion
32     optCoercion (forall (co_X5:t1~t2). ...co_B1...)
33 The co_X5 is a wild-card; the bound variable of a coercion for-all
34 should never appear in the body of the forall. Indeed we often
35 write it like this
36     optCoercion ( (t1~t2) => ...co_B1... )
37
38 Just because it's a wild-card doesn't mean we are free to choose
39 whatever variable we like.  For example it'd be wrong for optCoercion
40 to return
41    forall (co_B1:t1~t2). ...co_B1...
42 because now the co_B1 (which is really free) has been captured, and
43 subsequent substitutions will go wrong.  That's why we can't use
44 mkCoPredTy in the ForAll case, where this note appears.  
45
46 \begin{code}
47 optCoercion :: CvSubst -> Coercion -> NormalCo
48 -- ^ optCoercion applies a substitution to a coercion, 
49 --   *and* optimises it to reduce its size
50 optCoercion env co 
51   | opt_NoOptCoercion = substCo env co
52   | otherwise         = opt_co env False co
53
54 type NormalCo = Coercion
55   -- Invariants: 
56   --  * The substitution has been fully applied
57   --  * For trans coercions (co1 `trans` co2)
58   --       co1 is not a trans, and neither co1 nor co2 is identity
59   --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
60
61 type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
62
63 opt_co, opt_co' :: CvSubst
64                 -> Bool        -- True <=> return (sym co)
65                 -> Coercion
66                 -> NormalCo     
67 opt_co = opt_co'
68 {-
69 opt_co env sym co
70  = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
71    co1 `seq`
72    pprTrace "opt_co done }" (ppr co1) $
73    (WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (Pair s1 t1)
74                          $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )
75     WARN( not (coreEqCoercion co1 simple_result),
76            (text "env=" <+> ppr env) $$
77            (text "input=" <+> ppr co) $$
78            (text "simple=" <+> ppr simple_result) $$
79            (text "opt=" <+> ppr co1) )
80    co1)
81  where
82    co1 = opt_co' env sym co
83    same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
84    Pair s t = coercionKind (substCo env co)
85    (s1,t1) | sym = (t,s)
86            | otherwise = (s,t)
87    Pair s2 t2 = coercionKind co1
88
89    simple_result | sym = mkSymCo (substCo env co)
90                  | otherwise = substCo env co
91 -}
92
93 opt_co' env _   (Refl ty)           = Refl (substTy env ty)
94 opt_co' env sym (SymCo co)          = opt_co env (not sym) co
95 opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)
96 opt_co' env sym (AppCo co1 co2)     = mkAppCo (opt_co env sym co1) (opt_co env sym co2)
97 opt_co' env sym (ForAllCo tv co)    = case substTyVarBndr env tv of
98                                          (env', tv') -> mkForAllCo tv' (opt_co env' sym co)
99      -- Use the "mk" functions to check for nested Refls
100
101 opt_co' env sym (CoVarCo cv)
102   | Just co <- lookupCoVar env cv
103   = opt_co (zapCvSubstEnv env) sym co
104
105   | Just cv1 <- lookupInScope (getCvInScope env) cv
106   = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)
107                 -- cv1 might have a substituted kind!
108
109   | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
110                 ASSERT( isCoVar cv )
111                 wrapSym sym (CoVarCo cv)
112
113 opt_co' env sym (AxiomInstCo con cos)
114     -- Do *not* push sym inside top-level axioms
115     -- e.g. if g is a top-level axiom
116     --   g a : f a ~ a
117     -- then (sym (g ty)) /= g (sym ty) !!
118   = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)
119       -- Note that the_co does *not* have sym pushed into it
120
121 opt_co' env sym (UnsafeCo ty1 ty2)
122   | ty1' `eqType` ty2' = Refl ty1'
123   | sym                = mkUnsafeCo ty2' ty1'
124   | otherwise          = mkUnsafeCo ty1' ty2'
125   where
126     ty1' = substTy env ty1
127     ty2' = substTy env ty2
128
129 opt_co' env sym (TransCo co1 co2)
130   | sym       = opt_trans in_scope opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
131   | otherwise = opt_trans in_scope opt_co1 opt_co2
132   where
133     opt_co1 = opt_co env sym co1
134     opt_co2 = opt_co env sym co2
135     in_scope = getCvInScope env
136
137 opt_co' env sym (NthCo n co)
138   | TyConAppCo tc cos <- co'
139   , isDecomposableTyCon tc              -- Not synonym families
140   = ASSERT( n < length cos )
141     cos !! n
142   | otherwise
143   = NthCo n co'
144   where
145     co' = opt_co env sym co
146
147 opt_co' env sym (InstCo co ty)
148     -- See if the first arg is already a forall
149     -- ...then we can just extend the current substitution
150   | Just (tv, co_body) <- splitForAllCo_maybe co
151   = opt_co (extendTvSubst env tv ty') sym co_body
152
153      -- See if it is a forall after optimization
154      -- If so, do an inefficient one-variable substitution
155   | Just (tv, co'_body) <- splitForAllCo_maybe co'
156   = substCoWithTy (getCvInScope env) tv ty' co'_body   
157
158   | otherwise = InstCo co' ty'
159
160   where
161     co' = opt_co env sym co
162     ty' = substTy env ty
163
164 -------------
165 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
166 opt_transList is = zipWith (opt_trans is)
167
168 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
169 opt_trans is co1 co2
170   | isReflCo co1 = co2
171   | otherwise    = opt_trans1 is co1 co2
172
173 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
174 -- First arg is not the identity
175 opt_trans1 is co1 co2
176   | isReflCo co2 = co1
177   | otherwise    = opt_trans2 is co1 co2
178
179 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
180 -- Neither arg is the identity
181 opt_trans2 is (TransCo co1a co1b) co2
182     -- Don't know whether the sub-coercions are the identity
183   = opt_trans is co1a (opt_trans is co1b co2)  
184
185 opt_trans2 is co1 co2 
186   | Just co <- opt_trans_rule is co1 co2
187   = co
188
189 opt_trans2 is co1 (TransCo co2a co2b)
190   | Just co1_2a <- opt_trans_rule is co1 co2a
191   = if isReflCo co1_2a
192     then co2b
193     else opt_trans1 is co1_2a co2b
194
195 opt_trans2 _ co1 co2
196   = mkTransCo co1 co2
197
198 ------
199 -- Optimize coercions with a top-level use of transitivity.
200 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
201
202 -- push transitivity down through matching top-level constructors.
203 opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
204   | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $
205                  TyConAppCo tc1 (opt_transList is cos1 cos2)
206
207 -- push transitivity through matching destructors
208 opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
209   | d1 == d2
210   , co1 `compatible_co` co2
211   = fireTransRule "PushNth" in_co1 in_co2 $
212     mkNthCo d1 (opt_trans is co1 co2)
213
214 -- Push transitivity inside instantiation
215 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
216   | ty1 `eqType` ty2
217   , co1 `compatible_co` co2
218   = fireTransRule "TrPushInst" in_co1 in_co2 $
219     mkInstCo (opt_trans is co1 co2) ty1
220  
221 -- Push transitivity inside apply
222 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
223   = fireTransRule "TrPushApp" in_co1 in_co2 $
224     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
225
226 opt_trans_rule is co1@(TyConAppCo tc cos1) co2
227   | Just cos2 <- etaTyConAppCo_maybe tc co2
228   = ASSERT( length cos1 == length cos2 )
229     fireTransRule "EtaCompL" co1 co2 $
230     TyConAppCo tc (opt_transList is cos1 cos2)
231
232 opt_trans_rule is co1 co2@(TyConAppCo tc cos2)
233   | Just cos1 <- etaTyConAppCo_maybe tc co1
234   = ASSERT( length cos1 == length cos2 )
235     fireTransRule "EtaCompR" co1 co2 $
236     TyConAppCo tc (opt_transList is cos1 cos2)
237
238 -- Push transitivity inside forall
239 opt_trans_rule is co1 co2
240   | Just (tv1,r1) <- splitForAllCo_maybe co1
241   , Just (tv2,r2) <- etaForAllCo_maybe co2
242   , let r2' = substCoWithTy is tv2 (mkTyVarTy tv1) r2
243   = fireTransRule "EtaAllL" co1 co2 $
244     mkForAllCo tv1 (opt_trans2 (extendInScopeSet is tv1) r1 r2')
245
246   | Just (tv2,r2) <- splitForAllCo_maybe co2
247   , Just (tv1,r1) <- etaForAllCo_maybe co1
248   , let r1' = substCoWithTy is tv1 (mkTyVarTy tv2) r1
249   = fireTransRule "EtaAllR" co1 co2 $
250     mkForAllCo tv1 (opt_trans2 (extendInScopeSet is tv2) r1' r2)
251
252 -- Push transitivity inside axioms
253 opt_trans_rule is co1 co2
254
255   -- TrPushAxR/TrPushSymAxR
256   | Just (sym, con, cos1) <- co1_is_axiom_maybe
257   , Just cos2 <- matchAxiom sym con co2
258   = fireTransRule "TrPushAxR" co1 co2 $
259     if sym 
260     then SymCo $ AxiomInstCo con (opt_transList is (map mkSymCo cos2) cos1)
261     else         AxiomInstCo con (opt_transList is cos1 cos2)
262
263   -- TrPushAxL/TrPushSymAxL
264   | Just (sym, con, cos2) <- co2_is_axiom_maybe
265   , Just cos1 <- matchAxiom (not sym) con co1
266   = fireTransRule "TrPushAxL" co1 co2 $
267     if sym 
268     then SymCo $ AxiomInstCo con (opt_transList is cos2 (map mkSymCo cos1))
269     else         AxiomInstCo con (opt_transList is cos1 cos2)
270
271   -- TrPushAxSym/TrPushSymAx
272   | Just (sym1, con1, cos1) <- co1_is_axiom_maybe
273   , Just (sym2, con2, cos2) <- co2_is_axiom_maybe
274   , con1 == con2
275   , sym1 == not sym2
276   , let qtvs = co_ax_tvs con1
277         lhs  = co_ax_lhs con1 
278         rhs  = co_ax_rhs con1 
279         pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
280   , all (`elemVarSet` pivot_tvs) qtvs
281   = fireTransRule "TrPushAxSym" co1 co2 $
282     if sym2
283     then liftCoSubstWith qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
284     else liftCoSubstWith qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
285   where
286     co1_is_axiom_maybe = isAxiom_maybe co1
287     co2_is_axiom_maybe = isAxiom_maybe co2
288
289 opt_trans_rule _ co1 co2        -- Identity rule
290   | Pair ty1 _ <- coercionKind co1
291   , Pair _ ty2 <- coercionKind co2
292   , ty1 `eqType` ty2
293   = fireTransRule "RedTypeDirRefl" co1 co2 $
294     Refl ty2
295
296 opt_trans_rule _ _ _ = Nothing
297
298 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
299 fireTransRule _rule _co1 _co2 res
300   = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
301     Just res
302
303 -----------
304 wrapSym :: Bool -> Coercion -> Coercion
305 wrapSym sym co | sym       = SymCo co
306                | otherwise = co
307
308 -----------
309 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom, [Coercion])
310 isAxiom_maybe (SymCo co) 
311   | Just (sym, con, cos) <- isAxiom_maybe co
312   = Just (not sym, con, cos)
313 isAxiom_maybe (AxiomInstCo con cos)
314   = Just (False, con, cos)
315 isAxiom_maybe _ = Nothing
316
317 matchAxiom :: Bool -- True = match LHS, False = match RHS
318            -> CoAxiom -> Coercion -> Maybe [Coercion]
319 -- If we succeed in matching, then *all the quantified type variables are bound*
320 -- E.g.   if tvs = [a,b], lhs/rhs = [b], we'll fail
321 matchAxiom sym (CoAxiom { co_ax_tvs = qtvs, co_ax_lhs = lhs, co_ax_rhs = rhs }) co
322   = case liftCoMatch (mkVarSet qtvs) (if sym then lhs else rhs) co of
323       Nothing    -> Nothing
324       Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)
325
326 -------------
327 compatible_co :: Coercion -> Coercion -> Bool
328 -- Check whether (co1 . co2) will be well-kinded
329 compatible_co co1 co2
330   = x1 `eqType` x2              
331   where
332     Pair _ x1 = coercionKind co1
333     Pair x2 _ = coercionKind co2
334
335 -------------
336 etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
337 -- Try to make the coercion be of form (forall tv. co)
338 etaForAllCo_maybe co
339   | Just (tv, r) <- splitForAllCo_maybe co
340   = Just (tv, r)
341
342   | Pair ty1 ty2  <- coercionKind co
343   , Just (tv1, _) <- splitForAllTy_maybe ty1
344   , Just (tv2, _) <- splitForAllTy_maybe ty2
345   , tyVarKind tv1 `eqKind` tyVarKind tv2
346   = Just (tv1, mkInstCo co (mkTyVarTy tv1))
347
348   | otherwise
349   = Nothing
350
351 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
352 -- If possible, split a coercion 
353 --       g :: T s1 .. sn ~ T t1 .. tn
354 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] 
355 etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)
356   = ASSERT( tc == tc2 ) Just cos2
357
358 etaTyConAppCo_maybe tc co
359   | isDecomposableTyCon tc
360   , Pair ty1 ty2     <- coercionKind co
361   , Just (tc1, tys1) <- splitTyConApp_maybe ty1
362   , Just (tc2, tys2) <- splitTyConApp_maybe ty2
363   , tc1 == tc2
364   , let n = length tys1
365   = ASSERT( tc == tc1 ) 
366     ASSERT( n == length tys2 )
367     Just (decomposeCo n co)  
368     -- NB: n might be <> tyConArity tc
369     -- e.g.   data family T a :: * -> *
370     --        g :: T a b ~ T c d
371
372   | otherwise
373   = Nothing
374 \end{code}