One thing that jumps out (besides the unusual code formatting) is that the resulting type system considers code like bad/1:
to be typed correctly, due to how it handles “downcasting” from any.
2 Likes
