[ghc-steering-committee] Discussion on #155 Type Variable in Labmdas

[Eric Seidel]

On Mon, Mar 4, 2019, at 07:57, Simon Peyton Jones wrote:
>  
> 1. Should we allow binding type variables that are not explicitly 
> quantified with a forall? I'm concerned about the potential for 
> breaking code should GHC's rules for ordering quantifiers change. Does 
> GHC already guarantee a particular ordering?
> 
> 
> See  my comments 
> <https://github.com/ghc-proposals/ghc-proposals/pull/155#issuecomment-469241834> on GitHub.

Ah, thanks for the clarification. In retrospect, I guess it makes sense that GHC guarantees an ordering. TypeApplications would have been quite disruptive if we could only specify types that were explicitly quantified..

> 2. I wonder if supporting type binders in inference mode is as hard as 
> the proposal fears.
> 
> 
> I think it’s hard. 
> 
>  f @a x = x
> 
> we could infer any of.
> 
>  f :: forall a b. b -> b
> 
>  f :: forall a. a -> a
> 
>  f :: forall b a. b -> b

I don't know how we'd infer the 2nd option, even though that's surely what was intended. There's simply no link between the `a` and `x` in the code. So I'd expect GHC to infer either the 1st or 3rd type, and emit a warning about the unused type abstraction similar to the existing warnings about unused variables or unused foralls. Does the order of tyvars matter here? Doesn't seem so, as `b` should be marked inferred, and thus ineligible for VTA.

> Roughly, it’s as hard as figuring out impredicative polymorphism I 
> think. Let’s not go there 😊.

Is it really like impredicative polymorphism? Based on my (very limited) understanding of impredicativity, the difficulty is in figuring out where to place quantifiers. But with explicit type abstraction the user has told us precisely where the quantifier goes! So this seems like a rather different, and simpler, problem than impredicativity.