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

Type inference crashes in lets for numeric types #2373

Closed
lukaszcz opened this issue Sep 18, 2023 · 0 comments · Fixed by #2390
Closed

Type inference crashes in lets for numeric types #2373

lukaszcz opened this issue Sep 18, 2023 · 0 comments · Fixed by #2390
Assignees
Milestone

Comments

@lukaszcz
Copy link
Collaborator

The following

import Stdlib.Prelude open;

main : Nat :=
  let
     x : _ := 0;
     y : Nat := 1;
  in
  x + y;

crashes with

juvix: impossible: x@650 is not in the InfoTable

The following also crashes:

import Stdlib.Prelude open;

main : Int :=
  let
     x : _ := 0;
     y : Int := 1;
  in
  x - y;

The following works:

import Stdlib.Prelude open;

main : Bool :=
  let
     x : _ := true;
     y : Bool := false;
  in
  x || y;
@lukaszcz lukaszcz added this to the 0.5.2 milestone Sep 18, 2023
@janmasrovira janmasrovira self-assigned this Sep 25, 2023
@janmasrovira janmasrovira linked a pull request Sep 25, 2023 that will close this issue
lukaszcz pushed a commit that referenced this issue Sep 26, 2023
- Closes #2373 

Consider this:
```
let 
 x : _ := 0
in ...
```
When translating the let to internal, we build the dependency graph and
then use that to group definitions in mutually recursive blocks. Since
`x` has no edge, it was not being added to the dependency graph, so it
was not being translated to Internal, thus crashing later during
inference.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants