[GHC] #11739: Simplify axioms; should be applied to types

[GHC]

#11739: Simplify axioms; should be applied to types
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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 the example shows that the new expressiveness is not expressive
 enough!

 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.   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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11739>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler