Why does this nested typeclass derivation work?

user_10930850 0
Viewed 83

Yeah, it's the unusual "why does this work" question. I have this piece of code:

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

data F a = A (F a) | B (a (F a)) -- a :: * -> *
deriving instance (forall b. Eq b => Eq (a b)) => Eq (F a)

-- the following errors, asking me to add (Eq b) into the context
deriving instance (forall b. Eq (a b)) => Eq (F a)

The second version errors out if one define

data T a = C | D a deriving Eq
x = B C == B C

From a logical aspect, adding (Eq b) to the constraints should be something like (forall b. Eq b && Eq (a b)) => Eq (F a), because we need to keep it in the scope of forall. It is conceivable that (Eq b) is assumed implicitly, as most deriving instances do. But if so, why doesn't the second version work?

typeclass haskell types
2 Answers

The first deriving equals the following instance

instance (forall b. Eq b => Eq (f b)) => Eq (F f) where
  (==) :: F f -> F f -> Bool
  A a1 == A b1 = (==) @(F f)     a1 b1
  B a1 == B b1 = (==) @(f (F f)) a1 b1
  _    == _    = False

Given that equality is closed under f (forall b. Eq b => Eq (f b)) the following constraints are wanted from (==) @(F f) and (==) @(f (F f))

  1. Eq (F f)
  2. Eq (f (F f))

For the first one is the equality instance we are writing/deriving: Eq (F f) which holds in the current context (Eq is closed under f). So that constraint is satisfied.

The second one asks for equality for our lifted type: Eq (f (F f)) which follows from the context: Eq being closed under f.

If we instantiate b with F f we see that our lifted type supports equality Eq (F f) => Eq (f (F f)) if the type we are defining supports equlity.. which it does (1.).

The second instance compiles on GHC Head.

deriving instance (forall b. Eq (f b)) => Eq (F f)

If you know that Eq (f b) holds for any b, you can solve 1. and 2. by instantiating b with F f.

user_1658060

After playing around for a little bit, I think I nailed down the problem. Sorry for editing the question frequently! I oversimplified the code, and didn't test carefully.

The data T a = C | D a derives an Eq instance that requires Eq a. Without that, the forall b. Eq (T b) premise cannot be satisfied. With forall b. (Eq b) => Eq (T b), we can use Eq b to obtain the required equality predicate on a.

user_109308500
Related