bar :: forall a b. (a ~ Int) => a -> b -> a
Is it the case that `:t bar @Bool` will print
bar :: (Bool ~ Int) => Bool -> b -> Bool
This looks particularly confusing without the explicit `forall`, although it seems questionable either way.
Yes, you understand correctly. `:t bar @Bool` will print that unfortunate type. I agree this is questionable. But I don't know how to do better. The current state of affairs is awkward in a different way, in that `:t bar @Bool` errors (that's OK) and `:t bar @Int` prints `forall {b}. Int -> b -> Int`, even though a further visible type application is possible. Perhaps worse, `:t bar` today prints `forall {b}. Int -> b -> Int` even though the next variable to be instantiated is `a`. This is why we have `:type +v`.
The direction in the proposal came about in wondering if it's possible to improve the mechanics of `:t` (without the `+v`). After we thought of doing maximal instantiation of inferred arguments (but no generalization), then we realized we could drop `:type +v` as redundant. I agree it's something of an uneasy compromise here, but I think any choice is going to have unfortunate behavior in some scenarios.
Richard