The strange behaviour you get is because the occurrece of f in y gives rise to a top-level constraint (F Int Bool). Then with the definition z = f we get a second top-level constraint (F Int Char), and thence the error message
Couldn't match expected type `Bool' against inferred type `Char'
When using functional dependencies to combine
F Int Char, arising from a use of `f' at Foo12.hs:15:4
F Int Bool, arising from a use of `f' at Foo12.hs:12:4
However, with the definition z = x no constraint is genreated (since x does not have an overloaded type) and all is well.
This is an unexected (to me) consequence of lifting the Coverage Condition. Yet I do not want to re-impose it because (as 5.2 explains) it's sometimes useful to have it lifted.
I'm not sure what the Right Answer here is. It looks like another fundep brain-bender. I'm inclined to continue working on type inference for associated types!