Current Teika typing is broken due to the lack of opening and closing which is required for a working locally nameless implementation. This is a bit tricky as we also have inference, so the approach decided here is to use "explicit substitutions" for opening and closing.
Goals
A working type checker with inference.
Context
Current Teika typing is broken due to the lack of opening and closing which is required for a working locally nameless implementation. This is a bit tricky as we also have inference, so the approach decided here is to use "explicit substitutions" for opening and closing.