typos
[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, checkAxInstCo ) 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 CoAxiom
22 import Var
23 import VarSet
24 import VarEnv
25 import StaticFlags      ( opt_NoOptCoercion )
26 import Outputable
27 import Pair
28 import Maybes( allMaybes )
29 import FastString
30 import Util
31 import Unify
32 import InstEnv
33 \end{code}
34
35 %************************************************************************
36 %*                                                                      *
37                  Optimising coercions                                                                   
38 %*                                                                      *
39 %************************************************************************
40
41 Note [Subtle shadowing in coercions]
42 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
43 Supose we optimising a coercion
44     optCoercion (forall (co_X5:t1~t2). ...co_B1...)
45 The co_X5 is a wild-card; the bound variable of a coercion for-all
46 should never appear in the body of the forall. Indeed we often
47 write it like this
48     optCoercion ( (t1~t2) => ...co_B1... )
49
50 Just because it's a wild-card doesn't mean we are free to choose
51 whatever variable we like.  For example it'd be wrong for optCoercion
52 to return
53    forall (co_B1:t1~t2). ...co_B1...
54 because now the co_B1 (which is really free) has been captured, and
55 subsequent substitutions will go wrong.  That's why we can't use
56 mkCoPredTy in the ForAll case, where this note appears.  
57
58 \begin{code}
59 optCoercion :: CvSubst -> Coercion -> NormalCo
60 -- ^ optCoercion applies a substitution to a coercion, 
61 --   *and* optimises it to reduce its size
62 optCoercion env co 
63   | opt_NoOptCoercion = substCo env co
64   | otherwise         = opt_co env False co
65
66 type NormalCo = Coercion
67   -- Invariants: 
68   --  * The substitution has been fully applied
69   --  * For trans coercions (co1 `trans` co2)
70   --       co1 is not a trans, and neither co1 nor co2 is identity
71   --  * If the coercion is the identity, it has no CoVars of CoTyCons in it (just types)
72
73 type NormalNonIdCo = NormalCo  -- Extra invariant: not the identity
74
75 opt_co, opt_co' :: CvSubst
76                 -> Bool        -- True <=> return (sym co)
77                 -> Coercion
78                 -> NormalCo     
79 opt_co = opt_co'
80 {-
81 opt_co env sym co
82  = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $
83    co1 `seq`
84    pprTrace "opt_co done }" (ppr co1) $
85    (WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (Pair s1 t1)
86                          $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )
87     WARN( not (coreEqCoercion co1 simple_result),
88            (text "env=" <+> ppr env) $$
89            (text "input=" <+> ppr co) $$
90            (text "simple=" <+> ppr simple_result) $$
91            (text "opt=" <+> ppr co1) )
92    co1)
93  where
94    co1 = opt_co' env sym co
95    same_co_kind = s1 `eqType` s2 && t1 `eqType` t2
96    Pair s t = coercionKind (substCo env co)
97    (s1,t1) | sym = (t,s)
98            | otherwise = (s,t)
99    Pair s2 t2 = coercionKind co1
100
101    simple_result | sym = mkSymCo (substCo env co)
102                  | otherwise = substCo env co
103 -}
104
105 opt_co' env _   (Refl ty)           = Refl (substTy env ty)
106 opt_co' env sym (SymCo co)          = opt_co env (not sym) co
107 opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)
108 opt_co' env sym (AppCo co1 co2)     = mkAppCo (opt_co env sym co1) (opt_co env sym co2)
109 opt_co' env sym (ForAllCo tv co)    = case substTyVarBndr env tv of
110                                          (env', tv') -> mkForAllCo tv' (opt_co env' sym co)
111      -- Use the "mk" functions to check for nested Refls
112
113 opt_co' env sym (CoVarCo cv)
114   | Just co <- lookupCoVar env cv
115   = opt_co (zapCvSubstEnv env) sym co
116
117   | Just cv1 <- lookupInScope (getCvInScope env) cv
118   = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)
119                 -- cv1 might have a substituted kind!
120
121   | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
122                 ASSERT( isCoVar cv )
123                 wrapSym sym (CoVarCo cv)
124
125 opt_co' env sym (AxiomInstCo con ind cos)
126     -- Do *not* push sym inside top-level axioms
127     -- e.g. if g is a top-level axiom
128     --   g a : f a ~ a
129     -- then (sym (g ty)) /= g (sym ty) !!
130   = wrapSym sym $ AxiomInstCo con ind (map (opt_co env False) cos)
131       -- Note that the_co does *not* have sym pushed into it
132
133 opt_co' env sym (UnsafeCo ty1 ty2)
134   | ty1' `eqType` ty2' = Refl ty1'
135   | sym                = mkUnsafeCo ty2' ty1'
136   | otherwise          = mkUnsafeCo ty1' ty2'
137   where
138     ty1' = substTy env ty1
139     ty2' = substTy env ty2
140
141 opt_co' env sym (TransCo co1 co2)
142   | sym       = opt_trans in_scope opt_co2 opt_co1   -- sym (g `o` h) = sym h `o` sym g
143   | otherwise = opt_trans in_scope opt_co1 opt_co2
144   where
145     opt_co1 = opt_co env sym co1
146     opt_co2 = opt_co env sym co2
147     in_scope = getCvInScope env
148
149 opt_co' env sym (NthCo n co)
150   | TyConAppCo tc cos <- co'
151   , isDecomposableTyCon tc   -- Not synonym families
152   = ASSERT( n < length cos )
153     cos !! n
154   | otherwise
155   = NthCo n co'
156   where
157     co' = opt_co env sym co
158
159 opt_co' env sym (LRCo lr co)
160   | Just pr_co <- splitAppCo_maybe co'
161   = pickLR lr pr_co
162   | otherwise
163   = LRCo lr co'
164   where
165     co' = opt_co env sym co
166
167 opt_co' env sym (InstCo co ty)
168     -- See if the first arg is already a forall
169     -- ...then we can just extend the current substitution
170   | Just (tv, co_body) <- splitForAllCo_maybe co
171   = opt_co (extendTvSubst env tv ty') sym co_body
172
173      -- See if it is a forall after optimization
174      -- If so, do an inefficient one-variable substitution
175   | Just (tv, co'_body) <- splitForAllCo_maybe co'
176   = substCoWithTy (getCvInScope env) tv ty' co'_body   
177
178   | otherwise = InstCo co' ty'
179   where
180     co' = opt_co env sym co
181     ty' = substTy env ty
182
183 -------------
184 opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
185 opt_transList is = zipWith (opt_trans is)
186
187 opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
188 opt_trans is co1 co2
189   | isReflCo co1 = co2
190   | otherwise    = opt_trans1 is co1 co2
191
192 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
193 -- First arg is not the identity
194 opt_trans1 is co1 co2
195   | isReflCo co2 = co1
196   | otherwise    = opt_trans2 is co1 co2
197
198 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
199 -- Neither arg is the identity
200 opt_trans2 is (TransCo co1a co1b) co2
201     -- Don't know whether the sub-coercions are the identity
202   = opt_trans is co1a (opt_trans is co1b co2)  
203
204 opt_trans2 is co1 co2 
205   | Just co <- opt_trans_rule is co1 co2
206   = co
207
208 opt_trans2 is co1 (TransCo co2a co2b)
209   | Just co1_2a <- opt_trans_rule is co1 co2a
210   = if isReflCo co1_2a
211     then co2b
212     else opt_trans1 is co1_2a co2b
213
214 opt_trans2 _ co1 co2
215   = mkTransCo co1 co2
216
217 ------
218 -- Optimize coercions with a top-level use of transitivity.
219 opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
220
221 -- Push transitivity through matching destructors
222 opt_trans_rule is in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)
223   | d1 == d2
224   , co1 `compatible_co` co2
225   = fireTransRule "PushNth" in_co1 in_co2 $
226     mkNthCo d1 (opt_trans is co1 co2)
227
228 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
229   | d1 == d2
230   , co1 `compatible_co` co2
231   = fireTransRule "PushLR" in_co1 in_co2 $
232     mkLRCo d1 (opt_trans is co1 co2)
233
234 -- Push transitivity inside instantiation
235 opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
236   | ty1 `eqType` ty2
237   , co1 `compatible_co` co2
238   = fireTransRule "TrPushInst" in_co1 in_co2 $
239     mkInstCo (opt_trans is co1 co2) ty1
240  
241 -- Push transitivity down through matching top-level constructors.
242 opt_trans_rule is in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)
243   | tc1 == tc2 
244   = fireTransRule "PushTyConApp" in_co1 in_co2 $
245     TyConAppCo tc1 (opt_transList is cos1 cos2)
246
247 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
248   = fireTransRule "TrPushApp" in_co1 in_co2 $
249     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
250
251 -- Eta rules
252 opt_trans_rule is co1@(TyConAppCo tc cos1) co2
253   | Just cos2 <- etaTyConAppCo_maybe tc co2
254   = ASSERT( length cos1 == length cos2 )
255     fireTransRule "EtaCompL" co1 co2 $
256     TyConAppCo tc (opt_transList is cos1 cos2)
257
258 opt_trans_rule is co1 co2@(TyConAppCo tc cos2)
259   | Just cos1 <- etaTyConAppCo_maybe tc co1
260   = ASSERT( length cos1 == length cos2 )
261     fireTransRule "EtaCompR" co1 co2 $
262     TyConAppCo tc (opt_transList is cos1 cos2)
263
264 opt_trans_rule is co1@(AppCo co1a co1b) co2
265   | Just (co2a,co2b) <- etaAppCo_maybe co2
266   = fireTransRule "EtaAppL" co1 co2 $
267     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
268
269 opt_trans_rule is co1 co2@(AppCo co2a co2b)
270   | Just (co1a,co1b) <- etaAppCo_maybe co1
271   = fireTransRule "EtaAppR" co1 co2 $
272     mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
273
274 -- Push transitivity inside forall
275 opt_trans_rule is co1 co2
276   | Just (tv1,r1) <- splitForAllCo_maybe co1
277   , Just (tv2,r2) <- etaForAllCo_maybe co2
278   , let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
279         is' = is `extendInScopeSet` tv1
280   = fireTransRule "EtaAllL" co1 co2 $
281     mkForAllCo tv1 (opt_trans2 is' r1 r2')
282
283   | Just (tv2,r2) <- splitForAllCo_maybe co2
284   , Just (tv1,r1) <- etaForAllCo_maybe co1
285   , let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
286         is' = is `extendInScopeSet` tv2
287   = fireTransRule "EtaAllR" co1 co2 $
288     mkForAllCo tv1 (opt_trans2 is' r1' r2)
289
290 -- Push transitivity inside axioms
291 opt_trans_rule is co1 co2
292
293   -- TrPushSymAxR
294   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
295   , Just cos2 <- matchAxiom sym con ind co2
296   , True <- sym
297   , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
298   , Nothing <- checkAxInstCo newAxInst
299   = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
300
301   -- TrPushAxR
302   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
303   , Just cos2 <- matchAxiom sym con ind co2
304   , False <- sym
305   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
306   , Nothing <- checkAxInstCo newAxInst
307   = fireTransRule "TrPushAxR" co1 co2 newAxInst
308
309   -- TrPushSymAxL
310   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
311   , Just cos1 <- matchAxiom (not sym) con ind co1
312   , True <- sym
313   , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
314   , Nothing <- checkAxInstCo newAxInst
315   = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
316
317   -- TrPushAxL  
318   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
319   , Just cos1 <- matchAxiom (not sym) con ind co1
320   , False <- sym
321   , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
322   , Nothing <- checkAxInstCo newAxInst
323   = fireTransRule "TrPushAxL" co1 co2 newAxInst
324
325   -- TrPushAxSym/TrPushSymAx
326   | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
327   , Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
328   , con1 == con2
329   , ind1 == ind2
330   , sym1 == not sym2
331   , let branch = coAxiomNthBranch con1 ind1
332         qtvs = coAxBranchTyVars branch
333         lhs  = coAxNthLHS con1 ind1
334         rhs  = coAxBranchRHS branch
335         pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)
336   , all (`elemVarSet` pivot_tvs) qtvs
337   = fireTransRule "TrPushAxSym" co1 co2 $
338     if sym2
339     then liftCoSubstWith qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs  -- TrPushAxSym
340     else liftCoSubstWith qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs  -- TrPushSymAx
341   where
342     co1_is_axiom_maybe = isAxiom_maybe co1
343     co2_is_axiom_maybe = isAxiom_maybe co2
344
345 opt_trans_rule _ co1 co2        -- Identity rule
346   | Pair ty1 _ <- coercionKind co1
347   , Pair _ ty2 <- coercionKind co2
348   , ty1 `eqType` ty2
349   = fireTransRule "RedTypeDirRefl" co1 co2 $
350     Refl ty2
351
352 opt_trans_rule _ _ _ = Nothing
353
354 fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
355 fireTransRule _rule _co1 _co2 res
356   = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
357     Just res
358
359 \end{code}
360
361 Note [Conflict checking with AxiomInstCo]
362 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
363 Consider the following type family and axiom:
364
365 type family Equal (a :: k) (b :: k) :: Bool
366 type instance where
367   Equal a a = True
368   Equal a b = False
369 --
370 Equal :: forall k::BOX. k -> k -> Bool
371 axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
372            ; forall k::BOX. forall a::k. forall b::k. Equal k a b ~ False }
373
374 We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is 0-based,
375 so this is the second branch of the axiom.) The problem is that, on the surface, it
376 seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ False) and that all is
377 OK. But, all is not OK: we want to use the first branch of the axiom in this case,
378 not the second. The problem is that the parameters of the first branch can unify with
379 the supplied coercions, thus meaning that the first branch should be taken. See also
380 Note [Instance checking within groups] in types/FamInstEnv.lhs.
381
382 \begin{code}
383 -- | Check to make sure that an AxInstCo is internally consistent.
384 -- Returns the number of the conflicting branch, if it exists
385 -- See Note [Conflict checking with AxiomInstCo]
386 checkAxInstCo :: Coercion -> Maybe Int
387 -- defined here to avoid dependencies in Coercion
388 checkAxInstCo (AxiomInstCo ax ind cos)
389   = let branch = coAxiomNthBranch ax ind
390         tvs = coAxBranchTyVars branch
391         tys = map (pFst . coercionKind) cos 
392         subst = zipOpenTvSubst tvs tys
393         lhs' = Type.substTys subst (coAxBranchLHS branch) in
394     check_no_conflict lhs' (ind-1)
395   where
396     check_no_conflict :: [Type] -> Int -> Maybe Int
397     check_no_conflict _ (-1) = Nothing
398     check_no_conflict lhs' j
399       | SurelyApart <- tcApartTys instanceBindFun lhs' lhsj
400       = check_no_conflict lhs' (j-1)
401       | otherwise
402       = Just j
403       where
404         (CoAxBranch { cab_lhs = lhsj }) = coAxiomNthBranch ax j
405 checkAxInstCo _ = Nothing
406
407 -----------
408 wrapSym :: Bool -> Coercion -> Coercion
409 wrapSym sym co | sym       = SymCo co
410                | otherwise = co
411
412 -----------
413 isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
414 isAxiom_maybe (SymCo co) 
415   | Just (sym, con, ind, cos) <- isAxiom_maybe co
416   = Just (not sym, con, ind, cos)
417 isAxiom_maybe (AxiomInstCo con ind cos)
418   = Just (False, con, ind, cos)
419 isAxiom_maybe _ = Nothing
420
421 matchAxiom :: Bool -- True = match LHS, False = match RHS
422            -> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
423 -- If we succeed in matching, then *all the quantified type variables are bound*
424 -- E.g.   if tvs = [a,b], lhs/rhs = [b], we'll fail
425 matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
426   = let (CoAxBranch { cab_tvs = qtvs
427                     , cab_lhs = lhs
428                     , cab_rhs = rhs }) = coAxiomNthBranch ax ind in
429     case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
430       Nothing    -> Nothing
431       Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)
432
433 -------------
434 compatible_co :: Coercion -> Coercion -> Bool
435 -- Check whether (co1 . co2) will be well-kinded
436 compatible_co co1 co2
437   = x1 `eqType` x2              
438   where
439     Pair _ x1 = coercionKind co1
440     Pair x2 _ = coercionKind co2
441
442 -------------
443 etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
444 -- Try to make the coercion be of form (forall tv. co)
445 etaForAllCo_maybe co
446   | Just (tv, r) <- splitForAllCo_maybe co
447   = Just (tv, r)
448
449   | Pair ty1 ty2  <- coercionKind co
450   , Just (tv1, _) <- splitForAllTy_maybe ty1
451   , Just (tv2, _) <- splitForAllTy_maybe ty2
452   , tyVarKind tv1 `eqKind` tyVarKind tv2
453   = Just (tv1, mkInstCo co (mkTyVarTy tv1))
454
455   | otherwise
456   = Nothing
457
458 etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
459 -- If possible, split a coercion
460 --   g :: t1a t1b ~ t2a t2b
461 -- into a pair of coercions (left g, right g)
462 etaAppCo_maybe co
463   | Just (co1,co2) <- splitAppCo_maybe co
464   = Just (co1,co2)
465   | Pair ty1 ty2 <- coercionKind co
466   , Just (_,t1) <- splitAppTy_maybe ty1
467   , Just (_,t2) <- splitAppTy_maybe ty2
468   , typeKind t1 `eqType` typeKind t2      -- Note [Eta for AppCo]
469   = Just (LRCo CLeft co, LRCo CRight co)
470   | otherwise
471   = Nothing
472
473 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
474 -- If possible, split a coercion 
475 --       g :: T s1 .. sn ~ T t1 .. tn
476 -- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] 
477 etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)
478   = ASSERT( tc == tc2 ) Just cos2
479
480 etaTyConAppCo_maybe tc co
481   | isDecomposableTyCon tc
482   , Pair ty1 ty2     <- coercionKind co
483   , Just (tc1, tys1) <- splitTyConApp_maybe ty1
484   , Just (tc2, tys2) <- splitTyConApp_maybe ty2
485   , tc1 == tc2
486   , let n = length tys1
487   = ASSERT( tc == tc1 ) 
488     ASSERT( n == length tys2 )
489     Just (decomposeCo n co)  
490     -- NB: n might be <> tyConArity tc
491     -- e.g.   data family T a :: * -> *
492     --        g :: T a b ~ T c d
493
494   | otherwise
495   = Nothing
496 \end{code}  
497
498 Note [Eta for AppCo]
499 ~~~~~~~~~~~~~~~~~~~~
500 Suppose we have 
501    g :: s1 t1 ~ s2 t2
502
503 Then we can't necessarily make
504    left  g :: s1 ~ s2
505    right g :: t1 ~ t2
506 because it's possible that
507    s1 :: * -> *         t1 :: *
508    s2 :: (*->*) -> *    t2 :: * -> *
509 and in that case (left g) does not have the same
510 kind on either side.
511
512 It's enough to check that 
513   kind t1 = kind t2
514 because if g is well-kinded then
515   kind (s1 t2) = kind (s2 t2)
516 and these two imply
517   kind s1 = kind s2
518