Is it possible to place inequality constraints on haskell type variables?

user_1386599 0
Viewed 2769

Is it possible to place an inequality constraint on the typevariables of a function, à la foo :: (a ~ b) => a -> b as in GHC type family docs, except inequality rather than equality?

I realise that there is possibly no direct way to do this (as the ghc docs doesn't list any to my knowledge), but I would be almost puzzled if this weren't in some way possible in light of all the exotic type-fu I have been exposed to.

type-inference type-systems haskell
4 Answers

Now one can use == from Data.Type.Equality (or from singletons library) with DataKinds extension:

foo :: (a == b) ~ 'False => a -> b
user_18165030

Improving on Boldizsar's answer, which is itself an improvement of the accepted answer:

{-# language DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

import Data.Kind (Constraint)
import GHC.TypeLits (TypeError, ErrorMessage(..))

data Foo = Foo

data Bar = Bar

notBar :: Neq Bar a => a -> ()
notBar _ = ()

type family Neq a b :: Constraint where
  Neq a a = TypeError
    ( 'Text "Expected a type that wasn't "
    ':<>: 'ShowType a
    ':<>: 'Text "!"
    )
  Neq _ _ = ()


*Main> notBar Foo
()
*Main> notBar Bar

<interactive>:12:1: error:
    • Expected a type that wasn't Bar!
    • In the expression: notBar Bar
      In an equation for ‘it’: it = notBar Bar

The type errors for this are good, and it is very readable.

user_91254400
Related