Opened 6 years ago

Last modified 2 years ago

#8147 new bug

Exponential behavior in instance resolution on fixpoint-of-sum

Reported by: jkoppel Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: performance, Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Doing instance resolution on a fixpoint-of-sum type takes a very long time. This is possibly the same issue as issue #5642.

These are the numbers I see for various n:

10 : 0.329s
20 : 0.479s
40 : 0.935s
80 : 2.821s
160 : 11.694s
320 : 1m30.39s
640:  Ran for over 1 hour without terminating

This uses a couple of attached support files. Apologies for not being able to reduce further.

-- Test.hs
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, OverlappingInstances, TypeOperators, DeriveFunctor, TemplateHaskell #-}

module Test where

import Control.Monad

import Lib
import TH

{-
With n=3, produces

data X1 e = X1 e deriving (Functor)
data X2 e = X2 e deriving (Functor)
data X3 e = X3 e deriving (Functor)

type X = X1 :+: X2 :+: X3
-}
$(let n = 320 in
  liftM concat $ sequence [liftM concat $ mapM mkDec $ map (('X':).show) [1..n]
                          , makeSumType "X" (map (('X':).show) [1..n])])


data Y0 e = Y0 e deriving ( Functor )

type X' = Y0 :+: X

class Lift f g where
  lift' :: f (Fix g) -> Fix g

instance (Lift f g, Lift f' g) => Lift (f :+: f') g where
  lift' x = case x of 
              L e -> lift' e
              R e -> lift' e

instance (Functor f, f :<: g) => Lift f g where
  lift' = In . inj

cata :: (Functor f) => (f a -> a) -> Fix f -> a
cata f = f . fmap (cata f) . out

lift :: Fix X -> Fix X'
lift = cata lift' 

Virtually all the time is spent in compiling lift. For example, with n=640, commenting out lift makes it compile in around 2 seconds.

Interestingly, when I add the following code, compilation times only increase by 10-20%. In the original code where I encountered this issue, doing so doubles compilation time.

instance Lift Y0 X where
  lift' = undefined

lower :: Fix X' -> Fix X
lower = cata lift'

Attachments (5)

TH.hs (716 bytes) - added by jkoppel 6 years ago.
Template Haskell used by example code
Lib.hs (449 bytes) - added by jkoppel 6 years ago.
Sum and subtyping-class used by example code
TH.2.hs (800 bytes) - added by dfeuer 2 years ago.
Updated TH
Lib.2.hs (466 bytes) - added by dfeuer 2 years ago.
Updated Lib
Test.hs (1013 bytes) - added by dfeuer 2 years ago.
Updated Test

Download all attachments as: .zip

Change History (7)

Changed 6 years ago by jkoppel

Attachment: TH.hs added

Template Haskell used by example code

Changed 6 years ago by jkoppel

Attachment: Lib.hs added

Sum and subtyping-class used by example code

Changed 2 years ago by dfeuer

Attachment: TH.2.hs added

Updated TH

Changed 2 years ago by dfeuer

Attachment: Lib.2.hs added

Updated Lib

comment:1 Changed 2 years ago by dfeuer

The original files no longer work with GHC 8.2.1 as a result of TH changes. I've uploaded new ones that do. Unfortunately, the bug is still with us.

Changed 2 years ago by dfeuer

Attachment: Test.hs added

Updated Test

comment:2 Changed 2 years ago by dfeuer

Although there's still a bug, it has changed somewhat. We now get a context reduction stack overflow:

Test.hs:43:8: error:
    • Reduction stack overflow; size = 201
      When simplifying the following type:
        Functor
          (X201
           :+: (X202
                :+: (X203
                     :+: (X204
                          :+: (X205

...

      Use -freduction-depth=0 to disable this check
      (any upper bound you could choose might fail unpredictably with
       minor updates to GHC, so disabling the check is recommended if
       you're sure that type checking should terminate)
    • In the expression: cata lift'
      In an equation for ‘lift’: lift = cata lift'
   |
43 | lift = cata lift' 
   |        ^^^^^^^^^^

Removing the reduction depth limit brings my machine to its knees. I can compile the program with n=120 and a reduction depth limit of 300.

One other thing of note: removing the redundant Functor constraint on the Lift f g instance (which for some reason is not detected as redundant in 8.2.1, though it was in 8.0.2) improves matters considerably, but they're still pretty bad even in that case.

Note: See TracTickets for help on using tickets.