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?

Not a direct answer to the question, but `(forall b. c b => Semigroup b)` is stronger than it needs to be. The original code compiles if you switch this to `(c u => Semigroup u)`. — fluffyyboii, Aug 16 '23 at 15:51
Does this answer your question? [Why is using QuantifiedConstraints to specify a subclass of a typeclass also demanding an instance of the subclass?](https://stackoverflow.com/questions/56573436/why-is-using-quantifiedconstraints-to-specify-a-subclass-of-a-typeclass-also-dem) — HTNW, Aug 16 '23 at 17:06

cafce25 · Answer 1 · 2023-08-16T16:28:05.927

-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.

edited Aug 16 '23 at 16:28

answered Aug 16 '23 at 04:32

cafce25

15,907
4
25
31

This shouldn't be in the answer section because it ends in a question. Answers don't end in question marks. – Clinton Aug 16 '23 at 05:43
1

This shouldn't be in the question because it starts in "Answering my own Question" period. A follow up question honestly does belong in a new Post all together. – cafce25 Aug 16 '23 at 06:28
3

To me this reads like added details to the question, not an answer. – Cubic Aug 16 '23 at 15:05

Why does this usage of quantified constraints fail to compile:

1 Answers1