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

[Viktor Dukhovni]

On Tue, Jul 13, 2021 at 03:07:39PM +0000, Lana Black wrote:

> > 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.

Indeed, since this is generally a rather odd thing to do.

> 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.

This is only a problem if these multiple times are *nested*:

    module Test (foo) where
    import Data.Reflection

    foo :: Int -> Int
    foo x = give x given

    bar :: Int -> Int
    bar x = give x $
        let y :: Int
            y = given
         in give (y + 5) given

in the above, you can call `foo` as many times as you like, with
separate values, but `bar` does not behave as one might wish.

> 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.

If you're concerned about nested uses of `Given` the simplest solution
is to just use `reify` and `reflect` and avoid `given`:

    baz :: Int -> Int
    baz x = reify x $ \p ->
        let y :: Int
            y = reflect p
         in reify (y + 5) reflect

-- 
    Viktor.