FunDeps: divergent improvement from overlapping instances

--===============2898842499378964707==
Content-Type: multipart/alternative; boundary="0000000000007dbbcd05e5a3f663"

--0000000000007dbbcd05e5a3f663
Content-Type: text/plain; charset="UTF-8"

The HList project (~2004) had to abandon Hugs because (for example) they
couldn't express a type-level type equality test.

Hugs rejects any attempt 'Instances are not consistent with Functional
Dependencies'. Here's the equivalent that works in GHC.

>    class TypeEq a b e  | a b -> e
>    instance                                      TypeEq a a TTrue
>    instance {#- OVERLAPPABLE -#} (e ~ TFalse) => TypeEq a b e

Hugs rejects the equivalent of these instances because it can unify the
instance heads' determining positions (as TypeEq a a e0) but the
improvement diverges. Hugs always treats a wildcard e0 as apart from any
specific type or from any other wildcard; whereas GHC treats them as
unifiable, so accepts the instances. The instances (whole heads) are
overlappable, so GHC's overlapping instances mechanism will improve e ~
TFalse only on condition it can't unify types a, b at some usage site.

SPJ points out
https://gitlab.haskell.org/ghc/ghc/-/wikis/Functional-dependencies-in-GHC/Key-examples/FunDep-improvement-vs-instance-selection#qs-for-spj
that using an instance head to improve under a FunDep is a separate step
and proceeds first vs selecting an instance. So this form for the second
instance won't work in GHC:

>    instance                            TypeEq a b TFalse

(Also the instance heads are not overlapping.) In case of TypeEq a a e0,
instance improvement will find both instances match and improve e0 ~ TTrue,
e0 ~ TFalse, then reject as inconsistent, same as Hugs.

But notice this FunDep is 'Full' -- that is, mentions all of the classes,
parameters. ('Full' FunDep is introduced in the 2008 'via CHRs' paper.)

If improvement can use a Full FunDep matching to an instance head, it has
in effect selected that instance. This is really using the instance as a
_candidate_ for improvement -- it might be the Dependent types are already
improved as far as possible before looking at this instance. (That is, if
we already have [W] TypeEq Int Int TTrue, looking to the instance heads
won't improve further; but Hugs is not smart enough to shortcut that TTrue
can't be improved.)

Hugs' type routines at this step of compilation are very much focussed on
improving types, not selecting instances. And in case of a class with
multiple FunDeps, the routines should 'fire' all possible FunDeps for each
instance.

However it's only a small mod in routine instImprove to say: upon matching
to a Full FunDep for an instance, stop looking at other instances for
improvement. A precondition is that it scans instances in
most-specific-first sequence -- which Hugs is already doing. So I can write
these instances

> class     TypeEq a b e  | a b -> e
> instance TypeEq a a TTrue
> instance TypeEq a b TFalse

Without needing to clutter the instances by deferring improvement to
constraints. (This also makes type inference error messages less cluttered.)

I'm now working on the instance sequencing routines, to ignore those
divergent Dependent positions when deciding overlap ordering.

AntC

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

<div dir=3D"ltr">The HList project (~2004) had to abandon Hugs because (for=
 example) they couldn&#39;t express a type-level type equality test.<div><b=
r></div><div>Hugs rejects any attempt &#39;Instances are not consistent wit=
h Functional Dependencies&#39;. Here&#39;s the equivalent that works in GHC=
.</div><div><br></div><div>&gt;=C2=A0 =C2=A0 class TypeEq a b e=C2=A0 | a b=
 -&gt; e</div><div>&gt;=C2=A0 =C2=A0 instance=C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 TypeEq a a TTrue</div><div>&gt;=C2=A0 =C2=
=A0 instance {#- OVERLAPPABLE -#} (e ~ TFalse) =3D&gt; TypeEq a b e</div><d=
iv><br></div><div>Hugs rejects the equivalent of these instances because it=
 can unify the instance heads&#39; determining positions (as TypeEq a a e0)=
 but the improvement diverges. Hugs always treats a wildcard e0 as apart fr=
om any specific type or from any other wildcard; whereas GHC treats them as=
 unifiable, so accepts the instances. The instances (whole heads) are overl=
appable, so GHC&#39;s overlapping instances mechanism will improve e ~ TFal=
se only on condition it can&#39;t unify types a, b at some usage site.</div=
><div><br></div><div>SPJ points out=C2=A0<a href=3D"https://gitlab.haskell.=
org/ghc/ghc/-/wikis/Functional-dependencies-in-GHC/Key-examples/FunDep-impr=
ovement-vs-instance-selection#qs-for-spj">https://gitlab.haskell.org/ghc/gh=
c/-/wikis/Functional-dependencies-in-GHC/Key-examples/FunDep-improvement-vs=
-instance-selection#qs-for-spj</a> that using an instance head to improve u=
nder a FunDep is a separate step and proceeds first vs selecting an instanc=
e. So this form for the second instance won&#39;t work in GHC:</div><div><b=
r></div><div>&gt;=C2=A0 =C2=A0 instance=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 TypeEq a b T=
False</div><div><br></div><div>(Also the instance heads are not overlapping=
.) In case of TypeEq a a e0, instance improvement will find both instances =
match and improve e0 ~ TTrue, e0 ~ TFalse, then reject as inconsistent, sam=
e as Hugs.</div><div><br></div><div>But notice this FunDep is &#39;Full&#39=
; -- that is, mentions all of the classes, parameters. (&#39;Full&#39; FunD=
ep is introduced in the 2008 &#39;via CHRs&#39; paper.)</div><div><br></div=
><div>If improvement can use a Full FunDep matching to an instance head, it=
 has in effect selected that instance. This is really using the instance as=
 a _candidate_ for improvement -- it might be the Dependent types are alrea=
dy improved as far as possible before looking at this instance. (That is, i=
f we already have [W] TypeEq Int Int TTrue, looking to the instance heads w=
on&#39;t improve further; but Hugs is not smart enough to shortcut that TTr=
ue can&#39;t be improved.)</div><div><br></div><div>Hugs&#39; type routines=
 at this step of compilation are very much focussed on improving types, not=
 selecting instances. And in case of a class with multiple FunDeps, the rou=
tines should &#39;fire&#39; all possible FunDeps for each instance.</div><d=
iv><br></div><div>However it&#39;s only a small mod in routine instImprove =
to say: upon matching to a Full FunDep for an instance, stop looking at oth=
er instances for improvement. A precondition is that it scans instances in =
most-specific-first sequence -- which Hugs is already doing. So I can write=
 these instances</div><div><br></div><div>&gt; class=C2=A0 =C2=A0 =C2=A0Typ=
eEq a b e=C2=A0 | a b -&gt; e</div><div>&gt; instance TypeEq a a TTrue</div=
><div>&gt; instance TypeEq a b TFalse</div><div><br></div><div>Without need=
ing to clutter the instances by deferring improvement to constraints. (This=
 also makes type inference error messages less cluttered.)</div><div><br></=
div><div>I&#39;m now working on the instance sequencing routines, to ignore=
 those divergent Dependent positions when deciding overlap ordering.</div><=
div><br></div><div>AntC</div></div>

--0000000000007dbbcd05e5a3f663--

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

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy
cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs
Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo=

--===============2898842499378964707==--