Of course you could say it's a subset of unification, as it is.
But my previous reply is a little content-free, as what you're really asking for is how we solve the same problem that typeclasses solve in Haskell.
Very briefly, there's two ways of asking whether a caller can change the type of a parameter. The normal way is to say, are all the possible values of the caller's type in the set of nouns that the parameter defines? This is what I call "geometric polymorphism."
But there's also "generic polymorphism," in which we ask: will the Nock code that was generated for the parameter type, actually work with the type we're calling it with? A really stupid way to ask this is to recompile the function, with the parameters exchanged for the arguments. The Hoon approach is a little bit smarter than this but not much.
So, with these two approaches, you basically get variance and genericity, which is all of polymorphism.
It's difficult to have a conversation with someone using their own terms for well-established concepts.
If I understand you correctly, what you're calling "geometric polymorphism" is usually called structural typing or subtyping, and what you're calling "generic polymorphism" is usually called duck typing.
Duck typing isn't amenable to static typechecking, so it's not comparable to Haskell's typeclasses.
Looks like I'm behind on my programming language theory research! Typed Racket and soon, Typed Clojure, are actually adding optional static typing to duck-typed languages. Are you doing something similar?
The question posed by colanderman's expression is valid if and only if there is a type containing both 5 and "foo".
Here's Haskell's answer:
Prelude> \ a b -> a == b && b == 5 && a == "foo"
No instance for (Num [Char]) arising from the literal `5'
Possible fix: add an instance declaration for (Num [Char])
In the second argument of `(==)', namely `5'
In the first argument of `(&&)', namely `b == 5'
In the second argument of `(&&)', namely `b == 5 && a == "foo"'
Here, the typechecker took the most general type of 5, namely some type belonging to the Num typeclass, and discovered that the type of "foo", which is [Char], isn't an instance of the Num typeclass, or, in Java parlance, doesn't implement the Num interface. This means there is no type containing both 5 and "foo", hence — type error.
You're asking about implicit conversions, which are an undisputable evil. However, attempting to provide answers to invalid questions also isn't very good.
The central theme of this talk is not just implicit conversions — it's surprising answers to invalid questions. A much better way to handle an invalid question is to reject it as early as possible — Fail Fast. With a static type system, this can be very early indeed.