Jacques,
  I'd love to see this added to the distribution, even if only 
as an optional compile time flag. Allowing polymorphic recursion, and
mitigating the record naming problem are worthy goals, 

   Ohad.

> There are a few things that work well with this approach, polymorphic
> recursion being one. But it is not as general as it seems.
> A simple scheme is to assume that you can give explicitely a type to
> an identifier, use this type to resolve ambiguities, and check
> afterwards that this type is correct.
> With such a scheme,
>      let w : t = {x=1;y=2} in w.x
> will indeed be correctly handled.
> However, this breaks as soon as an annotation is lacking:
>      let w : t = {x=1;y=2} in
>      let v = w in
>      w.x
> Similarly, pairs won't work
>      let w : t * int = ({x=1;y=2}, 3) in (fst w).x
> Indeed, while w was given a special "assumed" type, propagating such
> assumed types through definitions and function calls is much more
> subtle.
> In a paper by Didier Remy and myself [1], we designed a system that
> could do a fair amount of "assumed" type propagation. This was
> intended for providing first class polymorphism and polymorphic
> methods, and was implemented in Objective Label. This could also be
> used for typing records, while some might see it as an overkill.
> But this is much more complex than what you are calling PRIOR.
> And this is not principal in the strict meaning (due to a mischevious
> side-effect of the value only prolymorphism rule).
> 
> I am currently working on reintegrating this feature in ocaml. However
> it is not yet clear whether it can be made cheap enough to make it
> into the main stream version (type inference becomes slower).
> And then some might discuss the fact it would require people to learn
> yet another set of rules about how assumed types are propagated.
> 
> Cheers,
> 
> Jacques
> 
> [1] Extending ML with semi-explicit higher order polymorphism,
>     Information and Computation 155, december 1999, pages 134-171.