Hi,
The summary is that the definition of what is "local" is not what one might expect: only things that depend
on variables in scope are considered to be locals, other bindings, that could be lifted out (e.g., like `p` in both examples)
are not considered local and are generalized. Of course, with implicit parameters this is not what one might hope for...
A while back there was a discussion about adding a construct for monomorphic bindings to the language (I think the proposed notation was something like "x := 2").
Perhaps we should revisit it, it seems much simpler than the rather surprising behavior of `MonoLocalBinds`.
-Iavor