'idiomatic' Haskell type inequality

ghc, haskell, type-equivalence, types

Solution

With new features being added to GHC, you'll be able to write:

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}

type family Equal (a :: k) (b :: k) :: Bool
type instance where
   Equal a a = True
   Equal a b = False

Problem

(edited from previous question where I thought code below doesn't work) I wish to implement a haskell function f that has a restriction such that its 2 parameters must not have the same type. I have used the following code: ``` {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, FlexibleInstances, FlexibleContexts, TypeFamilies, IncoherentInstances #-} data HTrue = HTrue data HFalse = HFalse class HEq x y b | x y -> b instance (b ~ HTrue) => HEq x x b instance (b ~ HFalse) => HEq x y b g :: (HEq a b HFalse) => a -> b -> () g x y = () ``` Now the function g only accepts a and b if they have different types. Is this the 'idiomiatic' way to code type inequality in haskell? If not, what are the problems with it?

Original source

Related problems