Why does this usage of quantified constraints fail to compile:

Question

Consider the following:

{-# LANGUAGE QuantifiedConstraints #-}

data SomeMaybe c t where
  SomeNothing :: SomeMaybe c t
  SomeJust :: c t => t -> SomeMaybe c t

instance (forall b. c b => Semigroup b) => Semigroup (SomeMaybe c u) where
  x <> y = case x of
    SomeNothing -> y
    SomeJust x' -> case y of
      SomeNothing -> x
      SomeJust y' -> SomeJust (x' <> y')

I get the following error:

src/Filename.hs: error:
    • Could not deduce: c (SomeMaybe c u)
        arising from a use of ‘GHC.Base.$dmsconcat’
      from the context: forall b. c b => Semigroup b
        bound by the instance declaration
        at src/Filename.hs
    • In the expression: GHC.Base.$dmsconcat @(SomeMaybe c u)
      In an equation for ‘GHC.Base.sconcat’:
          GHC.Base.sconcat = GHC.Base.$dmsconcat @(SomeMaybe c u)
      In the instance declaration for ‘Semigroup (SomeMaybe c u)’
    • Relevant bindings include
        sconcat :: GHC.Base.NonEmpty (SomeMaybe c u) -> SomeMaybe c u
          (bound at src/Filename.hs)

I believe the issue is the default implementation of sconcat and stimes which fail to typecheck.

However I don't quite understand why this is the case.

Background note:

For a brief background on why I'm trying to make such a type like SomeMaybe, I'm making my datatypes "barbies" so then for example, I can use bpure like so:

instance ApplicativeB f => Semigroup (f MyType) where
  (<>) = bzipWith (<>)

instance ApplicativeB f => Monoid (f MyType) where
  mempty = bpure mempty

But this only works if MyType a is a monoid for ALL a.

Edit: Workaround

Changing the Semigroup definition to the following:

semigroupOp :: forall c t. (forall b. c b => Semigroup b) => SomeMaybe c t -> SomeMaybe c t -> SomeMaybe c t
semigroupOp x y = case x of
  SomeNothing -> y
  SomeJust x' -> case y of
    SomeNothing -> x
    SomeJust y' -> SomeJust (x' <> y')

instance forall c t. (forall b. c b => Semigroup b) => Semigroup (SomeMaybe c t) where
  (<>) :: (forall b. c b => Semigroup b) => SomeMaybe c t -> SomeMaybe c t -> SomeMaybe c t
  (<>) = semigroupOp
  sconcat :: NonEmpty (SomeMaybe c t) -> (SomeMaybe c t)
  sconcat (a :| as) = go a as where
    go :: SomeMaybe c t -> [SomeMaybe c t] -> SomeMaybe c t
    go x = \case
      [] -> x
      (c : cs) -> semigroupOp x (go c cs)
  stimes n = \case
    SomeNothing -> SomeNothing
    SomeJust x -> SomeJust (stimes n x)

which gets this to compile, although it's not clear why I need to do this? In particular, why I can't just call <> instead of semigroupOp in sconcat?

Answer 1

Removed from the question cause it's an answer:

Answering my own question, changing the Semigroup definition to the following:

semigroupOp :: forall c t. (forall b. c b => Semigroup b) => SomeMaybe c t -> SomeMaybe c t -> SomeMaybe c t
semigroupOp x y = case x of
  SomeNothing -> y
  SomeJust x' -> case y of
    SomeNothing -> x
    SomeJust y' -> SomeJust (x' <> y')

instance forall c t. (forall b. c b => Semigroup b) => Semigroup (SomeMaybe c t) where
  (<>) :: (forall b. c b => Semigroup b) => SomeMaybe c t -> SomeMaybe c t -> SomeMaybe c t
  (<>) = semigroupOp
  sconcat :: NonEmpty (SomeMaybe c t) -> (SomeMaybe c t)
  sconcat (a :| as) = go a as where
    go :: SomeMaybe c t -> [SomeMaybe c t] -> SomeMaybe c t
    go x = \case
      [] -> x
      (c : cs) -> semigroupOp x (go c cs)
  stimes n = \case
    SomeNothing -> SomeNothing
    SomeJust x -> SomeJust (stimes n x)

solves the issue.