EDIT: I've been chewing over the following:

> This means that we can trivially translate a dynamically typed program into a statically typed program, though obviously we don't gain anything by that at this point (this is essentially an argument that Bob Harper has advanced before) and we pay for it in additional verbosity.

This is exactly the opposite of the argument I advance below; you're claiming that there is a "local" translation from dynamic to static. And on reflection, you might be right, but I'm not entirely sure. It hinges on exactly what counts as "local". Translating away exceptions, for example, requires inserting case-analyses which propagate an exception if one has been thrown literally everywhere in your program. It's "global" in the sense that it touches every node in the program; it's "local" in the sense that the transformations performed don't involve any global knowledge or analysis. I'm rereading Felleisen's paper now to see how precisely he defines things.

ORIGINAL:

> I had Matthias Felleisen's characterization of expressiveness [1] in mind (incidentally, he's also one of Racket's authors).

Great! I believe, by that definition, your assertion that "good" typesystems don't reduce expressiveness is false, at least for common type systems such as Haskell's, Java's, ML's, etc. There are plenty of programs which require non-local rewriting ("a global reorganization of the entire program") in order to appease the typechecker.

A simple example can be adapted from the expression problem: suppose I'm writing an compiler for a simple language, so I have an AST datatype and some functions on it. Then I add a pass to my compiler that removes a certain feature from the language I'm implementing - a certain branch of the AST. Now I wish to simplify my backend by removing the case which handles this branch of the AST. I cannot do that without either dynamically failing in that case (which a type system might even prevent me from doing) or introducing an entirely new AST type which does not have that branch - but this could require duplicating or else considerably generalizing existing code that operates on the AST (a global reorganization). Of course, a sufficiently powerful typesystem might let me do that, but for any typesystem you name, I suspect a similar example can be procured.

To get more precise, the "feature" we're considering adding is "ignoring the typechecker and running anyway". For example, GHC's -fdefer-type-errors. The question is "can any legitimate program written with -fdefer-type-errors be locally translated into an equivalent program that typechecks without -fdefer-type-errors". Without reaching for an explicit escape hatch like unsafeCoerce (which is analogous to "unsafe" blocks in Rust), I think the answer is no.

First, let me say that I think you're right that expressiveness is reduced. In the best case, all of that reduction is of things we don't want to express because they are incorrect - but in practice (and probably in theory!) the boundary will always be fuzzy.

That said, with regard to your "kill a branch in your AST" example, you can kill a branch with Void:

    import Data.Void

    frobnicate :: Either a Void -> a
    frobnicate (Right x) = absurd x
    frobnicate (Left x) = x

Now you can rely on no-one accidentally handing you a Right expecting you to do something reasonable with it.

> Great! I believe, by that definition, your assertion that "good" typesystems don't reduce expressiveness is false, at least for common type systems such as Haskell's, Java's, ML's, etc.

Haskell is not very good at extensible runtime polymorphism (one of its weaknesses). Try OCaml's polymorphic variants.

Okay, then I can pick another example: A dictionary where the type of the values depends on the key they're inserted under. (For example, a representation of the closure of a function in a typed language.) Of course, then I can go to a dependently typed language, but are you really going to tell me that only dependently typed languages count as "good" static type systems?

I am not arguing completeness here; a type system is not a full-blown specification language and does not have to be. (I actually tend towards the point of view that trying to make them complete specification languages has limited practical value, but that's a different issue.)

The point here is that the type system does not restrict me from implementing a data structure that adheres to this constraint, even if it does not enforce it for me.

You can do this in GHC Haskell with existential quantification, or trade static checks for runtime with Data.Dynamic.

(Again, not arguing against your thesis here.)

After quickly scanning https://realworldocaml.org/v1/en/html/variants.html, isn't the same thing accomplished by GADTs?

The point of polymorphic variants is that the entire type doesn't have to be fully defined in one place; you can have partial definitions in a module and those definitions can even overlap. You can have (say) [ `Int of int | `String of string ] in one module and [ `String of string | `Char of char ] in another, and the typechecker will handle intersections and unions of these types.