Could you write a type function to invert a constraint?

Question

Is it possible to write a type function that would take a constraint like Show and return one that constrains the RHS to types that are not an instance of Show?

The signature would be something like

type family Invert (c :: * -> Constraint) :: * -> Constraint

Answer 1

No. It is a design principle of the language that you are never allowed to do this. The rule is if a program is valid, adding more instances should not break it. This is the open-world assumption. Your desired constraint is a pretty direct violation:

data A = A
f :: Invert Show a => a -> [a]
f x = [x]
test :: [A]
test = f A

Would work, but adding

instance Show A

would break it. Therefore, the original program should never have been valid in the first place, and therefore Invert cannot exist.

Answer 2

As HTNW answered, it is in general not supposed to be possible to assert that a type is not an instance of a class. However, it is certainly possible to assert for a concrete type that it's never supposed to be possible to have an instance of some class for it. An ad-hoc way would be this:

{-# LANGUAGE ConstraintKinds, KindSignatures, AllowAmbiguousTypes
           , MultiParamTypeClasses, FlexibleInstances #-}

import GHC.Exts (Constraint)

class Non (c :: * -> Constraint) (t :: *) where
  nonAbsurd :: c t => r

But this is unsafe – the only way to write an instance is, like,

instance Non Show (String->Bool) where
  nonAbsurd = undefined

but then somebody else could come up with a bogus instance Show (String->Bool) and would then be able to use your nonAbsurd for proving the moon is made out of green cheese.

A better option to make an instance impossible is to “block” it: write that instance yourself “pre-emptively”, but in such a way that it's a type error to actually invoke it.

import Data.Constraint.Trivial -- from trivial-constraint

instance Impossible0 => Show (String->Bool) where
  show = nope

Now if anybody tries to add that instance, or tries to use it, they'll get a clear compiler error.