I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do next week.

Richard

On May 24, 2018, at 1:54 PM, Iavor Diatchki <iavor.diatchki@gmail.com> wrote:

Hello,

based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment.   Overall, I agree that it would be nice to come up with a consistent notation for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time?

-Iavor




On Sat, May 5, 2018 at 8:48 PM Joachim Breitner <mail@joachim-breitner.de> wrote:
Hi,

Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:
> Joachim, you are always a fount of interesting ideas.
>
> > On May 2, 2018, at 2:51 PM, Joachim Breitner <mail@joachim-breitner
> > .de> wrote:
> >
> >   class C k (a : k) where meth :: a
> >   meth :: forall {k} a. C k a -> k -> Constraint
>
> I think this is brilliant. But not only for this proposal! Imagine
> this:
>
> class Num a where
>   fromInteger :: Integer -> a
>
> fromInteger :: Integer -> forall a. Num a => a
>
> If we do that, then #129 is essentially solved, at no further cost to
> anyone. (Note that in all Haskell98-style code, no one will ever be
> able to notice the changed type of fromInteger.)
>
> This approach also allows for the possibility of reordering
> quantified type variables for Haskell98-style constructors, if anyone
> should want to do it.
>
> And it allows for updated types (including quantified variable
> ordering, etc.) for record selectors.
>
> And it allows (maybe?) for giving good types to GADT record
> selectors:
>
> data X a where
>   Foo :: { bar :: Int } -> X Int
>   Quux :: { bar :: Bool } -> X Bool
> bar :: X a -> a
>
> GHC currently rejects the declaration for X, but it could be accepted
> if only we could specify the correct type of bar. And now we can. I
> don't particularly want to cook up the typing rules here, but I don't
> think I'm totally crazy.
>
> GADT record selectors aside, the rule for these could be that the
> top-level type signature must be equivalent w.r.t. the subtype
> relation with the original type signature. That is, if the new
> signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy
> enough to check for. The implementation would probably do a little
> worker/wrapper stunt.

I smell a new proposal… what does this mean for #99? Will you want to
revise it?

Cheers,
Joachim
--
Joachim Breitner
  mail@joachim-breitner.de
  http://www.joachim-breitner.de/
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee