But Crystal recently had to walk back from global type inference as they found it was not realistic in practice, didn't they?

Why is it not realistic? Is it too slow or too unreadable?

You could dig up the mailing list messages at the time, but yeah it was slow and I think it produced error messages that were extremely hard to use - it would decide the type of functions was something nonsensical and then report that as an error at all the call sites instead.

Makes sense, bad errors is also why I don't use type inference in my code.