Why is using QuantifiedConstraints to specify a subclass of a typeclass also demanding an instance of the subclass?

Question

I'm playing around with a multikinded tagless encoding of Free

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
module Free where
import GHC.Types

type (a :: k) ~> (b :: k) = Morphism k a b

newtype Natural (f :: j -> k) (g :: j -> k) = 
  Natural { getNatural :: forall (x :: j). f x ~> g x }

type family Morphism k :: k -> k -> Type where
  Morphism Type = (->)
  Morphism (j -> k) = Natural

class DataKind k where
  data Free :: (k -> Constraint) -> k -> k
  interpret :: forall (cls :: k -> Constraint) (u :: k) (v :: k). 
               cls v => (u ~> v) -> (Free cls u ~> v)
  call :: forall (cls :: k -> Constraint) (u :: k). 
          u ~> Free cls u

instance DataKind Type where
  newtype Free cls u = Free0
    { runFree0 :: forall v. cls v => (u ~> v) -> v }
  interpret f = \(Free0 g) -> g f
  call = \u -> Free0 $ \f -> f u

I can write Semigroup instances for Free Semigroup and Free Monoid without a problem:

instance Semigroup (Free Semigroup u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

instance Semigroup (Free Monoid u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

These instances are the same, and will be for any other subclass of Semigroup.

I want to use QuantifiedConstraints so I can just write one instance for all subclasses of Semigroup:

instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

But the compiler (GHC-8.6.3) complains that it's unable to deduce cls (Free cls u):

Free.hs:57:10: error:
    • Could not deduce: cls (Free cls u)
        arising from a use of ‘GHC.Base.$dmsconcat’
      from the context: forall v. cls v => Semigroup v
        bound by the instance declaration at Free.hs:57:10-67
    • In the expression: GHC.Base.$dmsconcat @(Free cls u)
      In an equation for ‘GHC.Base.sconcat’:
          GHC.Base.sconcat = GHC.Base.$dmsconcat @(Free cls u)
      In the instance declaration for ‘Semigroup (Free cls u)’
    • Relevant bindings include
        sconcat :: GHC.Base.NonEmpty (Free cls u) -> Free cls u
          (bound at Free.hs:57:10)
   |
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Free.hs:57:10: error:
    • Could not deduce: cls (Free cls u)
        arising from a use of ‘GHC.Base.$dmstimes’
      from the context: forall v. cls v => Semigroup v
        bound by the instance declaration at Free.hs:57:10-67
      or from: Integral b
        bound by the type signature for:
                   GHC.Base.stimes :: forall b.
                                      Integral b =>
                                      b -> Free cls u -> Free cls u
        at Free.hs:57:10-67
    • In the expression: GHC.Base.$dmstimes @(Free cls u)
      In an equation for ‘GHC.Base.stimes’:
          GHC.Base.stimes = GHC.Base.$dmstimes @(Free cls u)
      In the instance declaration for ‘Semigroup (Free cls u)’
    • Relevant bindings include
        stimes :: b -> Free cls u -> Free cls u (bound at Free.hs:57:10)
   |
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

When I add this as context for the instance, it compiles fine:

instance (cls (Free cls u), forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

The added context is a little verbose, but since the whole point of Free is that cls (Free cls u) is always true, not onerous.

What I don't understand is why GHC needs to be able to conclude cls (Free cls u) for the subclass of Semigroup for the Semigroup instance to compile. I tried replacing the definition of (<>) with undefined and got the same error, so I think the issue is not in the implementation itself but in the declaration of the instance; probably due to some aspect of QuantifiedConstraints I don't understand.

Biblio

Answer 1

The error messages state these errors come from the default definitions of sconcat and stimes. Quantified contexts act like instances: within your instance Semigroup (Free cls v), it's as if there is an instance cls v => Semigroup v in scope. instances are chosen by matching. sconcat and stimes want Semigroup (Free cls v), so they match that want against the context instance forall z. cls z => Semigroup z, succeed with z ~ Free cls v, and get a further wanted of cls (Free cls v). This happens even though we also have a recursive instance _etc => Semigroup (Free cls v) around. Remember, we assume that typeclass instances are coherent; there should be no difference whether the quantified context is used or the currently defined instance is used, so GHC just picks whichever instance it feels like using.

However, this is not a good situation. The quantified context overlaps with our instance (actually, it overlaps with every Semigroup instance), which is alarming. If you try something like (<>) = const (Free0 _etc) ([1, 2] <> [3, 4]), you get a similar error, because the quantified context overshadows the real instance Semigroup [a] in the library. I think including some ideas from issue 14877 can make this less uncomfortable:

class (a => b) => Implies a b
instance (a => b) => Implies a b
instance (forall v. cls v `Implies` Semigroup v) => Semigroup (Free cls u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

Using Implies here means that the quantified context no longer matches the want for Semigroup (Free cls v) which is instead discharged by recursion. However, the requirement behind the constraint doesn't change. Essentially, we keep the requirement fragment of the quantified constraint, for the user, that Semigroup v should be implied by cls v, while slapping a safety on the discharge fragment, for the implementation, so it doesn't muck up our constraint resolution. The Implies constraint still can and has to be used to prove the Semigroup v constraint in (<>), but it's considered as a last resort after the explicit Semigroup instances are exhausted.

Wastage

Would it help any if the QuantifiedConstraints syntax distinguished between superclass and instance constraints? I'm rather sad that the committee rejected my suggestion that implication constraints (ill behaved) get a separate extension from quantified constraints (well behaved). I really think the former still need significantly more R & D to get right. – Jumbala

You mean you want arrows class S => C and instance R => H such that, in f :: (instance R => H) => T, you get instance R => H in scope (exactly like the current extension), but, for g :: (class S => C) => T, you get class S => C (adding S to whatever superclasses C already had)? I don't think that helps: instance constraints are constraints. Even without quantified constraints, we need to derive wanteds from the superclasses of instance constraints. Adding quantification is enough to emulate class constraints. Separating class constraints would not contain the wonkiness. – Wastage

I'm not quite understanding what you're saying, which of course doesn't mean you're wrong. In the latter case, it would probably look more like (forall a. class S a => c a) => T c. But as you suggest, that may not help the problem any. Do you see what I mean about quantification behaving better than implication? – Jumbala

@Jumbala Oh, you mean you want forall vars. Ctx vars to be kosher but Req => Deriv to be gated behind another extension? I don't think the latter behaves significantly worse than the former. Both let you get overlapping instances, which is the real source of the weirdness, but that the latter just causes errors sometimes instead of silently accepting. I just wish it were better documented. – Wastage

The usual problem with implication constraints is that the local/global instance chosen will affect the way resolution proceeds, since you'll get different wanteds; resolution can fail because the instance constraints of the chosen instance can't be satisfied even though there's another instance in scope whose constraints can be. With plain quantified constraints, I don't believe that happens, but maybe I'm wrong. – Jumbala

@Jumbala Yes, that all makes sense. I can't say I have any opinions on the matter. I do wonder: is there any trick, Implies or a generalization thereof, that can always resolve such conflicts? As long as there is one I can't complain. – Wastage