Improve type errors WIP

Don't merge yet. This improves a bit an error message and analyses the other one — we saw these problems with my (intentionally) faulty examples in System U.