<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <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 class="moz-txt-link-freetext" href="https://gist.github.com/phadej/266d68cf5cc1229c3548b7965f4335f8">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 class="moz-txt-link-freetext" href="https://hackage.haskell.org/package/free-5/changelog">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 class="moz-txt-link-freetext" href="https://www.haskell.org/ghc/">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 class="moz-cite-prefix">On 14.3.2020 16.10, chessai . wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAD34_kJw72dJwSzvfNbQ95ie-p25Mu72PC52TYUHnBfZMpSOCw@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <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"
            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" target="_blank"
                    rel="noreferrer" 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 class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Libraries mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Libraries@haskell.org">Libraries@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
    </blockquote>
  </body>
</html>