Re: lost polymorphism in Typed Tagless Final Interpreters

I do find it very non-obvious. I understand the semantic difference (due to seq), but I don’t understand the typing difference.

(So I understand why the compiler can’t automatically eta-expand, but I don’t understand why it would help anything to do so.)

Jeff

> On Nov 12, 2025, at 1:43 PM, Olaf Klinke via Haskell-Cafe <[email protected]> wrote:
> 
> 
>> 
>> So change lit <$> safeRead n to (\x ->
>> lit x) <$> safeRead n, for example.
> 
> Does anyone else find this highly non-obvious? 
> SPJ gives an example 
> https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-543683756
> of a context that can indeed distinguish, semantically, a function and
> its eta expansion. But the fact that, for the benefit of soundness,
> there must exist contexts where one can be a well-typed program while
> the other is not, is still mysterious to me. 
> 
> Can a type system with polymorphism really not do better than this? The
> discussion thread has some more interesting posts, e.g. 
> https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-544377361
> https://github.com/ghc-proposals/ghc-proposals/pull/287#issuecomment-1120461992
> 
> At least, thanks to Jaro, the error index now explains when you should
> eta-expand. 
> https://errors.haskell.org/messages/GHC-83865/
> 
> Olaf
> _______________________________________________
> Haskell-Cafe mailing list -- [email protected]
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list -- [email protected]
To (un)subscribe, modify options or view archives go to:
Only members subscribed via the mailman list are allowed to post.