The author's generalized subtype check is interesting: what the author defines as "inconclusive" is clearly a type error in more traditional statically typed la

The author's generalized subtype check is interesting: what the author defines as "inconclusive" is clearly a type error in more traditional statically typed languages. (Traditionally the type checker is supposed to guarantee progress and preservation, so leaving something inconclusive to the runtime isn't acceptable.) And I guess the kind of differentiation the author makes between "inconclusive" and "static error" is so unusual that the normal classification of covariance and contravariance break. This reminds me of Haskell, where type variables may have user-provided annotation of whether they are representational, nominal, or phantom. Such classification affects the ability for values to be treated at runtime as a different type (using Data.Coerce). Maybe the author can come up with a similar system for classifying type variables for things like List. However for a configuration language that is type checked and immediately run, there's not much difference between runtime type checks and pre-run static type checks. Given this escape hatch, I think the author is right to simply defer everything that cannot be checked statically into runtime checks.