Oh, very nice approach Viktor. It really seems easier than having a custom typeclass for which the blessed types have an instance, if the set of verboten types is considerably smaller than the set of allowed types. Le 12/07/2021 à 22:59, Viktor Dukhovni a écrit :

...

On 12 Jul 2021, at 4:24 pm, Viktor Dukhovni 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

-- Hécate ✨ 🐦: @TechnoEmpress IRC: Hecate WWW: https://glitchbra.in RUN: BSD

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.

On 13 Jul 2021, at 1:56 pm, Lana Black wrote:

...

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

Frankly, I'd rather stick to multireaders. Reflection seems to me like a worse case of extreme language abuse.

When clear and effective alternatives exist, by all means keep it simple. With reflection you get run-time type classes, which can be useful, but I agree should generally not be the first thing you reach for... -- Viktor.