DerivingVia QuantifiedConstraints

Learn
#1

I am trying to follow the helpful explanation from Ryan Scot on how to use Quantified Constraints to coerce types with higher kinded type variables to derive instances.

:set -XStandaloneDeriving -XDerivingVia -XQuantifiedConstraints
import Data.Coerce
import Data.Functor.Compose
class Alternative m where (<|>) :: m a -> m a -> m a
newtype WriterT w m a = WriterT (m (a, w))
newtype Flip a c b = Flip (a b c)
instance Alternative f => Alternative (Compose f g) where (<|>) = coerce ((<|>) :: f (g a) -> f (g a) -> f (g a)) :: forall a . Compose f g a -> Compose f g a -> Compose f g a
instance Alternative Maybe where x@(Just _) <|> _ = x; _ <|> x = x
deriving via Compose m (Flip (,) w) instance (Alternative m, forall a b. Coercible (m a) (m b)) => Alternative (WriterT w m)
WriterT (Just ('a', ())) <|> WriterT Nothing :: WriterT () Maybe Char

but get the following

<interactive>:11:26: error:
     Couldn't match representation of type ‘a’ with that of ‘b’
        arising from a use of ‘<|>’
      ‘a’ is a rigid type variable bound by
        a quantified context
        at <interactive>:11:1-69
      ‘b’ is a rigid type variable bound by
        a quantified context
        at <interactive>:11:1-69
     In the expression:
          WriterT (Just ('a', ())) <|> WriterT Nothing ::
            WriterT () Maybe Char
      In an equation for ‘it’:
          it
            = WriterT (Just ('a', ())) <|> WriterT Nothing ::
                WriterT () Maybe Char

Is there a way to use this derive this special version of Alternative for WriterT?

#2

You wrote:

deriving via Compose m (Flip (,) w) instance
  ( Alternative m
  , forall a b. Coercible (m a) (m b)
  ) =>
    Alternative (WriterT w m)

Did you instead mean

deriving via Compose m (Flip (,) w) instance
  ( Alternative m
  , forall a b. Coercible a b => Coercible (m a) (m b)
  ) =>
    Alternative (WriterT w m)

?

Otherwise, when using this derived instance you’re asking GHC to prove that Maybe a is coercible to Maybe b for any a and b, to which it is rightly objecting.

2 Likes
#3

Thank you for the correction.

It works with ```WriterT (Just ((), ())) <|> Writer Nothing`.

However, when I start using it in my tests I get

     Couldn't match type ‘a’ with ‘b’
        arising from a use of ‘runAllTests’
      ‘a’ is a rigid type variable bound by
        a quantified context
        at tests/Biparse/Core/ClassesSpec.hs:1:1
      ‘b’ is a rigid type variable bound by
        a quantified context
        at tests/Biparse/Core/ClassesSpec.hs:1:1
     In the expression:
        runAllTests @() @() @() @() @() @() @TestSuite testSuite
      In an equation for ‘spec’:
          spec = runAllTests @() @() @() @() @() @() @TestSuite testSuite
   |
12 | spec = runAllTests @() @() @() @() @() @() @TestSuite testSuite

which does not give you or me much to figure out the problem.

#4

Indeed not. Looking at the source code would help.

1 Like
#5

build biparsing-core-tests package on derivingvia-quantifiedconstraints branch

Alternative class and instances defined in biparsing-core/src/Biparse/Core/Alternative.hs

#6

Have you considered using Alt instead?

If the change to the Alternative instance is the only thing that took this test from compiling to not, then I can only conclude that somewhere in the bowels of runAllTests you have requested an Alternative (LazyWriterT w m) instance for which it is not (known to be) the case that Coercible a b implies Coercible (m a) (m b) for all a and b.

To dump this requirement, maybe you would prefer:

newtype ComposeFlip f g a b = ComposeFlip (f (g b a))

instance Alternative f => Alternative (ComposeFlip f g a) where
  (<|>) :: forall b. ComposeFlip f g a b -> ComposeFlip f g a b -> ComposeFlip f g a b
  (<|>) = coerce ((<|>) @f @(g b a))
  -- I know you're on an earlier GHC, but with -XTypeAbstractions this could instead be
  -- (<|>) @b = coerce ((<|>) @f @(g b a))
  -- without the redundant signature.

deriving via ComposeFlip m (,) w instance Alternative m => Alternative (WriterT w m)
#7

I am transitioning away from Alt because it is not easily derivable. derive Alt · Issue #135 · ekmett/semigroupoids · GitHub

#8

I think I have found the problem. These quantified instances work fine when they are not composed with each other.

If I use WriterT w (StateT s m), it fails with Couldn't match type ‘a’ with ‘b’. This is probably because both WriterT and StateT modify the result.

#9

Have you tried using standalone deriving?

newtype WE a b = WE (Either a b) deriving Functor
deriving instance Alt (WE a)