Botched Argument, Botched Algorithm

 "Everybody can know but the point is to understand." That's supposedly a quote by Einstein.

I've been discussing the previous post somewhat and been pointed at regular trees and how OCaml does it.

My point is, and I don't know whether it's true either, when you think your type system gives an inductive proof but it is actually giving a botched bisimulation argument, then that leads to botched algorithms and then also to incomprehensible errors. Because you fundamentally misunderstood the solution to the problem, or you didn't even get the problem right.

Indicative of that could be stuff like this: https://github.com/ocaml/ocaml/issues/7726

Then there was a comment on that I didn't propose a solution out of the conundrum. I don't have one but my instinct is to make the bisimulation relation explicit in the typing rules; i.e., the typing rules should include a bisimulation relation Eq: T x T. Because imperative type checkers prove types equal with a proof of existence of a bisimulation relation; I also suspect you cannot do it any other way without getting close but fundamentally getting it wrong.

But I don't know but that's what I want to experiment with. Once I get the egel interpreter sources accepted and compiled again.