Not really. That's the lifetime system, which is not the same thing. "Existential Types for Imperative Languages", also by Dan Grossman, explains more of the motivation, but the borrow check is a hybrid of the two solutions he presents.

Borrowing itself is something with a long history, but the whole "unique loan paths" thing makes Rust's solution distinct from a lot of the stuff you find in the research literature.

It's more akin to C++ templates, where the type checker only has a bounded number of reductions it will do before it gives up. Aside from writing something that really is infinite and a limit of trillions of reductions - which wouldn't really be a useful program - it ends up as a type error as you'd expect. This also only happens with -XUndecidableInstances, which frankly isn't really one of the most common extensions, I'd say.

That said, in practice, most Haskell programmers seem to largely consider subtyping a misfeature anyway, and approximations of it elsewhere in the ecosystem use things like RankNTypes to give a 'feel' for subtyping where you can do things like "use any instance of a more general base type, in place of that type, right here". The infamous lens library does this to great effect.

> previously allowed only by Haskell, and then not with user-defined types

I don't know what you mean here - Haskell has, until recently, never allowed overloaded literals for certain syntactic forms, like lists. For the other cases, though, like numerics, you have always been able to have polymorphic literals, which can be instantiated to user-defined type. The most general type of `1` by itself with no defaulting is `1 :: Num a => a`, and there's certainly no problem with instantiating `a` to whatever user-defined type you have, providing it can sensibly be constructed from a base-10 decimal value (meaning, you have a function `toInteger :: Integer -> a`)

These days, lists are also syntactically overloadable by a similar convention, through value polymorphism/type classes.

Type inference in a OO language is still considered, if not impossible, at least very impractical. Swift, Scala and Rust avoid most algorithmic complexity and ambiguity by mostly supporting only type propagation instead of type inference, and thus require annotations on function parameters.

http://cowlark.com/2009-11-15-go/