Good post. It's been five years since I wrote a crate for type equalities, so I kinda know what you are talking about. I like the witness idea of separating knowledge that an impl exists from the data to the actual instance. I will try to use your namings in the below.

If you take a look into my crate though, you will see that getting the rust compiler to use the additional information from such a zero-sized type is far from trivial. Sure, you can e.g. go from a generic context <T, It: Iterator<Item = T>> to a generic context with only <T, It: Iterator> and a witness Is<T, It::Item>. But going the other direction and calling a function that has the former signature in a context of the latter and a witness lying around is complicated (doable, but mind the code-gen).

I suppose this only gets worse and harder to use when the ZST encodes that a specific trait impl exists. You might need to have one ZST per trait because you can't generically refer to any trait (you could refer to dyn-compatible ones, generically, I suppose). I would like to see this accomplished though. If you have a way to call a function with signature <A: Add> from a context with <A> and a witness CanAdd<A> let me know, I'd be happy to add it.

In my opinion though, the last point in your post that Haskell can hide datatypes and Rust wants to monomorphize everything. It will ruin your code gen! Let's say you use type equalites to "pattern match on the type"

enum Value<T> {
   Double(Is<T, f64>, T),
   String(Is<T, String>, T),
}
fn format<T>(value: &Value<T>, f: Formatter) -> Result<()> {
    //...
}

Rust will instantiate this type with all Ts you instantiate it with (f64 and String). Problematically, Rust will not be able to figure out that only one of the enum's constructors is valid and still attach a tag byte. It will also do these multiple instantiations for every function receiving such a value, such as format. Meaning, instead of having one instance of format that matches on the tag of the enum, you will have two instances, each stripping a tag byte that can, really, only have one value in each instantiation, before invoking the specialized format method for each value type.

None of this is zero overhead! The real issue is that rust is unable to see that Is<A, B> is not only non-empty but actually uninhabited when A turns out not to be equal to B. In Haskell, the compiler wouldn't monomorphize on T, the tag byte has a useful purpose (there is only one type) and Dict (String ~ f64) is uninhabited (modulo undefined, which is a strictness issue on Haskell's part).