props for Hugs over System FC

--===============2051781216814885461==
Content-Type: multipart/alternative; boundary="0000000000003ae2fd0584e49861"

--0000000000003ae2fd0584e49861
Content-Type: text/plain; charset="UTF-8"

heh heh. I've got to record this for posterity. I've never known an example
before.

Some code that compiles in Hugs and works fine; but GHC (8.6.4) can't
typecheck so rejects.

It's an example in the 2011 'System F with Type Equality Coercions',
section 2.3 discussing FunDeps; and used to justify the extra power of type
inference in Type Families as opposed to FunDeps. Full details discussed
here: https://gitlab.haskell.org/ghc/ghc/issues/16430#note_189393

    class F a b | a -> b

    instance F Int Bool

    class D a where { op :: F a b => a -> b }

    instance D Int where { op _ = True }

True that doesn't compile as given. Hugs says: 'Inferred type is not
general enough'.

GHC says 'Couldn't match expected type `b' with actual type `Bool''/
'`b' is a rigid type variable'. (So essentially the same failure of
typechecking.)

With a little help for the type inference, this compiles in Hugs.

    class F a b | a -> b

    instance F Int Bool

    class D a where { op :: (F a b) => a -> b }

    instance (TypeCast Bool b') => D Int where { op _ = typeCast True }


With `TypeCast` defined as for HList.

That dangling type variable `b'` in the constraint is weird.

But GHC still rejects it; and rejects a version with a `(~)`
constraint instead of the `TypeCast`.


AntC

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

<div dir=3D"ltr"><br><div class=3D"gmail_quote"><div dir=3D"ltr"><div dir=
=3D"ltr"><div dir=3D"ltr"><div dir=3D"ltr">heh heh. I&#39;ve got to record =
this for posterity. I&#39;ve never known an example before.<div><br></div><=
div>Some code that compiles in Hugs and works fine; but GHC (8.6.4) can&#39=
;t typecheck so rejects.</div><div><br></div><div>It&#39;s an example in th=
e 2011 &#39;System F with Type Equality Coercions&#39;, section 2.3 discuss=
ing FunDeps; and used to justify the extra power of type inference in Type =
Families as opposed to FunDeps. Full details discussed here:=C2=A0<a href=
=3D"https://gitlab.haskell.org/ghc/ghc/issues/16430#note_189393" target=3D"=
_blank">https://gitlab.haskell.org/ghc/ghc/issues/16430#note_189393</a></di=
v><div><br></div><div><pre class=3D"m_1803594792555619484gmail-code m_18035=
94792555619484gmail-highlight" lang=3D"plaintext"><span id=3D"m_18035947925=
55619484gmail-LC1" class=3D"m_1803594792555619484gmail-line" lang=3D"plaint=
ext">    class F a b | a -&gt; b</span></pre><pre class=3D"m_18035947925556=
19484gmail-code m_1803594792555619484gmail-highlight" lang=3D"plaintext"><s=
pan id=3D"m_1803594792555619484gmail-LC2" class=3D"m_1803594792555619484gma=
il-line" lang=3D"plaintext">    instance F Int Bool</span></pre><pre class=
=3D"m_1803594792555619484gmail-code m_1803594792555619484gmail-highlight" l=
ang=3D"plaintext"><span id=3D"m_1803594792555619484gmail-LC4" class=3D"m_18=
03594792555619484gmail-line" lang=3D"plaintext">    class D a where { op ::=
 F a b =3D&gt; a -&gt; b }</span></pre><pre class=3D"m_1803594792555619484g=
mail-code m_1803594792555619484gmail-highlight" lang=3D"plaintext"><span id=
=3D"m_1803594792555619484gmail-LC5" class=3D"m_1803594792555619484gmail-lin=
e" lang=3D"plaintext">    instance D Int where { op _ =3D True }</span></pr=
e><pre class=3D"m_1803594792555619484gmail-code m_1803594792555619484gmail-=
highlight" lang=3D"plaintext">True that doesn&#39;t compile as given. Hugs =
says: &#39;Inferred type is not general enough&#39;.=C2=A0</pre><pre class=
=3D"m_1803594792555619484gmail-code m_1803594792555619484gmail-highlight" l=
ang=3D"plaintext"><font face=3D"Arial, Helvetica, sans-serif"><span style=
=3D"white-space:normal">GHC says &#39;</span></font>Couldn&#39;t match expe=
cted type `b&#39; with actual type `Bool&#39;&#39;/ &#39;`b&#39; is a rigid=
 type variable&#39;. (So essentially the same failure of typechecking.)</pr=
e><pre class=3D"m_1803594792555619484gmail-code m_1803594792555619484gmail-=
highlight" lang=3D"plaintext"><pre class=3D"m_1803594792555619484gmail-code=
 m_1803594792555619484gmail-highlight" lang=3D"plaintext"><font face=3D"Ari=
al, Helvetica, sans-serif"><span style=3D"white-space:normal">With a little=
 help for the type inference, this compiles in Hugs.=C2=A0</span></font>   =
 </pre><pre class=3D"m_1803594792555619484gmail-code m_1803594792555619484g=
mail-highlight" lang=3D"plaintext"><pre class=3D"gmail-code gmail-highlight=
" lang=3D"plaintext"><span id=3D"gmail-LC1" class=3D"gmail-line" lang=3D"pl=
aintext">    class F a b | a -&gt; b</span></pre><pre class=3D"gmail-code g=
mail-highlight" lang=3D"plaintext"><span id=3D"gmail-LC2" class=3D"gmail-li=
ne" lang=3D"plaintext">    instance F Int Bool</span>
<span id=3D"gmail-LC4" class=3D"gmail-line" lang=3D"plaintext"><br></span><=
/pre><pre class=3D"gmail-code gmail-highlight" lang=3D"plaintext"><span cla=
ss=3D"gmail-line" lang=3D"plaintext">    class D a where { op :: (F a b) =
=3D&gt; a -&gt; b } </span></pre><pre class=3D"gmail-code gmail-highlight" =
lang=3D"plaintext"><span id=3D"gmail-LC5" class=3D"gmail-line" lang=3D"plai=
ntext">    instance (TypeCast Bool b&#39;) =3D&gt; D Int where { op _ =3D t=
ypeCast True }</span></pre><pre class=3D"gmail-code gmail-highlight" lang=
=3D"plaintext"><span class=3D"gmail-line" lang=3D"plaintext"><br></span></p=
re><pre class=3D"m_1803594792555619484gmail-code m_1803594792555619484gmail=
-highlight" lang=3D"plaintext">With `TypeCast` defined as for HList.</pre><=
/pre><pre class=3D"m_1803594792555619484gmail-code m_1803594792555619484gma=
il-highlight" lang=3D"plaintext">That dangling type variable `b&#39;` in th=
e constraint is weird.</pre><pre class=3D"m_1803594792555619484gmail-code m=
_1803594792555619484gmail-highlight" lang=3D"plaintext">But GHC still rejec=
ts it; and rejects a version with a `(~)` constraint instead of the `TypeCa=
st`.</pre><pre class=3D"m_1803594792555619484gmail-code m_18035947925556194=
84gmail-highlight" lang=3D"plaintext"><br></pre><pre class=3D"m_18035947925=
55619484gmail-code m_1803594792555619484gmail-highlight" lang=3D"plaintext"=
>AntC
</pre></pre><pre class=3D"m_1803594792555619484gmail-code m_180359479255561=
9484gmail-highlight" lang=3D"plaintext"></pre></div></div></div></div></div=
>
</div></div>

--0000000000003ae2fd0584e49861--

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

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy
cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs
Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo=

--===============2051781216814885461==--