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

On Monday, 12 July 2021 20:59:46 UTC Viktor Dukhovni wrote:

...

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

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.