Type-level deletion quite slow

[danidiaz]

The following core uses type-level deletion and winnow:

{-# LANGUAGE DataKinds, TypeApplications, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Main where

import Data.RBR 

import GHC.TypeLits
import Data.Kind

type Phase01 = FromList '[ 
                           '("ctor1",Int), 
                           '("ctor2",Bool), 
                           '("ctor4",Char),
                           '("ctor3",Char),
                           '("ctor6",Char),
                           '("ctor5",Char),
                           '("ctor10",Char),
                           '("ctor11",Char),
                           '("ctor13",Char),
                           '("ctor14",Char),
                           '("ctor39",Char),
                           '("ctor46",Char),
                           '("ctor47",Char),
                           '("ctor44",Char),
                           '("ctor43",Char),
                           '("ctor7",Char),
                           '("ctor9",Char),
                           '("ctor20",Char),
                           '("ctor45",Char),
                           '("ctor21",Char),
                           '("ctor48",Char),
                           '("ctor49",Char),
                           '("ctor50",Char),
                           '("ctor41",Char),
                           '("ctor33",Char),
                           '("ctor32",Char),
                           '("ctor42",Char),
                           '("ctor22",Char),
                           '("ctor23",Char),
                           '("ctor8",Char),
                           '("ctor40",Char),
                           '("ctor29",Char),
                           '("ctor24",Char),
                           '("ctor38",Char),
                           '("ctor25",Char),
                           '("ctor26",Char),
                           '("ctor27",Char),
                           '("ctor28",Char),
                           '("ctor36",Char),
                           '("ctor52",Char),
                           '("ctor51",Char),
                           '("ctor53",Char),
                           '("ctor12",Char),
                           '("ctor54",Char),
                           '("ctor15",Char),
                           '("ctor31",Char),
                           '("ctor30",Char),
                           '("ctor34",Char),
                           '("ctor35",Char),
                           '("ctor17",Char),
                           '("ctor16",Char),
                           '("ctor18",Char),
                           '("ctor19",Char),
                           '("ctor37",Char)
                           ]

type Phase02 = Insert "xtor4" Int Phase01

type Phase03 = Delete "ctor1" Int Phase02

fromPhase1ToPhase2 :: Variant I Phase01 -> Variant I Phase02
fromPhase1ToPhase2 = widen @"xtor4"

fromPhase2ToPhase3 :: Variant I Phase02 -> Variant I Phase03
fromPhase2ToPhase3 v = case winnowI @"ctor1" @Int v of 
    Right z -> injectI @"ctor2" False
    Left l -> l

main :: IO ()
-- main = print (match @"ctor17" (fromPhase1ToPhase2 (injectI @"ctor1" 2)))
main = print (match @"ctor17" (fromPhase2ToPhase3 (fromPhase1ToPhase2 (injectI @"ctor1" 2))))

It compiles in about 2 minutes, often more. But removing the fromPhase2ToPhase3 function makes it compile in about 22 seconds!

This seems to indicate that type-level deletion is way slower than insertion.

[danidiaz]

Commit 9c63c7d improves times somewhat (it takes ~ 1 minute to compile now) but I have no idea why.

What I did was to pull out a type family invocation that was sitting in a typeclass argument. Instead of that, I evaluate the type family to a result designated with an equality constraint ~ and then use that result as the typeclass argument.

Why should that be faster? I have no idea and I would like to know.

[danidiaz]

Commit c896bd2 adds a number of similar changes. The impact in compilation times is minor, but let's include them for consistency anyway.

[danidiaz]

Here's the code sample without the insert, with a simple deletion:

{-# LANGUAGE DataKinds, TypeApplications, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Main where

import Data.RBR 

import GHC.TypeLits
import Data.Kind

type Phase01 = FromList '[ 
                           '("ctor1",Int), 
                           '("ctor2",Bool), 
                           '("ctor4",Char),
                           '("ctor3",Char),
                           '("ctor6",Char),
                           '("ctor5",Char),
                           '("ctor10",Char),
                           '("ctor11",Char),
                           '("ctor13",Char),
                           '("ctor14",Char),
                           '("ctor39",Char),
                           '("ctor46",Char),
                           '("ctor47",Char),
                           '("ctor44",Char),
                           '("ctor43",Char),
                           '("ctor7",Char),
                           '("ctor9",Char),
                           '("ctor20",Char),
                           '("ctor45",Char),
                           '("ctor21",Char),
                           '("ctor48",Char),
                           '("ctor49",Char),
                           '("ctor50",Char),
                           '("ctor41",Char),
                           '("ctor33",Char),
                           '("ctor32",Char),
                           '("ctor42",Char),
                           '("ctor22",Char),
                           '("ctor23",Char),
                           '("ctor8",Char),
                           '("ctor40",Char),
                           '("ctor29",Char),
                           '("ctor24",Char),
                           '("ctor38",Char),
                           '("ctor25",Char),
                           '("ctor26",Char),
                           '("ctor27",Char),
                           '("ctor28",Char),
                           '("ctor36",Char),
                           '("ctor52",Char),
                           '("ctor51",Char),
                           '("ctor53",Char),
                           '("ctor12",Char),
                           '("ctor54",Char),
                           '("ctor15",Char),
                           '("ctor31",Char),
                           '("ctor30",Char),
                           '("ctor34",Char),
                           '("ctor35",Char),
                           '("ctor17",Char),
                           '("ctor16",Char),
                           '("ctor18",Char),
                           '("ctor19",Char),
                           '("ctor37",Char)
                           ]

type Phase02 = Delete "ctor1" Int Phase01

fromPhase1ToPhase2 :: Variant I Phase01 -> Variant I Phase02
fromPhase1ToPhase2 v = case winnowI @"ctor1" @Int v of 
    Right z -> injectI @"ctor2" False
    Left l -> l

main :: IO ()
main = print (match @"ctor17" (fromPhase1ToPhase2 ((injectI @"ctor1" 2))))

It's taking ~ 29 seconds to compile. Removing the deletion (Phase02, fromPhase1ToPhase2, leaving only the construction of the type-level map) makes it take ~ 8 seconds.

20 seconds of compilation time is a steep price to pay for removing a single branch.

[danidiaz]

Yet another mystery. If I inline the fromPhase1ToPhase2 definition like this:

{-# LANGUAGE DataKinds, TypeApplications, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Main where

import Data.RBR 

import GHC.TypeLits
import Data.Kind

type Phase01 = FromList '[ 
                           '("ctor1",Int), 
                           '("ctor2",Bool), 
                           '("ctor4",Char),
                           '("ctor3",Char),
                           '("ctor6",Char),
                           '("ctor5",Char),
                           '("ctor10",Char),
                           '("ctor11",Char),
                           '("ctor13",Char),
                           '("ctor14",Char),
                           '("ctor39",Char),
                           '("ctor46",Char),
                           '("ctor47",Char),
                           '("ctor44",Char),
                           '("ctor43",Char),
                           '("ctor7",Char),
                           '("ctor9",Char),
                           '("ctor20",Char),
                           '("ctor45",Char),
                           '("ctor21",Char),
                           '("ctor48",Char),
                           '("ctor49",Char),
                           '("ctor50",Char),
                           '("ctor41",Char),
                           '("ctor33",Char),
                           '("ctor32",Char),
                           '("ctor42",Char),
                           '("ctor22",Char),
                           '("ctor23",Char),
                           '("ctor8",Char),
                           '("ctor40",Char),
                           '("ctor29",Char),
                           '("ctor24",Char),
                           '("ctor38",Char),
                           '("ctor25",Char),
                           '("ctor26",Char),
                           '("ctor27",Char),
                           '("ctor28",Char),
                           '("ctor36",Char),
                           '("ctor52",Char),
                           '("ctor51",Char),
                           '("ctor53",Char),
                           '("ctor12",Char),
                           '("ctor54",Char),
                           '("ctor15",Char),
                           '("ctor31",Char),
                           '("ctor30",Char),
                           '("ctor34",Char),
                           '("ctor35",Char),
                           '("ctor17",Char),
                           '("ctor16",Char),
                           '("ctor18",Char),
                           '("ctor19",Char),
                           '("ctor37",Char)
                           ]

main :: IO ()
main = print $ match @"ctor17" $
    (\v -> case winnowI @"ctor1" @Int v of 
        Right z -> injectI @"ctor2" False
        Left l -> l)
    ((injectI @"ctor1" 2) :: Variant I Phase01)

Then compilation time drops down to about ~ 8 seconds! For some reason having fromPhase1ToPhase2 as a separate function makes compilation take much longer. So it wasn't the deletion what was causing the problem...

[danidiaz]

Even more mysterious. When I put fromPhase1ToPhase2 inside a where clause, like this

{-# LANGUAGE DataKinds, TypeApplications, UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Main where

import Data.RBR 

import GHC.TypeLits
import Data.Kind

type Phase01 = FromList '[ 
                           '("ctor1",Int), 
                           '("ctor2",Bool), 
                           '("ctor4",Char),
                           '("ctor3",Char),
                           '("ctor6",Char),
                           '("ctor5",Char),
                           '("ctor10",Char),
                           '("ctor11",Char),
                           '("ctor13",Char),
                           '("ctor14",Char),
                           '("ctor39",Char),
                           '("ctor46",Char),
                           '("ctor47",Char),
                           '("ctor44",Char),
                           '("ctor43",Char),
                           '("ctor7",Char),
                           '("ctor9",Char),
                           '("ctor20",Char),
                           '("ctor45",Char),
                           '("ctor21",Char),
                           '("ctor48",Char),
                           '("ctor49",Char),
                           '("ctor50",Char),
                           '("ctor41",Char),
                           '("ctor33",Char),
                           '("ctor32",Char),
                           '("ctor42",Char),
                           '("ctor22",Char),
                           '("ctor23",Char),
                           '("ctor8",Char),
                           '("ctor40",Char),
                           '("ctor29",Char),
                           '("ctor24",Char),
                           '("ctor38",Char),
                           '("ctor25",Char),
                           '("ctor26",Char),
                           '("ctor27",Char),
                           '("ctor28",Char),
                           '("ctor36",Char),
                           '("ctor52",Char),
                           '("ctor51",Char),
                           '("ctor53",Char),
                           '("ctor12",Char),
                           '("ctor54",Char),
                           '("ctor15",Char),
                           '("ctor31",Char),
                           '("ctor30",Char),
                           '("ctor34",Char),
                           '("ctor35",Char),
                           '("ctor17",Char),
                           '("ctor16",Char),
                           '("ctor18",Char),
                           '("ctor19",Char),
                           '("ctor37",Char)
                           ]

type Phase02 = Delete "ctor1" Int Phase01

main :: IO ()
main = print (match @"ctor17" (fromPhase1ToPhase2 (injectI @"ctor1" 2)))
    where
    fromPhase1ToPhase2 :: Variant I Phase01 -> Variant I Phase02
    fromPhase1ToPhase2 v = case winnowI @"ctor1" @Int v of 
        Right z -> injectI @"ctor2" False
        Left l -> l

Compilation time goes back to ~ 8 seconds.

It seems that having fromPhase1ToPhase2 at the top level is what causes problems.

[danidiaz]

SO question and GHC ticket.