Opened 19 months ago

Last modified 16 months ago

#14831 new bug

QuantifiedConstraints: Odd superclass constraint

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This code works

{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #-}

import Data.Semigroup

newtype Free cls a = Free ()

instance (forall xx. cls xx => Semigroup xx) => Semigroup (Free cls a) where
  (<>)    = undefined 
  stimes  = undefined
  sconcat = undefined

-- instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where
--   mempty = undefined 

but uncomment the Monoid instance and we get

$ ghci -ignore-dot-ghci /tmp/I.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/I.hs, interpreted )

/tmp/I.hs:12:10: error:
    • Could not deduce: cls (Free cls a)
        arising from the superclasses of an instance declaration
      from the context: forall xx. cls xx => Semigroup xx
        bound by the instance declaration at /tmp/I.hs:12:10-67
    • In the instance declaration for ‘Monoid (Free cls a)’
   |
12 | instance (forall xx. cls xx => Semigroup xx) => Monoid (Free cls a) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude> 

Is this correct behavior?

Change History (8)

comment:1 Changed 19 months ago by Iceland_jack

Based off recent changes (ticket:14733#comment:9), I think this worked prior

Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:2 Changed 19 months ago by Iceland_jack

Similarly

newtype Free :: (Type -> Constraint) -> (Type -> Type) where
  Free :: () -> Free cls a

instance (forall xx. cls xx => Semigroup xx) => Semigroup (Free cls a) where
  (<>) = undefined 

fails because of the default methods sconcat and stimes

class Semigroup a where
  (<>)    :: a -> a -> a
  sconcat :: NonEmpty a -> a
  stimes  :: Integral b => b -> a -> a
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( I.hs, interpreted )

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

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

comment:3 Changed 19 months ago by simonpj

Looks like a bug -- will investigate.

comment:4 Changed 19 months ago by simonpj

Ah. Maybe not a bug. Consider

instance (forall xx. cls xx => Semigroup xx)
      => Monoid (Free cls a) where
   mempty = undefined

We need the superclass

 [W] Semigroup (Free cls a)

What you were hoping was that GHC would use the instance

instance (forall xx. cls xx => Semigroup xx)
      => Semigroup (Free cls a) where

to reduce the wanted superclass to

 [W] (forall xx. cls xx => Semigroup xx)

which we can readily solve from the context of the Monoid instance.

But ALASf, the Monoid instace claims to have a way to solve (Semigroup xx) for any xx. Currently GHC tries the local, quantified constraints first, so from

 [W] Semigroup (Free cls a)

using the quantified constraint, we get

 [W] cls (Free cls a)

which we have no way to solve.

The quantified constraint does look far too general. I'll declare this not-a-bug for now.

I have not looked at comment:2 yet; let's sort this part out first.

comment:5 Changed 19 months ago by Iceland_jack

Update: With latest changes the original code compiles AND we can build these beautiful instances for our own Semigroup-Monoid-Group hierarchy

instance semi ~=> Semigroup => Semigroup (Free semi a) where
  (<>)    = liftFree2 (<>)
  sconcat = undefined
  stimes  = undefined

instance mon ~=> Monoid => Monoid (Free mon a) where
  mempty  = liftFree0 mempty
  mappend = liftFree2 (<>)
  mconcat = undefined

instance grp ~=> Group => Group (Free grp a) where
  inv = liftFree1 inv

but leaving out or inlining default methods mconcat = foldr mappend mempty fails.


class Monoid a => Group a where
  inv :: a -> a

type cls ~=> cls' = (forall xx. cls xx => cls' xx :: Constraint)

liftFree0 :: (forall xx. cls xx => xx) -> Free cls a
liftFree0 a = Free (pure a)

liftFree1 :: (forall xx. cls xx => xx -> xx) -> (Free cls a -> Free cls a)
liftFree1 f (Free xs) = Free (fmap f xs)

liftFree2 :: (forall xx. cls xx => xx -> xx -> xx) -> (Free cls a -> Free cls a -> Free cls a)
liftFree2 f (Free xs) (Free ys) = Free (liftA2 f xs ys)
Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:6 Changed 19 months ago by RyanGlScott

You didn't post the full code that you're alluding to in comment:5, but my hunch is that you're experiencing the same bug as in https://ghc.haskell.org/trac/ghc/ticket/5927#comment:32. This probably deserves its own ticket regardless.

comment:7 Changed 19 months ago by simonpj

but my hunch is that you're experiencing the same bug as in...

Indeed: see comment:4 above, which gives exactly the same diagnosis as I gave in https://ghc.haskell.org/trac/ghc/ticket/5927#comment:33.

In both comments I point out that a local instance declaration that claims to produce evidence for Semigroup xx for any xx is very suspicious (comment:4 above).

Now you have two ways of proving SemiGroup (Free ...): from the top-level instance or from the local instance (QC). And currently the local one "wins".

For now I'm saying "not a bug" and "you probably didn't really want that program anyway". But I could obviously be wrong about the latter.

comment:8 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.