Automatically print full names when types don't match but have the same short name

[briangmilnes]

The attached file shows this bug on the last definition (which was under construction), print_implicits/universes was on but provided no help. (Error 19) Subtyping check failed; expected type p’: pfp n {seqisperm n s1 p s2}; got type p: pfp n {seqisperm n s1 p s2}; The SMT solver could not prove the query. Use --query_stats for more details. Related location (C-c C-’ to visit, M-, to come back): /tmp/ParFunPermBug.fst(109,19-109,38) Mark set print_full_names was required.

This raises the question that when two types don't match, we should test if all of their short names are the same, and in which case print or reprint with the full names.

ParFunPermBug.txt

[briangmilnes]

And if you're going to fix that printing, you could print the mismatched types in alignment to each other to make the difference simpler to understand, or even print a message as to where the difference occurs.