Detecting redundant constraints in Haskell?

Question

Is there any way of detecting redundant constraints in Haskell?

For example:

class    (A a, B a) => C1 a -- C1 ~ A AND B
instance (A a, B a) => C1 a

class    (A a, B a, C a) => C2 a
instance (A a, B a, C a) => C2 a

f :: (C1 a, C2 a) => a
f = ...

Here, C2 implies C1, and use of C1 in the signature of f is redundant, i.e. tautological.

In a real-world metaprogramming situation, This would be waaaay more complex, and would significantly help de-clutter signature heads, as well as help me understand and keep track of what is going on.

Is this logically possible, given GHC's formalism?

Is the infrastructure available within GHC?

Answer 1

If I put your stub in a file:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
class A a
class B a
class C a

class    (A a, B a) => C1 a -- C1 ~ A AND B
instance (A a, B a) => C1 a

class    (A a, B a, C a) => C2 a
instance (A a, B a, C a) => C2 a

Then you can learn about redundant constraints by binding a variable to undefined and the type you're interested in reducing in ghci:

> x = undefined :: (C1 a, C2 a) => a

<interactive>:1:18: warning: [-Wsimplifiable-class-constraints]
    • The constraint ‘C1 a’ matches
        instance forall a. (A a, B a) => C1 a -- Defined at test.hs:8:10
      This makes type inference for inner bindings fragile;
        either use MonoLocalBinds, or simplify it using the instance
    • In an expression type signature: (C1 a, C2 a) => a
      In the expression: undefined :: (C1 a, C2 a) => a
      In an equation for ‘x’: x = undefined :: (C1 a, C2 a) => a

<interactive>:1:18: warning: [-Wsimplifiable-class-constraints]
    • The constraint ‘C2 a’ matches
        instance forall a. (A a, B a, C a) => C2 a
          -- Defined at test.hs:11:10
      This makes type inference for inner bindings fragile;
        either use MonoLocalBinds, or simplify it using the instance
    • In an expression type signature: (C1 a, C2 a) => a
      In the expression: undefined :: (C1 a, C2 a) => a
      In an equation for ‘x’: x = undefined :: (C1 a, C2 a) => a
*Main
> :t x
x :: forall {a}. (A a, B a, C a) => a

The first two warnings in this case are actually just a happy accident, related to how simple your stub is; you won't always get them. The truly interesting bit is the second query, :t x, which has reduced the constraints to the basic facts that you need to know about a.