[TYPES] Minimal type reconstruction

[Didier Remy]

> That is, if a let-bound variable is not used polymorphically, we may  
> just as well infer a monomorphic type for it. In some specific  
> situations, such a "minimal" completion may even be preferable over a  
> fully polymorphic one. (Looking through a Curry-Howard lens, we are  
> after the "simplest" proofs.) Although I'm quite sure it has been  
> considered before, I have not found any discussion in literature of  
> the problem of finding minimal completions. Can anyone on this list  
> provide me with pointers to such discussions?

Dear Stefan,

I think that this is exactly the problem studied by Nikolaj Bjorner in the
case of ML in his paper "Minimal Typing Deriviations" presented at the ML
workshop in 1994 [http://theory.stanford.edu/people/nikolaj/ml-work94.ps]

Best wishes,

         Didier