Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Slow typechecking interface with complex constraint #3419

Open
spcfox opened this issue Nov 20, 2024 · 0 comments
Open

Slow typechecking interface with complex constraint #3419

spcfox opened this issue Nov 20, 2024 · 0 comments

Comments

@spcfox
Copy link
Contributor

spcfox commented Nov 20, 2024

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:

  • Transform.idr should not import SomeUnit
  • transform should not be reduced (e.g. you can leave it undefined)
  • The constraint should be auto

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant