Very large case tree for a simple function

[spcfox]

Gist with code

Steps to Reproduce

This code typechecks on my machine in about 50 seconds and generates a huge .ttc.

data X : () -> Type where
  A : X i
  B : X i
  C : X i

data Y : ((i ** X i), (i ** X i)) -> Type where
  MkY : Y x

f : (a, b : ()) -> (x : X a) -> (y : X b) -> Y ((a ** x), (b ** y)) -> ()
f a  () A A MkY = ()
f () b  A B MkY = ()
f a  () B A MkY = ()
f a  b  B B MkY = ()
f a  () C A MkY = ()
f a  b  C B MkY = ()
f a  b  _ _ _   = ()

I have prepared various modifications to find the influencing factors. Compilation time correlates with the size of .ttc, so I will give the file sizes for comparison:

$ du -h --apparent-size *.ttc | sort -hr
46M     ExampleFull.ttc
44M     Example.ttc
17M     ExampleNoMatchLastY.ttc
8.2M    ExampleSwap.ttc
4.8M    ExampleNoPair.ttc
1.4M    ExampleSwapNoPair.ttc
56K     ExampleNoMatchY.ttc
13K     ExampleNoMatchAB.ttc
13K     ExampleErased.ttc
12K     ExampleMatchAll.ttc

The full code for all modifications is available in gist. Here I will give a brief description of them:

• Example — the code presented above
• ExampleFull — all implicit arguments are explicitly specified
• ExampleNoMatchLastY — removed last matching on MkY
• ExampleSwap — swap the first two cases
• ExampleNoPair — Y has two indices instead of one pair
• ExampleSwapNoPair — combination of ExampleSwap and ExampleNoPair
• ExampleNoMatchY — no matching on MkY
• ExampleNoMatchAB — no matching on a and b.
• ExampleErased — a and b have quantity 0
• ExampleMatchAll — matching on a and b everywhere

From my observations, every matching on the MkYslows down the typecheck a lot.

---

I also tested this example on Yaffle, the result is similar:

$ du -h --apparent-size *.ttc | sort -hr
73M     Example.ttc
57M     ExampleFull.ttc
15M     ExampleNoMatchLastY.ttc
13M     ExampleSwap.ttc
5.7M    ExampleNoPair.ttc
1.6M    ExampleSwapNoPair.ttc
34K     ExampleNoMatchY.ttc
11K     ExampleNoMatchAB.ttc
11K     ExampleErased.ttc
7.8K    ExampleMatchAll.ttc

Expected Behavior

Fast typechecking

Observed Behavior

$ idris2 --check Example.idr --timing 5
1/1: Building Example (Example.idr)
TIMING ++ Parsing Example.idr: 0.006s
TIMING ++ Reading imports: 0.074s
TIMING +++ Check RHS Example:12:1--12:21: 0.000s
TIMING +++ Check RHS Example:13:1--13:21: 0.000s
TIMING +++ Check RHS Example:14:1--14:21: 0.000s
TIMING +++ Check RHS Example:15:1--15:21: 0.000s
TIMING +++ Check RHS Example:16:1--16:21: 0.000s
TIMING +++ Check RHS Example:17:1--17:21: 0.000s
TIMING +++ Check RHS Example:18:1--18:21: 0.000s
TIMING +++ Building compile time case tree for Example.f: 17.781s
TIMING +++ Building size change graphs Example.f: 0.352s
TIMING +++ Checking Coverage Example.f: 14.853s
TIMING +++ Totality check overall: 0.000s
TIMING ++ Processing decls: 33.041s
TIMING ++ Compile defs: 3.841s
TIMING + Elaborating Example.idr: 36.965s
TIMING + Build deps: 50.003s
TIMING + Loading main file: 50.006s