Allowing only different 'any' types in Haskell

Question

Say we have a function with signature

foo :: a -> b -> Int

Is it possible to enforce a constraint ensuring that a and b are different? That is

foo :: Int -> String -> Int -- ok
foo :: Int -> Int    -> Int -- not ok

The purpose of this question is to learn more about Haskell and perhaps solve a design issue I'm facing. My particular case does not make sense if a == b, so I'd like to disallow that at the compiler level. I probably could make this issue go away with a different design altogether but that's besides the point now - the Pandoras box has been opened and I'd like to learn if an equality constraint on the type level is possible.

Answer 1

Like this?

{-# LANGUAGE DataKinds #-}
module TyEq where

import Data.Type.Equality (type (==))
import GHC.TypeLits
import Data.Kind (Constraint)

class ((a == b) ~ eq) => Foo a b eq where
  foo :: a -> b -> Int

instance (TypeError ('Text "NAUGHTY!"), (a == b) ~ True) => Foo a b 'True where
  foo _ _ = error "The types have failed us!"

instance (a == b) ~ False => Foo a b 'False where
  foo _ _ = 42

--_ = foo True True -- NAUGHTY!
_ = foo () True
_ = foo True (42 :: Int)

Notice how the eq index is needed in the Foo type class, or we're getting 'duplicate instance' errors despite differing instance contexts (only heads are taken into account).

We can streamline that a bit using purpose-specific type family:

type family Check a b :: Constraint where
  Check a a = TypeError ('Text "VERY NAUGHTY!")
  Check a b = ()

foo' :: Check a b => a -> b -> Int
foo' _ _ = 42

--_ = foo' True True -- VERY NAUGHTY!
_ = foo' () True
_ = foo' True (42 :: Int)

I'm pretty sure I've learnt that all from Sandy Maguire's 'Thinking with Types', which I sincerely recommend to everyone interested :)

Answer 2

The type a :~: b -> Void is inhabited (by a total function) exactly when a and b are different, so one lightweight way would be to take one as an argument. You can then ask the compiler to check whether callers supply a total argument with -Wincomplete-patterns. A complete example might look like this:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}

import Data.Void
import Data.Type.Equality

foo :: (a :~: b -> Void) -> a -> b -> Int
foo _ _ _ = 0

fooUseGood :: Int
fooUseGood = foo (\case) True () -- accepted, no warning

fooUseBad :: Int
fooUseBad = foo (\case) () () -- warning: Patterns not matched: Refl

Answer 3

Here's a riff on Artur's version. It uses machinery developed for the trivial-constraints package.

{-# LANGUAGE DataKinds, KindSignatures, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, ExplicitNamespaces, TypeOperators, UndecidableSuperClasses, UndecidableInstances #-}


import Data.Type.Equality (type (==))
import GHC.TypeLits
import GHC.Exts (Any)

-- The Any constraint prevents malicious/ignorant
-- instantiation with no = undefined. The only
-- way to produce an instance of this class is in a local context
-- using something deeply unsafe like unsafeCoerce, magicDict, or unsafePerformIO.
class Any => Bottom where
  no :: a

-- Why not just put the `no` method in this class?
-- Because then `no` will need to be applied to the type argument `e`, which is
-- very annoying and unnecessary.
class (TypeError e, Bottom) => Oops e

class Foo a b (eq :: Bool) where
  foo' :: a -> b -> Int

foo :: forall a b. Foo a b (a == b) => a -> b -> Int
foo = foo' @a @b @(a == b)

instance Oops ('Text "NAUGHTY!") => Foo a b 'True where
  foo' = no

instance Foo a b 'False where
  foo' _ _ = 42