Implement a proper wellformedness check

effekt-lang / effekt

A language with lexical effect handlers and lightweight effect polymorphism

https://effekt-lang.org

MIT License

335 stars 24 forks source link

Implement a proper wellformedness check #552

Closed b-studios closed 3 months ago

b-studios commented 3 months ago

This is an attempt at fixing #548

Create a proper context tracking which bindings (types and captures) are in scope and then run the wellformedness check on inferred types.

TODO:

[x] make sure that we catch all binding occurrences
[x] make sure that we check all inferred types (type arguments, return types of functions and matches, ...)
[x] treat existentials properly

b-studios commented 3 months ago

Still todo:

[x] improve implementation and deduplicate
[x] improve error messages (previously they have been specialized to what kind of capture escaped "local variable ... escapes" instead of "captures {x} escapes ..."

Especially the worse error messages are frustrating. It would be great to look at the diff of this PR and see how we can get this kind of (or better) messages back.