<div dir="ltr"><div dir="ltr"><div dir="ltr">Hello,</div><div class="gmail_quote"><div dir="ltr" class="gmail_attr"><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
> 2. I wonder if supporting type binders in inference mode is as hard as <br>
> the proposal fears.<br>
> <br>
> <br>
> I think it’s hard. <br>
> <br>
>  f @a x = x<br>
> <br>
> we could infer any of.<br>
> <br>
>  f :: forall a b. b -> b<br>
> <br>
>  f :: forall a. a -> a<br>
> <br>
>  f :: forall b a. b -> b<br>
<br>
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.<br></blockquote><div><br></div><div>Like Eric, I would expect that the type of `f` should be something like (1) or (3), except that the inferred polymorphic variables should not be visible (i.e., you shouldn't be able to explicitly apply them), in which case (1) and (3) are essentially the same:</div><div><br></div><div>f :: forall a {b}. b -> b</div><div><br></div><div>-Iavor</div><div><br></div><div>  </div></div></div></div>