<div dir="ltr">Hello,<div><br></div><div>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?</div><div><br></div><div>-Iavor</div><div><br></div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Sat, May 5, 2018 at 8:48 PM Joachim Breitner <<a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:<br>
> Joachim, you are always a fount of interesting ideas.<br>
> <br>
> > On May 2, 2018, at 2:51 PM, Joachim Breitner <mail@joachim-breitner<br>
> > .de> wrote:<br>
> > <br>
> >   class C k (a : k) where meth :: a<br>
> >   meth :: forall {k} a. C k a -> k -> Constraint<br>
> <br>
> I think this is brilliant. But not only for this proposal! Imagine<br>
> this:<br>
> <br>
> class Num a where<br>
>   fromInteger :: Integer -> a<br>
> <br>
> fromInteger :: Integer -> forall a. Num a => a<br>
> <br>
> If we do that, then #129 is essentially solved, at no further cost to<br>
> anyone. (Note that in all Haskell98-style code, no one will ever be<br>
> able to notice the changed type of fromInteger.)<br>
> <br>
> This approach also allows for the possibility of reordering<br>
> quantified type variables for Haskell98-style constructors, if anyone<br>
> should want to do it.<br>
> <br>
> And it allows for updated types (including quantified variable<br>
> ordering, etc.) for record selectors.<br>
> <br>
> And it allows (maybe?) for giving good types to GADT record<br>
> selectors:<br>
> <br>
> data X a where<br>
>   Foo :: { bar :: Int } -> X Int<br>
>   Quux :: { bar :: Bool } -> X Bool<br>
> bar :: X a -> a<br>
> <br>
> GHC currently rejects the declaration for X, but it could be accepted<br>
> if only we could specify the correct type of bar. And now we can. I<br>
> don't particularly want to cook up the typing rules here, but I don't<br>
> think I'm totally crazy.<br>
> <br>
> GADT record selectors aside, the rule for these could be that the<br>
> top-level type signature must be equivalent w.r.t. the subtype<br>
> relation with the original type signature. That is, if the new<br>
> signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy<br>
> enough to check for. The implementation would probably do a little<br>
> worker/wrapper stunt.<br>
<br>
I smell a new proposal… what does this mean for #99? Will you want to<br>
revise it?<br>
<br>
Cheers,<br>
Joachim<br>
-- <br>
Joachim Breitner<br>
  <a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a><br>
  <a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.de/</a><br>
_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</blockquote></div>