Incoherence using only overlapping instances and existentials, and avoiding it using a type family

Overlapping.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

import Prelude hiding (compare)
import Data.Type.Equality

class Compare a b where
  compare :: Maybe (a :~: b)

instance Compare a a where
  compare = Just Refl

instance {-# OVERLAPPABLE #-} Compare a b where
  compare = Nothing

test1 :: Maybe (Int :~: Bool)
test1 = compare

test2 :: Maybe (Int :~: Int)
test2 = compare

data Test3 = forall a b. Test3 a b

test3 :: Test3 -> String
test3 (Test3 (_ :: a) (_ :: b)) = show (compare :: Maybe (a :~: b))

test3a, test3b :: String
test3a = test3 $ Test3 'a' True
test3b = test3 $ Test3 'a' 'b'

TypeFamilies.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Prelude hiding (compare)
import Data.Proxy
import Data.Type.Equality

type family IsEq a b where
  IsEq a a = 'True
  IsEq a b = 'False

class Compare' (a :: *) (b :: *) (isEq :: Bool) where
  compare' :: Proxy a -> Proxy b -> Proxy isEq -> Maybe (a :~: b)

instance Compare' a a 'True where
  compare' _ _ _ = Just Refl

instance Compare' a b 'False where
  compare' _ _ _ = Nothing

class Compare (a :: *) (b :: *) where
  compare :: Maybe (a :~: b)

instance Compare' (a :: *) (b :: *) (IsEq a b) => Compare a b where
  compare = compare' (Proxy :: Proxy a) (Proxy :: Proxy b) (Proxy :: Proxy (IsEq a b))

test1 :: Maybe (Int :~: Bool)
test1 = compare

test2 :: Maybe (Int :~: Int)
test2 = compare

data Test3 = forall a b. Test3 a b

test3 :: Test3 -> String
test3 (Test3 (_ :: a) (_ :: b)) = show (compare :: Maybe (a :~: b))

test3a, test3b :: String
test3a = test3 $ Test3 'a' True
test3b = test3 $ Test3 'a' 'b'