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

[Lana Black]

On Monday, 12 July 2021 20:59:46 UTC Viktor Dukhovni wrote:
> > On 12 Jul 2021, at 4:24 pm, Viktor Dukhovni <ietf-dane at dukhovni.org>
> > wrote:
> > 
> > However, it is possible to get something along those lines with
> 
> > a closed type family and an explicit list of verboten types:
> Somewhat cleaner (no complaints from -Wall, and the Filtered type family
> now returns a constraint):
> 
>     {-# LANGUAGE ConstraintKinds
>                , DataKinds
>                , FlexibleContexts
>                , TypeFamilies
>                , TypeOperators
>                , UndecidableInstances
>       #-}
> 
>     import GHC.TypeLits (ErrorMessage(..), TypeError)
>     import Data.Kind (Constraint)
> 
>     type family Filtered a :: Constraint where
>       Filtered Int = TypeError ('ShowType Int ':<>: 'Text "s not welcome
> here") Filtered a   = ()
> 
>     foo :: (Show a, Filtered a) => a -> String
>     foo = show

Thank you! I know this seems like an extreme case and I doubt I will ever use 
your example in any real application.

My question was prompted by the package called reflection (https://
hackage.haskell.org/package/reflection-2.1.6/docs/Data-Reflection.html), that 
allows to implicitly pass data to functions via a typeclass dictionary. The 
big issue with it however is that you can pass values of same type multiple 
times, therefore shooting yourself in the foot somewhere.

>From the manual:

>give :: forall a r. a -> (Given a => r) -> r

>Reify a value into an instance to be recovered with given.

>You should only give a single value for each type. If multiple instances are 
in scope, then the behavior is implementation defined.

I was curious whether it would be possible to allow `give` to be used only 
once in the same call stack with something like

give :: forall a r. Not (Given a) => a -> (Given a => r) -> r

If this even makes sense.