New implementation for `ImpredicativeTypes`

[John Ericson]

On 9/2/21 11:04 PM, Richard Eisenberg wrote:

> On Sep 2, 2021, at 2:56 PM, john.ericson 
> <john.ericson at obsidian.systems <mailto:john.ericson at obsidian.systems>> 
> wrote:
>>
>> Does the most basic e.g.
>>
>> newtype Some f where
>>   MkSome :: forall a. f a -> Some f
>>
>> Have one of those problematic equalities?
>
> No. That's not a GADT -- the constructor doesn't restrict anything 
> about `f`.

Morally, sure, but GHC doesn't know about this.

I tried, and -XGADTSyntax + -XExistenialTypes = -XGADTs it seems.

>
> I think you're after newtype existentials. I think these should indeed 
> be possible, because what you propose appears to be the same as
>
> newtype Some f = MkSome (exists a. f a)
>
> We can probably support the syntax you wrote, too, but I don't want to 
> commit to that right now.

The syntax I wrote is already basically valid?

data Some f = forall a. Some (f a)

data Some f where MkSome :: forall a f. f a -> Some f

Is accepted

newtype Some f = forall a. Some (f a)

newtype Some f where MkSome :: forall a f. f a -> Some f

Is not with "A newtype constructor cannot have existential type variables"

I propose we teach GHC how these "GADTs" in fact merely have existential 
variables, and not the FC constraints that require the extra evaluation 
for soundness. Than we can get the operational/runtime benefits of what 
you propose for cheap. Don't get me wrong -- the other aspects in the 
paper this doesn't address are still quite valuable, but I think this is 
a useful stepping stone / removal of artificial restrictions we should 
do first.

This sort of thing is brought up in #1965, where it is alleged this is 
in fact more difficult than it sounds. All more reason it is a good 
stepping stone, I say!

John

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210906/44d3b766/attachment.html>