search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Typo in LambdaLift AST #325

Closed evertedsphere closed 4 years ago

evertedsphere commented 4 years ago

The var here should be vars, I believe:

https://github.com/edwinb/Idris2/blob/master/src/Compiler/LambdaLift.idr#L29

gallais commented 4 years ago

:scream:

I wonder whether we should add an optional warning about implicitly polymorphic functions where the polymorphism only shows up in one of the arguments. There are legitimate use cases (existential types) but this could help catch these kind of typos.

I'll try to implement that & see how many warnings it would trigger on the idris2 codebase.

edwinb commented 4 years ago

Hm, that's an interesting idea. If I got a warning like that I think I'd be happy to make the binding explicit anyway.

jfdm commented 4 years ago

@gallais Slight typo's like this has caught me out a few times. Having something to try and catch these sorts of errors would be good, especially if it was optional as you suggested.