<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Yes there is that. If you (or anyone else is) curious,
<a class="moz-txt-link-freetext" href="https://gitlab.haskell.org/ghc/ghc/issues/17295">https://gitlab.haskell.org/ghc/ghc/issues/17295</a> discusses this a
bit. In the last comment I wonder whether `Note [Instance and
Given overlap]` is really about quantified vs non-quantified,
rather than local and global, and just conflates the two because
it dates back to the introduction of OutsideIn when there were no
local givens with implication.<br>
</p>
<div class="moz-cite-prefix">On 4/20/20 9:47 PM, David Feuer wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAMgWh9tkekaNb2pMVX6hYLBcxe67Vi=9Eh9o06kkVCLGfZBQtA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="auto">That's definitely part of the problem, but the way
QuantifiedConstraints leads to local overlap is also generally
troubling.</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, Apr 20, 2020, 9:44 PM
John Ericson <a class="moz-txt-link-rfc2396E" href="mailto:john.ericson@obsidian.systems"><john.ericson@obsidian.systems></a> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>
<p>I think that the problem there is not
QuantifiedConstraints, but Coercible (and likewise ~ and
~~) not working well with local constraints of any sort.
That's a problem I very much want fixed, but still
separate. It should be possible to turn a `Foo => Bar`
into a `Dict Foo -> Dict Bar` can get oneself unstuck.</p>
<p>John<br>
</p>
<div>On 4/18/20 2:51 PM, David Feuer wrote:<br>
</div>
<blockquote type="cite">
<div dir="auto">It's been some months, but the last time I
messed with quantified constraints I found they didn't
work well at all with Coercible.</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sat, Mar 14, 2020,
11:44 AM Oleg Grenrus <<a
href="mailto:oleg.grenrus@iki.fi" target="_blank"
rel="noreferrer" moz-do-not-send="true">oleg.grenrus@iki.fi</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div>
<p>QuantifiedConstraints are not buggy, but they are
not _complete_<br>
(I do mean that as "buggy" = not sound, properly
expressive = complete).<br>
<br>
There are at least three issues:<br>
<br>
1. Instance definition need UndecidableInstances
(in my opinion this is big deal)<br>
2. Instances are not elegant (easy to write, but
not elegant).<br>
3. QuantifiedConstraints resists to be abstracted
over<br>
<br>
See <a
href="https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8</a>
for<br>
the standalone code file.<br>
<br>
For the reasons below I wouldn't recommend using
QuantifiedConstraints.<br>
I very like them, but I'm not convinced the
feature is ready for "prime time".<br>
To put into perspective, I think code classes of
`singletons` are more ready to<br>
be included in `base` than changing instances of
Data.Functor.Sum and .Product.<br>
I do use singletons in my code more than
QuantifiedConstraints. :)<br>
<br>
I'm very worried how this change will affect
libraries like `free` and<br>
`recursion-schemes` and what builds on top of
them.<br>
This is not only change to `base`, it strongly
guides how downstream<br>
libraries should be written (or changed) as well.<br>
<br>
On the other hand, I don't feel strongly about<br>
<br>
instance (Eq (f a), Eq (g a)) => Eq
(Product f g a)<br>
<br>
Yet, in the light of `free` it is "a step
backwards".<br>
See <a
href="https://hackage.haskell.org/package/free-5/changelog"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">https://hackage.haskell.org/package/free-5/changelog</a><br>
<br>
---<br>
<br>
Simple example with `newtype Fix f = Fix (f (Fix
f))`<br>
<br>
class Eq1 f where<br>
liftEq :: (a -> b -> Bool) -> f a
-> f b -> Bool<br>
<br>
class Eq1 f => Ord1 f where<br>
liftCompare :: (a -> b -> Ordering)
-> f a -> f b -> Ordering<br>
<br>
instance Eq1 f => Eq (Fix f) where<br>
(==) = eq where eq (Fix x) (Fix y) =
liftEq eq x y<br>
<br>
instance Ord1 f => Ord (Fix f) where<br>
compare = cmp where cmp (Fix x) (Fix y) =
liftCompare cmp x y<br>
<br>
works. It's boilerplate, but it's already written.<br>
<br>
However, if we want to use QuantifiedConstraints,<br>
then we<br>
<br>
1. need UndecidableInstances<br>
2. and then the code turns out to be less elegant:<br>
<br>
instance (forall x. Eq x => Eq (f x)) => Eq
(Fix f) where<br>
(==) = eq where eq (Fix x) (Fix y) = x == y<br>
<br>
instance (forall x. Ord x => Ord (f x)) =>
Ord (Fix f) where<br>
compare = cmp where cmp (Fix x) (Fix y) =
compare x y<br>
<br>
fails to compile with<br>
<br>
GHCi, version 8.8.3: <a
href="https://www.haskell.org/ghc/"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">https://www.haskell.org/ghc/</a>
:? for help<br>
[1 of 1] Compiling Main ( Ord1.hs,
interpreted )<br>
<br>
Ord1.hs:28:10: error:<br>
• Could not deduce (Ord x)<br>
arising from the superclasses of an
instance declaration<br>
<br>
we need to write Ord instance differently<br>
<br>
instance (forall x. Ord x => Ord (f x),
forall x. Eq x => Eq (f x)) => Ord (Fix f)
where<br>
compare = cmp where cmp (Fix x) (Fix y) =
compare x y<br>
<br>
<br>
This _cannot_ be made to work:<br>
<br>
forall x. Ord x => Ord (f x)<br>
<br>
doesn't entail<br>
<br>
forall x. Eq x => Eq (f x)<br>
<br>
If you try to write defaultLiftEq using
liftCompare<br>
<br>
defaultLiftEq :: Ord1 f => (a -> b ->
Bool) -> f a -> f b -> Bool<br>
defaultLiftEq eq x y = EQ == liftCompare
_problem_ x y<br>
<br>
then you will se a problem.<br>
<br>
---<br>
<br>
Third issue is that We cannot abstract over
QuantifiedConstraints.<br>
<br>
Take an example `Dict`. We can use `Dict` for
various things.<br>
<br>
data Dict :: (k -> Constraint) -> k
-> * where<br>
Dict :: c a => Dict c a<br>
<br>
It nicely uses PolyKinds extension so we can
write:<br>
<br>
eqInt :: Dict Eq Int<br>
eqInt = Dict<br>
<br>
eq1List :: Dict Eq1 []<br>
eq1List = Dict<br>
<br>
And we can use Dict to *manually* thread
information<br>
<br>
entail :: Dict Ord1 f -> Dict Eq1 f<br>
entail Dict = Dict<br>
<br>
The selling pitch of QuantifiedConstraints, that
we could get this for free.<br>
Above Ord (Fix) example however makes me
suspicious. Let's try:<br>
<br>
eqQList :: Dict (forall x. Eq x => Eq (f
x)) []<br>
eqQList = undefined<br>
<br>
But it doesn't work!<br>
<br>
Ord1.hs:53:28: error:<br>
• Expected kind ‘(* -> *) ->
Constraint’,<br>
but ‘Eq (f x)’ has kind ‘*’<br>
• In the first argument of ‘Dict’, namely<br>
‘(forall x. Eq x => Eq (f x))’<br>
In the type signature:<br>
eqQList :: Dict (forall x. Eq x =>
Eq (f x)) []<br>
|<br>
53 | eqQList :: Dict (forall x. Eq x => Eq
(f x)) []<br>
|<br>
<br>
Ord1.hs:53:36: error:<br>
• Expected a type, but ‘Eq (f x)’ has kind
‘Constraint’<br>
• In the first argument of ‘Dict’, namely<br>
‘(forall x. Eq x => Eq (f x))’<br>
In the type signature:<br>
eqQList :: Dict (forall x. Eq x =>
Eq (f x)) []<br>
|<br>
53 | eqQList :: Dict (forall x. Eq x => Eq
(f x)) []<br>
|
^^^^^^^^<br>
<br>
Then we remember that we have seen that,<br>
we **cannot define** type synonyms for quantified
constraints<br>
<br>
type Eq1' f = forall x. Eq x => Eq (f x)<br>
<br>
errors with<br>
<br>
Ord1.hs:56:33: error:<br>
• Expected a type, but ‘Eq (f x)’ has kind
‘Constraint’<br>
<br>
Luckily GHC-8.10.1 (which is not released at the
moment of writing)<br>
will give us ability to say<br>
<br>
type Eq1' :: (* -> *) -> Constraint<br>
type Eq1' f = forall x. Eq x => Eq (f x)<br>
<br>
This is promising! Let's try to fix eqQList<br>
<br>
eqQList2 :: Dict Eq1' []<br>
eqQList2 = undefined<br>
<br>
But that doesn't work. Type-aliases have to be
fully applied!<br>
<br>
How in Haskell we fix issues when type-aliases (of
classes) need to be partially<br>
evaluated? We defined<br>
<br>
class ... => Example a b c<br>
instance ... => Example a b c<br>
<br>
Third try<br>
<br>
eqQList3 :: Dict Eq1'' f<br>
eqQList3 = Dict<br>
<br>
The type signature is accepted, but the
implementation is not<br>
<br>
Ord1.hs:67:12: error:<br>
• Could not deduce (Eq (f x)) arising from
a use of ‘Dict’<br>
<br>
At this point I'm clueless.<br>
<br>
---<br>
<br>
Best regards,<br>
Oleg<br>
<br>
P.S. If we would like to take
QuantifiedConstraints somewhere into use, then IMO
we should start with MonadTrans class. IIRC it's
well motivated in the paper. But
UndecidableInstances is very unfortunate.<br>
</p>
<div>On 14.3.2020 16.10, chessai . wrote:<br>
</div>
<blockquote type="cite">
<div dir="auto">I can second Richard's estimation
of QuantifiedConstraints, I have used them a lot
in my own code since they were in HEAD. I
consider it a sufficiently stable feature to
include in base or any library. </div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sat, Mar
14, 2020, 4:16 AM Richard Eisenberg <<a
href="mailto:rae@richarde.dev"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">rae@richarde.dev</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0
0 0 .8ex;border-left:1px #ccc
solid;padding-left:1ex">
<div
style="word-wrap:break-word;line-break:after-white-space"><br>
<div><br>
<blockquote type="cite">
<div>On Mar 14, 2020, at 4:14 AM, Eric
Mertens <<a
href="mailto:emertens@gmail.com"
rel="noreferrer noreferrer
noreferrer" target="_blank"
moz-do-not-send="true">emertens@gmail.com</a>>
wrote:</div>
<br>
<div><span
style="font-family:Helvetica;font-size:12px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;text-decoration:none;float:none;display:inline!important">The
last thing I'd heard about
quantified constraints was that they
were buggy and I've been avoiding
relying on them. (I should probably
review that assumptions at some
point.)</span></div>
</blockquote>
</div>
<br>
<div>Without expressing an opinion about
chessai's proposal (which I have not
really thought about): quantified
constraints are in good shape and ready
for prime time. They have limitations
(e.g. you can't mention a type family to
the right of the =>), but when they are
valid, they work well. I'll never swear
that a feature is bug-free, but I think
it's reasonable to consider using
quantified constraints in `base`.</div>
<div><br>
</div>
<div>Richard</div>
</div>
</blockquote>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Libraries mailing list
<a href="mailto:Libraries@haskell.org" rel="noreferrer noreferrer" target="_blank" moz-do-not-send="true">Libraries@haskell.org</a>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank" moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
</blockquote>
</div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer
noreferrer" target="_blank" moz-do-not-send="true">Libraries@haskell.org</a><br>
<a
href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries"
rel="noreferrer noreferrer noreferrer"
target="_blank" moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Libraries mailing list
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer" moz-do-not-send="true">Libraries@haskell.org</a>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank" rel="noreferrer" moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
</blockquote>
</div>
</blockquote>
</div>
</blockquote>
</body>
</html>