Re: [GHC] #8095: TypeFamilies painfully slow

18 Jul 2017

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

Comment (by mbieleck):

 Replying to [comment:41 simonpj]:
...
But do read comment:15 above carefully.   It's ''crucial'' to keep track
 of the free coercion variables of a coercion, otherwise GHC may (after
 discarding coercions) "optimise" a correct program into one that seg-
 faults.  We don't want that.
My hypothesis was is that the coercion returned specifically by
 `flatten_fam_app` should not have more free variables than the original
 type (`F arg1 arg2`). I failed to see how example from comment:15 would
 interact with type families. But I was wrong - `flatten_fam_app` could not
 only use axioms, but also coercion variables that happen to be in scope.

 Here's an example that demonstrates bad behavior of `-fomit-type-family-
 coercions`:

 {{{#!hs
 {-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances #-}
 module Bad where
 type family Id a
 data T a where
   T1 :: Id a ~ Bool => T a
 f :: T a -> Id a -> Bool
 f x y =
     case x of
       T1 -> not y
 }}}

 Core (simplified) without `-fomit-type-family-coercions`:

 {{{
 f = \ (@ a) (x :: T a) (y :: Id a) ->
       case x of
         T1 (co :: Id a ~ Bool) ->
           not (y |> co)
 }}}

 Core (simplified) with `-fomit-type-family-coercions`:

 {{{
 f = \ (@ a) (x :: T a) (y :: Id a) ->
       case x of
         T1 (co :: Id a ~ Bool) ->
           not (y |> UnivCo (Id a) Bool)
 }}}

 `not (y |> UnivCo (Id a) Bool)` can be floated out, which should not
 happen.

 The next obvious thing is to generate the coercion, traverse it to find
 free variables and discard it, putting free variables in `UnivCo`. I've
 measured how much just traversing the coercion would impact the
 performance (using `seqCo`). This results in about 50% slowdown compared
 to just discarding the coercion (for `timings.sh`).

 An alternative is to track used coercion variables in `FlattenEnv`, but I
 don't know how reliable would that be. The in-scope coercion gets pulled
 in in `lookupFlatCache`, is that right? Are there other places in the
 flattener which can use coercion variables?

 I apologise for posting so much comments and code, I want to confirm
 whether my reasoning is correct.

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