Hi! There have been proposals to abandon generalisation for local let bindings because they make specifying and implementing the type system very complicated when extensions like multi parameter type classes, type functions and GADTs are taken into consideration. I agree with what the paper says in general, I'm just interested/concerned as to how abandoning local let generealisation would affect GHCi. While we rarely rely on the polymorphism of functions defined in local let bindings, I think a lot of programmers rely on the polymorphism of functions that they define with let in GHCi. I have a feeling that GHCi would be a lot less useful if it didn't allow us to define functions that are polymorphic in it. Also, what would the behavior be anyway? If we did

let f x = x

in GHCi and then inspected the type of f, what would GHCi report? Would it use defaulting and give us () -> ()? Or would it display a polymorphic type a -> a and then change that type to something monomorphic once we use f with some value? What if we defined several functions like this that called each other? So I think that if local let generalisation is abandoned, let bindings in GHCi would somehow have to be modified to remain polymorphic. Any thoughts?