> This is to say, I don't think inference and gradual systems are necessarily at odds, but could potentially work together, although that doesn't happen today.

Type inference demands some rigidity in the type structure of a language. You must have the right amount of polymorphism: the STLC has too little, System F has too much. If you want both type operators and type synonyms, then operators can't be applied to partially applied synonyms [0], because higher-order unification is undecidable. If you want subtyping, you also have to do it in a certain way [1]. More generally, the type language must have a nice enough algebraic structure to make it feasible to solve systems of type (in)equations, because that's how inference works.

Your post contains a link to a paper [2] that contains the following passage:

> In this paper, we present a way to achieve efficient sound gradual typing. The core component of this approach is a nominal type system with run-time type information, which lets us verify assumptions about many large data structures with a single, quick check.

I have no way to confirm this claim at the moment, but it seems entirely reasonable. Checking structural types requires doing more work. But it is this very structure that makes type inference possible and useful.

So, yes, it seems that inference and gradual typing will be difficult to reconcile.

---

Footnotes:

[0] http://cstheory.stackexchange.com/questions/32260/ (I am the author of this stupid question.)

[1] http://news.ycombinator.com/item?id=13781467

[2] http://www.cs.cornell.edu/~ross/publications/nomalive/nomali...