Force GHC to ignore missing type constraint

Question

I built a type Sup that embeds a value of another type t using constructor subtyping.

data Sup t = ...
           | Sub t 
           deriving Eq

Because the part omitted from Sup contains lots of constructors, none of which use t, I want to derive Eq (Sup t) rather than give a manual instance.

A type constraint Eq t is now in place on the instance of (==) for Sup t:

(==) :: Eq t => Sup t -> Sup t -> Bool

The predicate isSub :: Sup t -> Bool is defined as follows:

isSub :: Sup t -> Bool
isSub (Sub _) = True
isSub _       = False

With the help of this predicate I would like to define the following operator:

supEq :: Sup t -> Sup t -> Bool
supEq x y = not (isSub x) && not (isSub y) && x == y

The above definition is not accepted by GHC, as the type-constraint Eq t is missing. However, thanks to lazy evaluation, I know that equality between values of type t is never actually used.

Is there a way that I can force GHC to ignore the missing type-constraint? Alternatively, is there a way I could have defined Sup or supEq to get the desired result: a definition of supEq without having to propagate a redundant type constraint wherever supEq is used and without having to give a manual instance for Eq (Sup t).

Answer 1

Probably the easiest thing to do is define a custom Eq (Sup t) instance.

instance (Eq t) => Eq (Sup t) where
  (Sub a) == (Sub b) = a == b
  A == A = True
  ...

Alternatively, if you want == to behave like supEq (so you don't need supEq at all), you can write the instance without the constraint:

instance Eq (Sup t) where
  (Sub a) == (Sub b) = False
  A == A = True
  ...

Another approach is to split Sup t into two data types:

data Sup' = A | B | ... | Z deriving (Eq) -- nothing depends on `t`
data Sup t = Sub t | Sup'

supEq :: Sup t -> Sup t -> Bool
supEq (Sub _) _ = False
supEq _ (Sub _) = False
supEq a b = a == b

Of course yet a final option is to subvert the type system. This is almost certainly the wrong thing to do, but I'll leave that determination to you.

{-# LANGUAGE ScopedTypeVariables #-}
import Data.Constraint

supEq :: forall t . Sup t -> Sup t -> Bool
supEq x y = let Dict = unsafeCoerce (Dict :: Dict ()) :: Dict (Eq t)
            in not (isSub x) && not (isSub y) && x == y

Answer 2

Of course the simplest solution is to split your type into two types, as others have suggested. But this creates syntactic noise - an extra level of constructors. If you want the best of both you could use reflection:

import Data.Reflection
import Data.Proxy 
import Data.Coerce 

data Sup t = Sub t | A | B | C | D | E -- .. etc
  deriving (Eq, Show) 

We will now use the generated Eq code for Sup, but substitute in a different function, not (==), when comparing Sub with Sub.

First you need some setup (I think this should be in the reflection package itself - it has similair code for Monoid and Applicative):

newtype ReifiedEq a = ReifiedEq { eq :: a -> a -> Bool } 
newtype ReflectedEq s a = ReflectedEq a 

instance Reifies s (ReifiedEq a) => Eq (ReflectedEq s a) where 
  (==) = coerce (eq (reflect (Proxy :: Proxy s))) 

This is the heart of the solution - a value of type ReflectedEq s a is just an a, but when compared for equality uses the equality function provided by Reifies, which you can specify at any time. Note that the reflection package uses type level machinery to prevent multiple Eq instances from being used in the same context.

Now you can write a function even more general than your desired one:

supEqWith :: (t -> t -> Bool) -> Sup t -> Sup t -> Bool 
supEqWith k x y = reify (ReifiedEq k) (\p -> h p x == h p y) where 
  h :: Proxy s -> Sup a -> Sup (ReflectedEq s a) 
  h _ = coerce 

This function simply compares the Sup values for equality, using the specified function (k) to compare t values inside Sub. The h function is needed to specify the phantom type parameter (s) correctly, otherwise it is ambiguous.

Your desired function is simply:

supEq = supEqWith (\_ _ -> False) 

Answer 3

If your Sup type can be a functor in t (deriving Functor would work on the example you've given), and you know that none of the other constructors use t, then you could fmap (const ()) it.

Then you've got a guarantee that the t won't affect the equality check interestingly and don't need the original t to have Eq. You just need to guard the case when both inputs were some Sub _ so that you return false instead of true.

subEq (Sub _) _ = False
subEq _ (Sub _) = False
subEq x y = fmap (const ()) x == fmap (const ()) y

Even if you don't want to make Sup a functor, you could still implement submap :: (a -> b) ->Sup a -> Sup b and use that.

Answer 4

There is no way of getting rid of the Eq constraint if you use (==) while sticking with the unsurprising derived instance. Furthermore, as far as supEq is concerned your invariant is not being enforced (consider what would happen if you committed a mistake and swapped True and False in isSub). You are probably better off writing supEq in terms of Sup pattern matches alone:

data Sup t = Foo
           | Bar
           | Sub t 
           deriving Eq

supEq :: Sup t -> Sup t -> Bool
supEq (Sub _) _ = False
supEq _ (Sub _) = False
supEq Foo Foo = True
supEq Bar Bar = True
supEq _ _ = False

If there are enough cases that writing supEq in this way becomes annoying, you can split the non-Sub cases into a separate type, as in the next-to-last example in crockeea's answer, reproduced below for the sake of completeness:

data Sup' = Foo | Bar deriving (Eq)
data Sup t = Sub t | NotSub Sup' deriving (Eq)

supEq :: Sup t -> Sup t -> Bool
supEq (Sub _) _ = False
supEq _ (Sub _) = False
supEq (NotSub a) (NotSub b) = a == b