A tricky case of isorecursive subtyping

[tlively]

I've found what I believe to be a bug in Binaryen's implementation of the isorecursive type system described in #243, but it's a little tricky so I wanted to double check my understanding. Consider the following types (using made up subtype notation):

(type $A (struct))
(type $B (struct) sub $A)

(type $A' (struct))
(type $B' (struct) sub $A')

(type $X (struct (ref $A)))
(type $Y (struct (ref $B')) sub $X)

Here $A defines the same type as $A' and $B defines the same type as $B'. The subtyping $Y <: X is valid only if $B' <: $A, which should be true due to the type equivalences. The problem is that Binaryen checks for subtyping validity before canonicalizing the types, so it considers $A and $A' to be distinct types at that point and throws an error because it does not think that $B' <: $A is true.

Am I correct that this is a bug? Is the fix as simple as canonicalizing types before checking subtype validity?

[tlively]

Closing this because the fix is definitely as simple as canonicalizing before validating, and I have WebAssembly/binaryen#4506 up to fix it in Binaryen. It makes sense that you cannot validate supertypes until you have determined type equality, although this was a moot point in the nominal system since all declared types were distinct.

[rossberg]

Yes, that'a right. Validation depends on subtyping depends on equivalence. So if you want to implement the former without checking the latter algorithmically, you have to canonicalise upfront.