Introduce an equate judgment

[nilehmann]

The only way we have to relate types is via subtyping. This plays poorly with invariant type constructors because we must apply subtyping both ways. This is especially bad if invariant constructors are nested, which is common with mutable references.

For example, consider a type S<T> invariant on T. If we want to prove the judgment

&mut S<i32{v: v > 0}> <: &mut S<i32{v: 0 < v}>

We will generate the following derivation

       v>0 => 0<v              0<v => v>0                 0<v => v>0                 v>0 => v<0
------------------------  ------------------------   -----------------------   ------------------------
i32{v:v>0} <: i32{v:0<v}  i32{v:0<v} <: i32{v:v>0}   i32{v:0<v} <: i32{v:v>0}  i32{$v:>0} <: i32{v:v<0}
--------------------------------------------------   --------------------------------------------------
        S<i32{v:v>0}> <: S<i32{v:0<v}>                         S<i32{0<v}> <: S<i32{v>0}>
        ---------------------------------------------------------------------------------
                          &mut S<i32{v:v>0}> <: &mut S<i32{v:0<v}>

Maybe we could have an equate judgment and switch to that when we have invariant subtyping. This way, I think we could define most of the judgment structurally and "push down" the double implication. I'm thinking we can get a derivation like this

         v>0 => v<0  v<0 => v>0
        ------------------------
        i32{v:v>0} ≡ i32{v:v<0}
     ------------------------------
     S<i32{v:v>0}> ≡ S<i32{v:v<0}>
----------------------------------------
&mut S<i32{v:v>0}> <: &mut S<i32{v:0<v}>                  

In this simple example, it sounds like it should work because both types are structurally equal (up to the differences in the predicate), but in general, this is more complicated because existentials can appear out-of-order and there are types that are not structurally equal but should be (judgmentally) equivalent (they would be if we apply subtyping both ways). For example, the following should hold

∃a. (i32[a], ∃b. {i32[b] | a > b}) ≡ ∃a,b. ({i32[a] | b < a}, i32[b])

[nilehmann]

Also, more than out of order, types can differ in the number of existential and still be equivalent, e.g.,

i32[0] ≡ ∃v. {i32[v] | v == 0}

So I think in general we need to fall back to subtyping both ways in some cases, but what could help is to canonicalize types by pulling out constraints and existential to increase the chances of types being structurally equal. For example, we can canonicalize

∃a. (i32[a], ∃b. {i32[b] | a > b}) ≡ ∃a,b. ({i32[a] | b < a}, i32[b])

to

∃a,b. { (i32[a], i32[b]) | a > b } ≡ ∃a,b. { (i32[a], i32[b]) | b < a }

so the types are structurally equal up to the difference in the predicate.