Simplify axioms; should be applied to types

Simon PJ says:

In Note [Coercion axioms applied to coercions] in Coercion, we find the justification for allowing coercions as arguments to axioms. The goal is to add a bit of extra expressiveness, so that optimisations can be done pair-wise.

But this example shows that the new expressiveness is not expressive enough, given the apartness restrictions on closed type families. (The goal is to eliminate the call to checkAxInstCo in !OptCoercion.)

type family F (a :: *) (b :: *) where
 F a a = Int
 F a b = b

type family Id (a :: *) where
 Id a = a

----------------------

axF :: { [a::*].       F a a ~ Int
       ; [a::*, b::*]. F a b ~ b }
axId :: [a::*]. Id a ~ a

co1 = axF[1] (axId[0] <Int>) (axId[0] <Bool>)
 :: F (Id Int) (Id Bool) ~ Bool
co2 = sym (axId[0] <Bool>)
 :: Bool ~ Id Bool

co3 = co1 ; co2 :: F (Id Int) (Id Bool) ~ Id Bool
co3' = optimized co3 = axF[1] (axId[0] <Int>) <Id Bool>  -- bogus, fails call to checkAxInstCo

This last co3' is what would be produced if we didn't run checkAxInstCo. But, as the comment says, it runs afoul of the apartness condition (as checked by checkAxInstCo). Currently, !OptCoercion just gives up in this case, retaining the original co3.

Rather than give up (as you do in !OptCoercion) maybe we should re-examine the assumption. How could we optimise if axioms could only be instantiated with types, not coercions. Which would be a LOT simpler!

Let's take the example from the Note:

 C a : t[a] ~ F a
 g   : b ~ c

and we want to optimize

 sym (C b) ; t[g] ; C c    ::   F b ~ F c

One possibility is to perform a 3-component optimisation, but that's a bit horrible. But what about this: push the t[g] past the axiom rather than into it. For example

 t[g] ; C c  ==>  C b ; F g
  where
    t[g] : t[b]~t[c]
    C c  : t[c] ~ F c

If we use this to move axioms to the right, I think we'll get the same optimisations as now, but with a simpler system. Does that seem right?

Now it becomes clearer that you can't always commute the things.

  ax : F a a ~ a;
       F a b ~ b

  co :: Id Bool ~ Bool

If we have

	(F <Int> co ; ax[1] Int Bool)  :  F Int (Id Bool) ~ Bool

then we might try to commute co past the axiom thus:

	ax[1] Int (Id Bool) ; co 

but now (as you point out) the ax[1] is not necessarily OK; so we still need to use checkAxInstCo. But I hazard that the lack of the commuting isn't going to lose useful optimisations.

So in some ways we are no further forward (an optimisation is only sometimes OK), but I feel MUCH happier about simplifying the axiom-applied-to-coercion stuff.