Allowing only different 'any' types in Haskell

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 :)

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

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