Our philosophy is that the typed Pyret language is an explicitly-typed one. Inference is just a convenience to save you some amount of typewritering. We want to do a good enough job of it, and if you want to get more specific, you do it yourself. For instance, in the foreseeable future we do not plan to ever infer a refinement. So I think that addresses your example.

Furthermore, we aren't going to play the cute trick of having an inference process that is so consistent with the type-checker that we can get rid of a type-checker. One nice thing about old fashioned recursive-descent type-checkers is that they give simple and familiar error messages; I don't know of any research papers that have been written about better error reporting by them (at least in the past few decades). That's a feature. [NB: There's always an exception. Hopefully my point is clear.]

So, whatever type we infer is one that gets fed to the type-checker to check against the function. Typically, assuming the function has passed its tests, the function should be consistent with its inferred type, unless the tests didn't cover the code properly.

What happens with code that can apply to multiple types, i.e., parametrically polymorphic code? We made an explicit decision to not have union types; had we had them, this would have been more sticky. But because we don't, we simply assume you mean to use the function in a polymorphic fashion, and that's the type we "infer". [Put differently, if you have a polymorphic function, you should test it on at least two different types!]

For reporting errors, we intend to make a distinction between declared types and inferred ones -- a distinction that I don't believe is commonly made in other type inference error presentations. For instance, inconsistency between two inferred types should perhaps be treated a bit differently than inconsistency between two declared types or between an inferred and a declared type.

More broadly, types are specifications. The point of a spec is to provide a redundant statement of program behavior, that can be checked against an implementation. From that perspective, inferring the type from the implementation is a strange idea: one shouldn't be inferring specs from code. [Yes, I know, it's been fashionable to infer "specs" from code for over a decade now. I would not call those specs -- they're more like summaries of the code.]

But tests, to my mind, are a lightweight form of specification, so it does make sense to infer one specification from another [just as people have gone the other way and used specifications to derive tests: the area of specification-driven test-generation]. Especially since it's being backed up by a true type-checker.

As I said, these are all pretty novel and possibly heretical ideas. But this is the experiment we're trying.