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