Datatype (and Newtype) contexts: improvement

--===============0736583950052802949==
Content-Type: multipart/alternative; boundary="000000000000f86ab805b19760a8"

--000000000000f86ab805b19760a8
Content-Type: text/plain; charset="UTF-8"

(For some background to my thinking see here
https://mail.haskell.org/pipermail/haskell-cafe/2020-September/132714.html )

There's a part of the spec for DatatypeContexts that's been there since the
beginning (1991), but doesn't seem right to me. The effect of the 1999
'clarification' to the spec makes it seem even less right.

From the 1991 memo "each constructor gets a context which is a subset of
that given in the @data@ decl, containing all the constraints on the free type
variables of the constructor signature, and no others."

So we get (example from the 1998 Language Report)

    data Eq a => Set a = NilSet | ConsSet a (Set a)

    ===> NilSet :: forall a. Set a
    ===> ConsSet :: forall a. Eq a => a -> Set a

Well, in the type signature for NilSet, `a` _is_ free, why can't it get the
constraint? It's easy enough to give a signature with constraint for some
appearance of `NilSet` -- except in the one place I desperately want one,
that is in patterns. I can define

    nilSet = NilSet :: Eq a => Set a

and use that on rhs of function definitions, etc. The compiler doesn't seem
to come crashing down around my ears. Whereas without the `Eq a`, you can
write `NilSet :: Set (Int -> Int)` without complaint to produce an unusable
value -- something that will cause complaints every other place you try to
consume it or Cons to it. Compare

    emptyS1 NilSet = True           -- inferred :: Set a -> Bool
    emptyS1 _      = False

    emptyS2 (ConsSet _ _) = False  -- inferred :: Eq a => Set a -> Bool
    emptyS2 _             = True

Those two definitions are morally equivalent, but get different types. Note
that prior to the 1999 'clarification' GHC would have given them both the
same signature without the `Eq a`. The brains trust in 1999 was firmly of
the mind the constraint should be exposed everywhere. If they'd been asked
about that type for NilSet and how it didn't expose the constraint, I
wonder what they'd say?

Anyhoo, this note is to say it seems easy enough to modify Hugs  to give
the full set of constraints for every data constructor (and consequently
get those exposed, so the two definitions form `emptyS` above get the same
type, with the `Eq a`).

Would the concern in the 1991 memo still apply in 1999, or 2006 when Hugs
development ceased? "I was persuaded ... by John's comments, and by the
fact that many more cases of ambiguity are likely to arise otherwise." John
Hughes(?) Anyway I can see no comments on the forum. Would the ambiguities
be any worse than those for Numeric Literals being `Num a => a`? Or does
the defaulting mechanism rescue those?

AntC

--000000000000f86ab805b19760a8
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">(For some background to my thinking see here=C2=A0<a href=
=3D"https://mail.haskell.org/pipermail/haskell-cafe/2020-September/132714.h=
tml" target=3D"_blank">https://mail.haskell.org/pipermail/haskell-cafe/2020=
-September/132714.html</a>=C2=A0)<div><br></div><div>There&#39;s a part of =
the spec for DatatypeContexts that&#39;s been there since the beginning (19=
91), but doesn&#39;t seem right to me. The effect of the 1999 &#39;clarific=
ation&#39; to the spec makes it seem even less right.</div><div><br></div><=
div>From the 1991 memo &quot;<span style=3D"color:rgb(0,0,0);font-size:1em"=
>each constructor gets a context which is a subset of that=C2=A0</span><spa=
n style=3D"color:rgb(0,0,0);font-size:1em">given in the @data@=C2=A0</span>=
decl<span style=3D"color:rgb(0,0,0);font-size:1em">, containing all the con=
straints on the free=C2=A0</span><span style=3D"font-size:1em;color:rgb(0,0=
,0)">type variables of the constructor signature, and no others.</span>&quo=
t;</div><div><br></div><div>So we get (example from the 1998 Language Repor=
t)</div><div><br></div><div>=C2=A0 =C2=A0=C2=A0data Eq a =3D&gt; Set a =3D =
NilSet | ConsSet a (Set a)</div><div><br></div><div>=C2=A0 =C2=A0 =3D=3D=3D=
&gt; NilSet :: forall a. Set a</div><div>=C2=A0 =C2=A0 =3D=3D=3D&gt; ConsSe=
t :: forall a. Eq a =3D&gt; a -&gt; Set a</div><div><br></div><div>Well, in=
 the type signature for NilSet, `a` _is_ free, why can&#39;t it get the con=
straint? It&#39;s easy enough to give a signature with constraint for some =
appearance of `NilSet` -- except in the one place I desperately=C2=A0want o=
ne, that is in patterns. I can define</div><div><br></div><div>=C2=A0 =C2=
=A0 nilSet =3D NilSet :: Eq a =3D&gt; Set a</div><div><br></div><div>and us=
e that on rhs of function definitions, etc. The compiler doesn&#39;t seem t=
o come crashing down around my ears. Whereas without the `Eq a`, you can wr=
ite `NilSet :: Set (Int -&gt; Int)` without complaint to produce an unusabl=
e value -- something that will cause complaints every other place you try t=
o consume it or Cons to it. Compare</div><div><br></div><div>=C2=A0 =C2=A0 =
emptyS1 NilSet =3D True=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0-- inferred=
 :: Set a -&gt; Bool</div><div>=C2=A0 =C2=A0 emptyS1 _=C2=A0 =C2=A0 =C2=A0 =
=3D False</div><div><br></div><div>=C2=A0 =C2=A0 emptyS2 (ConsSet _ _) =3D =
False=C2=A0 -- inferred :: Eq a =3D&gt; Set a -&gt; Bool</div><div>=C2=A0 =
=C2=A0 emptyS2 _=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0=3D True</d=
iv><div><br></div><div>Those two definitions are morally equivalent, but ge=
t different types. Note that prior to the 1999 &#39;clarification&#39; GHC =
would have given them both the same signature without the `Eq a`. The brain=
s trust in 1999 was firmly of the mind the constraint should be exposed eve=
rywhere. If they&#39;d been asked about that type for NilSet and how it did=
n&#39;t expose the constraint, I wonder what they&#39;d say?</div><div><br>=
</div><div>Anyhoo, this note is to say it seems easy enough to modify Hugs=
=C2=A0 to give the full set of constraints for every data constructor (and =
consequently get those exposed, so the two definitions form `emptyS` above =
get the same type, with the `Eq a`).</div><div><br></div><div>Would the con=
cern in the 1991 memo still apply in 1999, or 2006 when Hugs development ce=
ased? &quot;<span style=3D"color:rgb(0,0,0);font-size:1em">I was persuaded =
... by John&#39;s comments, and=C2=A0</span><span style=3D"color:rgb(0,0,0)=
;font-size:1em">by the fact that many more cases of ambiguity are likely to=
 arise=C2=A0</span><span style=3D"font-size:1em;color:rgb(0,0,0)">otherwise=
.</span>&quot; John Hughes(?) Anyway I can see no comments on the forum. Wo=
uld the ambiguities be any worse than those for Numeric Literals being `Num=
 a =3D&gt; a`? Or does the defaulting mechanism rescue those?</div><div><br=
></div><div>AntC</div></div>

--000000000000f86ab805b19760a8--

--===============0736583950052802949==
Content-Type: text/plain; charset="utf-8"
MIME-Version: 1.0
Content-Transfer-Encoding: base64
Content-Disposition: inline

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy
cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs
Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo=

--===============0736583950052802949==--