Simplifying an instance context makes a rewrite rule no longer typecheck

This code (taken from the reducers package) compiles:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

import Prelude (Applicative(..), Functor(..), (.))

class Semigroup m where
  (<>) :: m -> m -> m

class Semigroup m => Reducer c m where
  snoc :: m -> c -> m

newtype Traversal f = Traversal { getTraversal :: f () }

instance Applicative f => Semigroup (Traversal f) where
  Traversal a <> Traversal b = Traversal (a *> b)

instance Applicative f => Reducer (f a) (Traversal f) where
  Traversal a `snoc` b = Traversal (() <$ (a *> b))

snocTraversal :: Reducer (f ()) (Traversal f) => Traversal f -> f () -> Traversal f
snocTraversal a = (<>) a . Traversal
{-# RULES "snocTraversal" snoc = snocTraversal #-}

But on GHC 8.2.1 and later, it gives this warning:

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:21:18: warning: [-Wsimplifiable-class-constraints]
    • The constraint ‘Reducer (f ()) (Traversal f)’
        matches an instance declaration
      instance Applicative f => Reducer (f a) (Traversal f)
        -- Defined at Bug.hs:18:10
      This makes type inference for inner bindings fragile;
        either use MonoLocalBinds, or simplify it using the instance
    • In the type signature:
        snocTraversal :: Reducer (f ()) (Traversal f) =>
                         Traversal f -> f () -> Traversal f
   |
21 | snocTraversal :: Reducer (f ()) (Traversal f) => Traversal f -> f () -> Traversal f
   |                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I decided to follow GHC's orders and reduce the Reducer (f ()) (Traversal f) context to just Applicative f:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

import Prelude (Applicative(..), Functor(..), (.))

class Semigroup m where
  (<>) :: m -> m -> m

class Semigroup m => Reducer c m where
  snoc :: m -> c -> m

newtype Traversal f = Traversal { getTraversal :: f () }

instance Applicative f => Semigroup (Traversal f) where
  Traversal a <> Traversal b = Traversal (a *> b)

instance Applicative f => Reducer (f a) (Traversal f) where
  Traversal a `snoc` b = Traversal (() <$ (a *> b))

snocTraversal :: Applicative f => Traversal f -> f () -> Traversal f
snocTraversal a = (<>) a . Traversal
{-# RULES "snocTraversal" snoc = snocTraversal #-}

But after doing so, the file no longer typechecks!

GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:23:34: error:
    • Could not deduce (Applicative f)
        arising from a use of ‘snocTraversal’
      from the context: Reducer (f ()) (Traversal f)
        bound by the RULE "snocTraversal" at Bug.hs:23:11-46
      Possible fix:
        add (Applicative f) to the context of the RULE "snocTraversal"
    • In the expression: snocTraversal
      When checking the transformation rule "snocTraversal"
   |
23 | {-# RULES "snocTraversal" snoc = snocTraversal #-}
   |                                  ^^^^^^^^^^^^^

Trac metadata

Trac field	Value
Version	8.2.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

Here's a simpler example:

{-# LANGUAGE GADTs, FlexibleContexts, NoMonoLocalBinds #-}

data T a where
  MkT :: Eq a => a -> T a

f :: T [b] -> Bool
f (MkT xs) = g xs

g :: Eq [b] => [b] -> Bool
g xs = xs == xs

We get

T14322.hs:12:6: warning: [-Wsimplifiable-class-constraints]
    * The constraint `Eq [b]' matches an instance declaration
      instance Eq a => Eq [a] -- Defined in `GHC.Classes'
      This makes type inference for inner bindings fragile;
        either use MonoLocalBinds, or simplify it using the instance

But you can't simplify g's type signature, becuase then at the call site in f we get a wanted Eq a dictionary which we can't get from a given Eq [a] dictionary bound by the existential.

The exact same thing is happening with your RULE.

I don't see a great solution here. Personally I's use MonoLocalBinds to suppress the warning.

closed

Very well. I suppose then that the warning is as accurate as it can possibly be in this scenario, since it advertises MonoLocalBinds.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

added Pnormal label