Why standalone deriving fails with rigid type on a record with existential quantification?

Question

I am trying to compare associated types with existential ones, and wrote following snippet:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}

import Prelude 

data App = forall t. Eq t => App { f :: t }

deriving instance Eq App  

Type checks barks with:

Couldn't match expected type ‘b’ with actual type ‘b1’ ‘b1’ is a rigid type variable bound by

At first glance the same snippet is provided as a solution on stack overflow earlier.

I found probably related GHC issue, but disabling PolyKinds extension doesn't have any effect and Polysemy plugin either.

GHC 9.2.5 is used.

P.S.

So in practice both approaches don't support deriving.

Answer 1

This isn't a GHC bug: there just isn't a sensible definition of (==) :: App -> App -> Bool in the first place.

Given a :: App and b :: App, we know they must be (disregarding bottoms) a = App x for some x (of some type X with Eq X) and b = App y for some y (of some type Y with Eq Y). But because you defined App existentially, there's absolutely no reason for x and y to be comparable, since they have different types. Within each type X and Y, you could use the Eq methods. So x == x makes sense, and so does y == y, but x == y doesn't make sense, since you'd be using (==) at the type X -> Y -> Bool. Therefore the tentative definition

instance Eq App where App x == App y = x == y

is considered nonsense, regardless of whether it's generated by deriving or written by hand. The type error you are getting is, at it's heart, just "you are trying to use (==) on objects of potentially different types."

Or, in short, exactly how is the expression App (5 :: Int) == App ("5" :: String) supposed to evaluate?

Perhaps you would like it if objects of different types always compared disequal. Then you need to store type information in App using Typeable or TypeRep. You compare for type equality first, and only upon getting a yes can you compare the values.

import Data.Typeable
data App = forall t. (Typeable t, Eq t) => App t
instance Eq App where
  App x == App y = case cast y of -- try to cast y to type of x (type information flows from (1))
    Just y' -> x == y' -- (1) x and y' are (==)'d, so they must be of the same type
    Nothing -> False