Re: [GHC] #8095: TypeFamilies painfully slow

8 Oct 2015

      #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 simonpj):

 Good idea.  And here's an easier way to implement it: replace every (non-
 trivial) coercion in the program (specifically in cases) with `UnivCo`!

 That deals with the "sometimes we'll need to type of the result in the
 cast" question.

 But we need to take care.  If we start with
 {{{
 data T a where
   T1 :: Bool -> T Bool
   T2 :: T a

 f :: T a -> a -> Bool
 f = /\a (x:T a) (y:a).
     case x of
           T1 (c : a~Bool) (z : Bool) -> not (y |> c)
           T2 -> True
 }}}
 If we discard the cast, or turn it into UnivCo we might then wrongly float
 the not-expression, thus
 {{{
 f = /\a (x:T a) (y:a).
     let w :: Bool = not (y |> UnivCo a Bool)
     case x of
           T1 (c : a~Bool) (z : Bool) -> w
           T2 -> True
 }}}
 This woudl not have happened before, because the 'c' would prevent the
 not-expression being floated.  But if we dump the 'c' it could (utterly
 bogusly, and risking seg-faults) be floated.

 So if we are going to radically abbreviate to `UnivCo` or something like
 it, we should include the free variables of the coercion we have
 discarded, something like `UnivCo t1 tc [v1,...,vn]`.  So we'd get:
 {{{
 f :: T a -> a -> Bool
 f = /\a (x:T a) (y:a).
     case x of
           T1 (c : a~Bool) (z : Bool) -> not (y |> UnivCo a Bool [c])
           T2 -> True
 }}}
 But now what if `c` was itself bound to a big coercion?  Then the `UnivCo`
 would keep the big coercion alive.
 But it's ok: we should just substitute for `c` to get
 {{{
 UnivCo a Bool [big-coercion]
 }}}
 and now have a magic `UnivCo` optimisation to take the free vars of `big-
 coercion`:
 {{{
 UnivCo a Bool [v1,..,vn]
 }}}
 I think that would do it.

 We could do this in the desugarer; or even earlier in `setEvBind` in the
 type checker.  In the latter case we'd essentially kill off those big
 coercions at birth.

 Simon

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