[ghc-steering-committee] Please review "Visible 'forall' in types of terms" #281

[Richard Eisenberg]

I agree with Joachim here, who has unpacked this better than I did.

For me, the key observation is "but that's not really #281's fault". That is, #281 just happens to be the first place where we're hitting this problem head on.

> On Nov 23, 2020, at 3:10 AM, Joachim Breitner <mail at joachim-breitner.de> wrote:
> 
> My impression is that all (most?) of
> those working towards a Dependent Haskell world assume that we get a
> unified namespace with no punning

That indeed has been my assumption, but I've been reminded recently that this assumption is just that. In particular, combining types and terms is not strictly necessary to support dependent types. I do think it's necessary to have the smooth, happy dependent types I yearn for, but maybe we can't always get what we want. I don't want to distract this particular thread with the details (which would take some work to spell out), but I will admit that this merger is not strictly necessary for dependent types -- and perhaps the merger is precisely what I mean when I use "ergonomic" in #378.

> Few are proposing to stick to
> a world of two namespaces and punning and make _that_ ergonomic. Is
> that impression correct?

For those of us working in this area, I think that is correct. There may be people about the excited about ergonomic dependent types that don't merge, but I don't believe they're actively working on designs.

> 
> Do local modules (#283) alleviate the punning problem a bit? Given
> `data T = T`, could we make it so that T is the type and T.T the
> constructor?

Interesting point. Yes, in #283's full glory. Maybe this is good motivation to make the requested updates there.

> 
> But this really isn't the right place to throw out shower ideas. I
> wonder if it would help if someone could maintain a wiki page with an
> overview of all the numerous proposals and ideas thrown around to
> tackle the problem about how we get from a world of two name spaces and
> punning to one with one namespaces and no punning.

Yes. I'll do this if no one beats me to it. But it may be a few days.

Thanks,
Richard