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

12 Jul 2021

      ...
On 12 Jul 2021, at 2:24 pm, Lana Black  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.

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

Viktor Dukhovni