[GHC] #8095: TypeFamilies painfully slow

[GHC]

#8095: TypeFamilies painfully slow
-------------------------------------+-------------------------------------
        Reporter:  MikeIzbicki       |                Owner:  bgamari
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  7.6.3
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  performance bug                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  5321              |  Differential Rev(s):
-------------------------------------+-------------------------------------

Comment (by goldfire):

 It has to get big, as the coercion witnesses the sequence of reductions
 that a type family makes to get to a normal form. There are roughly `N`
 steps. And each step must explicitly mention the decreasing value of `N`.
 And that's quadratic.

 Unless I'm missing something, the only way to remove the quadratic
 behavior here is to redesign Core to be less explicit. That might just be
 possible.

 Right now, we can take a coercion and ask what types it relates. We will
 always get an answer. But perhaps we can redesign things so that we ask a
 coercion what types it relates, '''and we always provide one of the
 types'''. Then some function tells us what the other type is. (This
 operation can't just be, say, left-to-right because we need `sym` to
 work.) As a really easy example, this new design means that reflexive
 coercions don't need to store their types, because one type is always the
 same as the other. In the case of axioms, getting from one type to another
 is much harder. Going left-to-right seems possible, but it will require a
 matching algorithm. Going right-to-left on non-injective type family
 axioms is not possible without some extra information, so that's annoying.
 But maybe there's a design of this feature available.

 What would be the consequences? Coercions would get smaller. Compilation
 would get faster. Core Lint would get slower. Core would get harder to
 debug, perhaps. Might be worth it.

 '''Wait! A new idea! '''

 This is actually an old idea of mine, but one I've never articulated. What
 if we just don't bother with coercions at all when `-dcore-lint` is off? I
 conjecture that they're entirely pointless without `-dcore-lint`.
 Sometimes we'll need to ask for the type of `(expr |> co)`, and so we'll
 have to store the type of the result of a cast (since we're omitting the
 coercion). Implementing this idea may be a challenge given our current
 code infrastructure, but I do think it would work. And then, poof, this
 problem goes away, and compilation probably gets a lot faster in a lot of
 cases. We absolutely want to keep coercions around for `-dcore-lint`, as
 that feature has saved us from unknown quantities of pain and
 embarrassment. But there's no good reason ordinary, trusting users need to
 pay the price (in compilation times/memory) for this feature.

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