That code simulates a bounded cellular automaton, which effectively reduces to a regular language, but that's about as far as I've been able to get. If it's possible to implement general recursion, I'm not quite sure how - yet.
> Kotlin has nominal subtyping, contravariance, and generics, therefore its type system is undecidable.
They're not using Kennedy and Pierce's system, but it's closely related. See Tate (2013) [1], in particular, "In general, since declaration-site variance can easily be encoded into use-site variance..."
> I ported that code directly to Kotlin
Can you share your translation of Eric's code? Maybe we can get it to work.
> They're not using Kennedy and Pierce's system, but it's closely related. See Tate (2013) [1], in particular, "In general, since declaration-site variance can easily be encoded into use-site variance..."
Well, Kotlin has both declaration-site and use-site variance. So surely that result applies.
> Can you share your translation of Eric's code? Maybe we can get it to work.
[1]: https://fool2013.cs.brown.edu/tate.pdf