Fix and simplify lub/glb

[rossberg]

Refactor lub and glb into a single unified operation and a few fixes:

• Handle abstract type bounds correctly by using promotion for the lub.
• Handle glb between incompatible abstract types without creating a vacuous cycle.
• Treat type field mismatches more orthogonally.
• Perform equivalence/subtype tests earlier, which should yield nicer results.
• Also prefer side that is named if there is a choice.
• Add more extensive tests.

While here, also removed subtyping between second-class types like Mut and Typ and Any/Non.

Fixes #515 (up to other potential pretty printing changes).

[dfinity-ci]

This PR does not affect the produced WebAssembly code.

[rossberg]

With @crusso on vacation, anybody else wants to review this?

[nomeata]

Not 100% confident on everything, in particular not subtyping on functions with type bounds, so another review by @crusso might improve quality. But if you want to get this out, here is a LGTM

[nomeata]

Suggested change

	| _, [] -> if rel == lubs then [] else fs1
	| [], _ -> if rel == lubs then [] else fs2
	| _, [] -> if rel == glbs then fs1 else []
	| [], _ -> if rel == glbs then fs2 else []

More symmetric with both cons_if below, and with combine_tags

[crusso]

This seems fishy to me, though I don't think its new behaviour:

As expected:

> func (x:{var y: Nat}): {y:Nat} {x};
stdin:7.33-7.34: type error [M0096], expression of type
  {var y : Nat}
cannot produce expected type
  {y : Nat}

So a var field never subtypes a non-var field, as expected.

Except we do allow it if the super type field has type Any.

> func (x:{var y: Nat}): {y:Any} {x};
func : {var y : Nat} -> {y : Any} 

And thus also:

> if true (object {public var x = 1}) else (object {public let x =1 });
{x = 1} : {x : Any}

If mut types really are second class, should they be included in Any?

[rossberg]

Yes, that matches what the subtype relation has always defined. We have discussed restricting it before. Originally the liberal rule was nice, because it made lubs/glbs fully defined and compositional. But with the advent of Typ, that's out the window anyway. So I went ahead and changed that as part of this PR, i.e., Non <: Mut <: Any is gone, and Mut and Typ are now handled analogously.

Also tweaked tests to prevent more liberal subtyping than intended.

[crusso]

Are there some words missing between the last two types in this error message or has run.sh just stripped them out?

[rossberg]

Yes, this is some artefact due to our test scripts. IIRC, @kritzcreek first ran into this a while ago and might be able to tell you more.

[kritzcreek]

Yeah it's one of the regexes in run.sh

[rossberg]

Do you remember which one? I can't spot one that would cause this.

[kritzcreek]

It's matching at common supertype

with:
^ *at ' from here (I think):

motoko/test/run.sh

Line 64 in 198c0ea

grep -a -E -v '^Raised by|^Raised at|^Re-raised at|^Re-Raised at|^Called from|^ *at ' $1 |

[crusso]

OK, not a real bug then

[rossberg]

Okay, this annoyed me, so I tweaked the regexp to not misfire on the error message. Seems to work. :)

[crusso]

I'm not too crazy about the use of exceptions for this - meant to be spec-like - can you not have combine_fields and (for arrays) a combine_element function that handles the special second class types, sans exceptions, and just assert on the second class types in combine?

[rossberg]

Yeah, I went back and forth on how to handle the partiality here. This way, its simplest and the structure of the function remains parallel to all others, especially sub, which is valuable. If we wanted a different structure, then that should apply everywhere and better be reflected in the type definition itself.

Not too worried about the spec aspect in this case -- these are algorithms that wouldn't appear in a spec. Their declarative spec is that of a lub/glb wrt the subtype relation.

[crusso]

Fair enough.

[crusso]

LGTM

[rossberg]

Thanks Claudio! Now please turn off this damn computer!