The "infoStr" I felt caused more noise and confusion, so I remove it.
I also pushed the type mismatch message done 1 line, so it displays
better multi-line (the "Found" and "Required" are alined).

TypeComparer's compareAtoms assumes it has an answer to subtyping if one
of the types has atoms and the other doesn't.  But an unreduced match
alias won't have atoms, so we shouldn't bail early.

Co-Authored-By: Matt Bovel <matthieu@bovel.net>

If the skolem-widened scrutinees are the same and the cases correspond,
then the match types are the same.

Also, with inlining the type embeded in inlining's Typed expression will
be without going through type-avoidance, so they won't be skolems.  So
we look to widen inline proxy term refs, in addition to skolems.

Co-Authored-By: Matt Bovel <matthieu@bovel.net>

Co-Authored-By: Matt Bovel <matthieu@bovel.net>

From the Match Type paper, typing rule S-Match5 requires that the LHS
scrutinee "Ss" is a subtype of the RHS scrutinee "Ts": Ss <: Ts.  It's
not required that they are the same type.  This covers widening a skolem
or inline proxy tp1 scrutinee, without erroneously widening the RHS tp2
scrutinee.