[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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by goldfire:

@@ -8,1 +8,1 @@
- But the example shows that the new expressiveness is not expressive
+ But this example shows that the new expressiveness is not expressive
@@ -10,0 +10,23 @@
+
+ {{{
+ 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
+ }}}

New description:

 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!

 {{{
 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
 }}}

 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler