Re: lost polymorphism in Typed Tagless Final Interpreters

> 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.