[ghc-steering-committee] #371: Stop treating ~ magically. Rec: weak accept

[Richard Eisenberg]

To my deep surprise, the following program is accepted:

> {-# LANGUAGE GADTSyntax, ExistentialQuantification #-}
> 
> module Bug where
> 
> data G a where
>   MkG :: a -> G Int

but the following additional definition is rejected:

> foo :: G a -> a
> foo (MkG _) = 5

Adding -XTypeFamilies fixes that last piece, though.

Looking through the source code, GADTs implies GADTSyntax and MonoLocalBinds, either GADTs or ExistentialQuantification allows the declaration of existential variables or a refined return type, either GADTs or TypeFamilies allows the use of the `~` syntax, and either GADTs or TypeFamilies allows pattern-matching on a constructor with an equality in its context. So, GADTSyntax, ExistentialQuantification, and TypeFamilies together imply all the functionality of GADTs.

This is all very strange, though, and should probably be tidied up. Not in this proposal though.

Richard

> On Apr 23, 2021, at 2:54 PM, Vladislav Zavialov (int-index) <vlad.z.4096 at gmail.com> wrote:
> 
> While the use of (~) itself no longer requires -XGADTs, the usual desugaring of GADTs still does. So this will require the extension:
> 
> data G a where
>  MkG :: G Int
> 
> even though this will not:
> 
> data T a where
>  MkT :: (a~Int) => T a
> 
> Perhaps that is what you meant by ‘vacuous’, but I wouldn’t go as far as to say that -XGADTs becomes implied by -XGADTSyntax and -XExistentialTypes.
> 
> - Vlad
> 
>> On 22 Apr 2021, at 12:25, Spiwack, Arnaud <arnaud.spiwack at tweag.io> wrote:
>> 
>> I'm still not sure what problem this proposal solves. The proposal alludes to some code simplification but doesn't give me a good idea of how much simpler this would make the code.
>> 
>> Also note that -XGADT becomes mostly vacuous with this proposal: -XGADTSyntax + -XExistentialTypes imply GADTs (both are in -XGHC2021). Not that I mind, really, I actually probably prefer it this way. But it's worthy of notice.
>> 
>> _______________________________________________
>> ghc-steering-committee mailing list
>> ghc-steering-committee at haskell.org
>> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>