sealed class TyEq<A, B>() {
    abstract fun cast(a: A): B
    abstract fun rot(): TyEq<B, A>

    class Refl<A>() : TyEq<A, A>() {
        override fun cast(a: A): A = a
        override fun rot(): TyEq<A, A> = this
    }
}

sealed interface Expr<T> {

    companion object {
        fun concat(x: Expr<String>, y: Expr<String>): Expr<String>
            = Concat(TyEq.Refl(), x, y)

        fun string(s: String): Expr<String>
            = Str(TyEq.Refl(), s)
    }

    data class Str<T>(
        val ty: TyEq<T, String>,
        val value: String,
    ) : Expr<T>

    data class Concat<T>(
        val ty: TyEq<T, String>,
        val lhs: Expr<String>,
        val rhs: Expr<String>,
    ) : Expr<T>
}

fun <T> eval(e: Expr<T>): T =
    when (e) {
        is Expr.Str -> e.ty.rot().cast(e.value)
        is Expr.Concat -> e.ty.rot().cast(eval(e.lhs) + eval(e.rhs))
    }

sealed class Nat<N : Nat<N>> {

    fun succ(): S<N> = S(this)

    abstract fun <M : Nat<M>> finOf(ix: Nat<M>): Fin<N>?

    object Z : Nat<Z>() {
        override fun <M : Nat<M>> finOf(ix: Nat<M>): Fin<Z>? = null

        override fun toString(): String = "Z"
    }

    data class S<N : Nat<N>>(val prev: Nat<N>) : Nat<S<N>>() {
        override fun <M : Nat<M>> finOf(ix: Nat<M>): Fin<S<N>>? =
            when (ix) {
                Z -> Fin.Z()
                is S<*> ->
                    when (val f = prev.finOf(ix.prev)) {
                        null -> null
                        else -> Fin.S(f)
                    }
            }
    }
}

sealed class SomeNat {

    fun succ(): SomeNat =
        accept(object : Visitor<SomeNat> {
            override fun <N : Nat<N>> visit(nat: Nat<N>): SomeNat = nat.succ().erase()
        })

    abstract fun <R> accept(visitor: Visitor<R>): R

    companion object {
        val Z = Nat.Z.erase()
        fun <N : Nat<N>> Nat<N>.erase(): SomeNat = Wrap(this)
    }

    interface Visitor<R> {
        fun <N : Nat<N>> visit(nat: Nat<N>): R
    }

    private data class Wrap<N : Nat<N>>(val nat: Nat<N>) : SomeNat() {
        override fun <R> accept(visitor: Visitor<R>): R = visitor.visit(nat)

        override fun toString(): String = "SomeNat(${nat})"
    }
}

sealed class Fin<N : Nat<N>> {

    fun succ(): S<N> = S(this)

    data class Z<N : Nat<N>>(val unit: Unit = Unit) : Fin<Nat.S<N>>()
    data class S<N : Nat<N>>(val prev: Fin<N>) : Fin<Nat.S<N>>()
}

abstract class Vect<A, N : Nat<N>> {

    abstract fun get(ix: Fin<N>): A

    abstract val length: N

    data class Nil<A>(val unit: Unit = Unit) : Vect<A, Nat.Z>() {
        override fun get(ix: Fin<Nat.Z>): A =
            when (ix) {
                else -> error("impossible")
            }

        override val length: Nat.Z = Nat.Z
    }

    data class Cons<A, N : Nat<N>>(val head: A, val tail: Vect<A, N>) : Vect<A, Nat.S<N>>() {
        override fun get(ix: Fin<Nat.S<N>>): A =
            when (ix) {
                is Fin.Z -> head
                is Fin.S -> tail.get(ix.prev)
            }

        override val length: Nat.S<N> = tail.length.succ()
    }
}

fun main(args: Array<String>) {
    println(eval(Expr.concat(Expr.string("hi"), Expr.string("world"))))

    println(Nat.Z.succ().succ().succ())
    println(SomeNat.Z.succ().succ())

    val xs = Vect.Cons(1, Vect.Cons(2, Vect.Nil()))
    println("xs=${xs}")
    println("length=${xs.length}")
    println(xs.get(Fin.Z()))
    println(xs.get(Fin.S(Fin.Z())))

    println(Nat.Z.succ().succ().succ().finOf(Nat.Z))
    println(Nat.Z.succ().succ().succ().finOf(Nat.Z.succ()))
    println(Nat.Z.succ().succ().succ().finOf(Nat.Z.succ().succ()))
    println(Nat.Z.succ().succ().succ().finOf(Nat.Z.succ().succ().succ()))
    println(Nat.Z.succ().succ().succ().finOf(Nat.Z.succ().succ().succ().succ()))
}