Matúš Tejiščák
Matúš Tejiščák
I agree, this should definitely not happen. We did have some erasure bugs in the past but it's been a long time since I've seen one so reports are welcome....
Yep, reproduced, thanks. This looks strange, I'll dig deeper after work.
The build works fine on my machine but maybe https://github.com/edwinb/Idris2/pull/255 broke something on NixOS? That change made codegen (and the generated scripts) use absolute paths.
Assuming that `let (omega q : Bool) = foo True in q` should be equivalent to `(\omega q : Bool => q) (foo True)`, this should typecheck because the result...
Oh, I see, thanks!
If we do this, we should tell the elaborator not to generalise names after dots to avoid `foo.n -> T` being translated as `{0 n : _} -> n foo...
I expect that once pluggable backends are a thing, it should not be hard to port the existing ones. Non-pluggable backends have to be in-tree. I'm also working on a...
For the record, I've abandoned the JS project I talked about. It turns out that the JS `switch` statement does not jump in constant time, at least not in the...
This seems to happen in overapplied lambdas, which I did not address. The RHS in `Erasure.hs:617` should probably be `mkApp tm vs`.
`mkApp tm vs` typechecks but the de Bruijn indices in `vs` will probably be wrong because we're reapplying them under new let bindings. The existing code of `lamToLet` probably suffers...