Tesla Zhang‮

Yes, that sounds like some important decisions, but probably would be done after we make structures available

I'm thinking 'bout this now. We should implement this to make Aya more 'practical'.

Please update to Kotlin 1.2.31.

I'm having the same issue.

Temporary workaround: adding type annotation to `x`

```arend \instance inst : C | f (x : B) => \new B { | v => suc (x.v) } ```

I hope we can use intellij's code instrumentation to get better error messages....

Is it this code that does such restriction? https://github.com/JetBrains/Arend/blob/3e8cfd5bd27421a8f78f5e7af326e21f55f3fab6/base/src/main/java/org/arend/typechecking/instance/pool/GlobalInstancePool.java#L122-L130

Some are impossible to address in my opinion

Is this fixed? I recall @valis has implemented tail-call optimization. Can we have some benchmark tests?