Btw this is the same problem with any kind of proof system that depends on terms and has exceptions / divergence / null (i.e. anything that can generate a term

Btw this is the same problem with any kind of proof system that depends on terms and has exceptions / divergence / null (i.e. anything that can generate a term of any type). Same problem would appear in Haskell, where you can define a term of any type (using a divergent function); the actual value is never executed (because of laziness), so it would crash at runtime. In OCaml, the type system would accept this, but it wouldn't crash (because the "any type" term cannot actually be created, but would result in an exception and/or divergence). The correct solution is for the type system to track "computability" and require that all terms used in proofs are actually well-defined. Liquid Haskell in particular had this problem that they had to solve by enforcing strictness for such terms. (Also, technically generic functions in Java/Scala aren't "parametrically polymorphic" - which means that you cannot do any operation on a value of polymorphic type - not even `typeof`).