Terrible performance with singletonized maps

[treeowl]

Just for fun, I decided to try porting Data.Map to singletons. I know, that's crazy. Here's the code. It takes a while to compile that, but that doesn't bother me. What does bother me is that generating even a relatively small map takes an incredibly long time.

{-# language ScopedTypeVariables, TypeInType #-}
module TestSingMap where

import Data.Singletons
import qualified Data.Singletons.Prelude as P
import Data.Singletons.Prelude.Foldable
import SingMap

type Foo = FromList (P.Zip ((P.EnumFromTo 1 50)) (P.Replicate 50 "a"))
foo :: Sing Foo
foo = sing

type Bar = Smallest Foo

bar :: Sing Bar
bar = sing

I don't really know where things go sideways, but -ddump-tc-trace seems to show some truly enormous coercion signatures even when the list is cut from 50 elements down to 5.

[treeowl]

It's not actually necessary to build any singletons to get sluggish performance either.

goo :: Bar :~: 'Just ('(1, "a"))
goo = Refl

will take a while too.

[RyanGlScott]

I'm not sure what you mean by "sluggish performance" here. Are you talking about the runtime performance? If so, then I'm not able to reproduce the issue, since the following:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
module Main where

import qualified Data.Singletons.Prelude as P
import Data.Singletons.Prelude.Foldable
import Data.Type.Equality
import SingMap

type Foo = FromList (P.Zip ((P.EnumFromTo 1 50)) (P.Replicate 50 "a"))
type Bar = Smallest Foo

goo :: Bar :~: 'Just ('(1, "a"))
goo = Refl
                                                                                                   
main :: IO ()                                                                                      
main = print goo

Runs quite quickly for me (after compiling):

$ time cabal new-run bug
Up to date
Refl

real    0m0.032s
user    0m0.030s
sys     0m0.000s

If you're talking about the compile times, then yes, that's likely to be quite slow. Unfortunately, I don't know of a way to mitigate this on singletons' end, as GHC's compilation of type families in general tends to be rather slow.

[treeowl]

Compilation (even with -O0) is unusably slow for maps with a few hundred elements. I don't know enough about the underlying compiler performance problems to know whether there's likely to be a way to work around them for code like this, or even for this specific code.

[goldfirere]

I agree with Ryan on this. I think it's GHC's problem. It's quite common for GHC to produce quadratically-sized code for type-family heavy shenanigans. And because the code produced is quadratic, that means that every core pass, etc., is quadratic, too. There is a fix: #8095. @bgamari was working on this and may have only a little bit further to go. Keeping open as I do think we should add this to our testsuite.