idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.53k stars 378 forks source link

Slow typechecking interface with complex constraint #3419

Open spcfox opened 5 days ago

spcfox commented 5 days ago

Steps to Reproduce

Here's a minimal example I was able to write. Transform.idr typechecking 150s on my machine.

Some important points, to reproduce the problem:

Expected Behavior

Fast typechecking

Observed Behavior

$ idris2 --check Transform.idr --timing 10
3/3: Building Transform (Transform.idr)
TIMING ++ Parsing Transform.idr: 0.001s
TIMING ++ Reading imports: 0.049s
TIMING +++ Check RHS Transform:6:1--6:18: 0.000s
TIMING +++ Building compile time case tree for Transform.transform: 0.000s
TIMING +++ Building size change graphs Transform.transform: 0.000s
TIMING +++ Checking Coverage Transform.transform: 0.000s
TIMING +++ Check RHS Transform:8:1--9:12: 0.000s
TIMING +++ Building compile time case tree for Transform.Iface implementation at Transform:8:1--9:12: 0.000s
TIMING +++ Building size change graphs Transform.Iface implementation at Transform:8:1--9:12: 0.000s
TIMING +++ Checking Coverage Transform.Iface implementation at Transform:8:1--9:12: 0.000s
TIMING +++ Check RHS Transform:9:3--9:12: 0.000s
TIMING +++ Building compile time case tree for Transform.unit: 0.000s
TIMING +++ Building size change graphs Transform.unit: 0.000s
TIMING +++ Checking Coverage Transform.unit: 0.000s
TIMING +++ Totality check overall: 0.000s
TIMING ++ Processing decls: 148.699s
TIMING ++ Compile defs: 0.000s
TIMING + Elaborating Transform.idr: 148.752s
TIMING + Build deps: 148.912s
TIMING + Loading main file: 148.914s