#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