@garrigue I believe the following code is close to the idea, it’s just a piece of code hacked together as essentially I wanted a instance_poly but in place.
It can type the example that started this thread and also fails to type all the unsound examples that you sent to me up to now.
It also rejects the example that I gave, so effectively any usage of the local type variable needs to be explicitly annotated as always but at least the syntax for named parameters is not terrible.
(* fails *)
let rec id (type a) (x: a): _ = ...
I believe the implementation is unsound because the way it set the levels of everything, but there is anything fundamentally unsound on the idea?
It is essentially improving the type approximation and dealing with the problem that the pattern will be typed as '_a and the approximation will be 'a -> 'a but when unified with '_a it leads to '_a -> '_a which seems just an artifact and nothing meaningful as in reality the ident is not constraining the type at all, so in this code I fix the variables levels and the types levels to generic which definitely leads to bugs(as it fails even to compile the stdlib fully).