[Haskell-cafe] Check a lack of a constraint?

[Viktor Dukhovni]

> On 12 Jul 2021, at 2:24 pm, Lana Black <lanablack at amok.cc> wrote:
> 
> Is it possible in Haskell to check a lack of a certain constraint?

Such a check is semantically dubious, because the complete list of
instances for a given type is unknowable; given orphan instances,
an instance could be defined in some module that has not been
imported at the call site.  So wanting to do this suggests the
possibility of a design issue.

> For example,
> 
> ```
> foo :: C => a
> foo = undefined
> 
> ```

However, it is possible to get something along those lines with
a closed type family and an explicit list of verboten types:

    {-# LANGUAGE DataKinds
           , FlexibleContexts
           , TypeFamilies
           , UndecidableInstances #-}
    
    import GHC.TypeLits (ErrorMessage(..), TypeError)
    
    type family Filtered a where
      Filtered Int = TypeError (Text "Ints not welcome here")
      Filtered a   = a
    
    foo :: (Show a, a ~ Filtered a) => a -> String
    foo = show

As seen in:

    λ> foo ('a' :: Char)
    "'a'"
    λ> foo (1 :: Int)

    <interactive>:2:1: error:
        • Ints not welcome here
        • In the expression: foo (1 :: Int)
          In an equation for ‘it’: it = foo (1 :: Int)

-- 
	Viktor.