{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE TypeFamilies #-}

import           Data.Coerce (Coercible)
import           Data.Kind   (Constraint, Type)
import           Data.Proxy  (Proxy)

data DistinctInstancesTrue k a b
data DistinctInstancesFalse

type family DistinctInstances (k :: Type -> Constraint) (a :: Type) (b :: Type) where
  DistinctInstances k a a = DistinctInstancesFalse
  DistinctInstances k a b = DistinctInstancesTrue k a b

proof :: (k a, k b) => DistinctInstancesTrue k a b -> Bool
proof _  = True

main = do
  print $ proof (undefined :: DistinctInstances Num Int Float)