[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 bgamari):

 Finally have a chance to look at this. In particular I'll be looking at
 the `b a` case identified in comment:6 as still being slow. For the record
 `runghc Types.hs 5 b a` produces output of the form,
 {{{#!hs
 {-# LANGUAGE
 TypeOperators,DataKinds,KindSignatures,TypeFamilies,PolyKinds,UndecidableInstances
 #-}
 import GHC.TypeLits

 data Nat1 = Zero | Succ Nat1

 type family Replicate1 (n :: Nat1) (x::a) :: [a]
 type instance Replicate1 n x = Replicate1' '[] n x

 type family Replicate1' (acc::[a]) (n :: Nat1) (x::a)  :: [a]
 type instance Replicate1' acc Zero x = acc
 type instance Replicate1' acc (Succ n) x = Replicate1' (x ': acc) n x

 class Class a where
     f :: a -> a

 data Data (xs::a) = X | Y
     deriving (Read,Show)

 main = print test1

 -- The numeric parameter adjusts this
 -- This definition is inlined in the actual output
 type N = Succ (Succ (Succ (Succ (Succ Zero)))

 instance (xs ~ Replicate1 N ()) => Class (Data xs) where
     f X = Y
     f Y = X

 test1 = f (X :: Data (Replicate1 N () ))
 }}}

 In particular the numeric parameter to `Test` is adjusting `N`.

 In the case of `N=500` compile-time is quite bad indeed,
 {{{
 $ ./Types 500 b a >| test.hs && time ghc test.hs  -freduction-depth=0
 -dshow-passes
 Glasgow Haskell Compiler, Version 7.11.20151006, stage 2 booted by GHC
 version 7.10.2
 ...
 *** Chasing dependencies:
 Chasing modules from: *test.hs
 Stable obj: []
 Stable BCO: []
 Ready for upsweep
   [NONREC
       ModSummary {
          ms_hs_date = 2015-10-06 11:44:53.905638216 UTC
          ms_mod = Main,
          ms_textual_imps = [import (implicit) Prelude, import
 GHC.TypeLits]
          ms_srcimps = []
       }]
 *** Deleting temp files:
 compile: input file test.hs
 Created temporary directory: /tmp/ghc27682_0
 *** Checking old interface for Main:
 [1 of 1] Compiling Main             ( test.hs, test.o )
 *** Parser:
 *** Renamer/typechecker:
 *** Desugar:
 Result size of Desugar (after optimization)
   = {terms: 103, types: 11,779, coercions: 509,036}
 *** Simplifier:
 Result size of Simplifier iteration=1
   = {terms: 107, types: 7,294, coercions: 516}
 Result size of Simplifier
   = {terms: 107, types: 7,294, coercions: 516}
 *** Tidy Core:
 Result size of Tidy Core
   = {terms: 111, types: 7,302, coercions: 518}
 *** CorePrep:
 Result size of CorePrep
   = {terms: 152, types: 7,880, coercions: 518}
 *** Stg2Stg:
 *** CodeGen:
 *** Assembler:
 Upsweep completely successful.
 *** Deleting temp files:
 Warning: deleting non-existent /tmp/ghc27682_0/ghc_3.c
 Warning: deleting non-existent /tmp/ghc27682_0/ghc_1.s
 Linking test ...
 *** C Compiler:
 *** C Compiler:
 *** Linker:
 *** Deleting temp files:
 *** Deleting temp dirs:

 real    0m22.835s
 user    0m22.514s
 sys     0m0.315s
 }}}

 It appears that the desugaring pass ends up producing a number of
 coercions quadratic in the number of depth of the equality in the context
 result (with almost all being eliminated during simplification),

   ||= input    =||= terms =||= types =||= coercions =||
   || 400 b a    || 103     || 9479    || 327236      ||
   || 200 b a    || 103     || 4879    || 83636       ||
   || 100 b a    || 103     || 2579    || 21836       ||
   || 50 b a     || 103     || 1429    || 5936        ||
   || 2 b a      || 103     || 325     || 80          ||

 Looking at the output from desugaring, it seems that the only definition
 which is growing non-linearly is `main` itself, where indeed we find a
 chain of quadratically growing coercions. For instance, in the case of
 `N=3` we have,

 {{{#!hs
 -- RHS size: {terms: 6, types: 85, coercions: 102}
 main :: IO ()
 [LclIdX, Str=DmdType]
 main =
   print
     @ (Data '[(), (), ()])
     (Main.$fShowData @ [*] @ '[(), (), ()])
     (f @ (Data '[(), (), ()])
        (Main.$fClassData
           @ '[(), (), ()]
           (Eq#
              @ [*]
              @ '[(), (), ()]
              @ (Replicate1 ('Succ ('Succ ('Succ 'Zero))) ())
              @~ (Sym
                    (Main.TFCo:R:Replicate1'kaccZerox[0]
                       <*>_N <'[(), (), ()]>_N <()>_N)
                  ; Sym
                      (Main.TFCo:R:Replicate1'kaccSuccx[0]
                         <*>_N <'[(), ()]>_N <'Zero>_N <()>_N)
                  ; Sym
                      (Main.TFCo:R:Replicate1'kaccSuccx[0]
                         <*>_N <'[()]>_N <'Succ 'Zero>_N <()>_N)
                  ; Sym
                      (Main.TFCo:R:Replicate1'kaccSuccx[0]
                         <*>_N <'[]>_N <'Succ ('Succ 'Zero)>_N <()>_N)
                  ; Sym
                      (Main.TFCo:R:Replicate1knx[0]
                         <*>_N <'Succ ('Succ ('Succ 'Zero))>_N <()>_N)
                  :: '[(), (), ()] ~# Replicate1 ('Succ ('Succ ('Succ
 'Zero))) ())))
        (((Main.X @ [*] @ '[(), (), ()])
          `cast` ((Data
                     (UnivCo opt_phantom phantom
                        '[(), (), ()] (Replicate1 ('Succ ('Succ ('Succ
 'Zero))) ())))_R
                  :: Data '[(), (), ()]
                     ~R# Data (Replicate1 ('Succ ('Succ ('Succ 'Zero)))
 ())))
         `cast` ((Data
                    (UnivCo opt_phantom phantom
                       (Replicate1 ('Succ ('Succ ('Succ 'Zero))) ()) '[(),
 (), ()]))_R
                 :: Data (Replicate1 ('Succ ('Succ ('Succ 'Zero))) ())
                    ~R# Data '[(), (), ()])))

 }}}

 More analysis to follow.

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