Why don't they just add the dynamic typing when that happens. There could then be a class of Haskell programs that are statically ill-formed, yet actually free of errors.

Maybe adding dynamic typing to a thoroughbred static language could turn out more fruitful than efforts to go the other way.

> Why don't they just add the dynamic typing when that happens.

Haskell (at least, GHC Haskell) has support for dynamic typing, in three(ish) parts.

"Dynamic typing" in the sense of being able to ask the types at runtime is available in the Typeable typeclass. This is provided by the compiler automatically for known types; it must be visibly asked for for polymorphic types - partly for visibility and to preserve reasoning (https://www.reddit.com/r/haskell/comments/4mu30y/what_is_the...) and partly to clarify what dictionaries need to be passed where.

"Dynamic typing" in the sense of foregoing static checks in favor of runtime checks can, of course, usually be done in a constrained way simply by choosing looser types. That said, depending on language, that can often mean substantial boilerplate. GHC does provide Dynamic, which will wrap any value up with its type annotations and let you apply (possibly wrapped) functions to these wrapped values in a dynamically checked way.

Lastly, I'd kind of put "existential quantification" in play here. It's sometimes the case that you only need to show that some pieces of "the same type" are internally consistent, without knowing their precise shape.

As for why it's not added, I'm not 100% sure what you mean.

If you mean on every build, making that the only option, then I would say "because many of us who choose Haskell find static checks a huge help (particularly when refactoring) and wouldn't want to give that up".

If you mean in place of the current behavior of -fdefer-type-errors, I expect it's sometimes quite useful to know earlier when you're exercising magically untyped code (as compared to deliberately demarcated untyped code).

If you mean, "why don't they add -fdynamic-type-errors", an additional flag that subs in use of Dynamic in place of inconsistently typed code, that's certainly an interesting idea; given that terms are sometimes derived from types (typeclass polymorphism) it may not always be possible, and in any case may be a large engineering effort - I suspect Simon and company simply haven't gotten around to it.

I mean without any boiler plate whatsoever. Just "we can't determine what the type of some term x is, so let it be anything and check it at run time when it is used in a way that requires it to be of some specific type(s)".

That's what I had understood you to mean; what I was unsure of is whether you intended this to be the only mode of compilation - and addressed what seemed like each possibility in the second half of my post.

Sure, only mode. Inform me "this program is not known to be well-typed" or "this program is outright ill typed". Then, let me run it anyway, and correctly detect the consequence of the admonition with run-time info. Or I could choose not to run that program; I want mine well-typed.

In the presence of -Werror, this seems isomorphic to the notion of adding a '-fdynamic-type-errors' flag.

It can't be done in full generality because, as I mentioned, there are places where term-level values depend on types. If we don't know what type, we can't know what term.

We could certainly treat only those situations where behavior is ambiguous like '-fdefer-type-errors' currently treats any type mismatch, and add dynamic checks for the rest. It would be an interesting point in the space, though not one I would expect to use very often.