We have a constraint (a~b) that can appear in a type signature

                f :: (a~b) => a -> b

We can also have a type-level equality function

                type family Eq a b where

                   Eq a a = True

                   Eq a b = False

The type-level Boolean reflects the (a~b) constraint precisely.

You sound as if you want a type family Satisfied, so you

                type family Satisfied :: Constraint -> Bool

Then you could have

                instance Ord T where …

                type instance Satisfied (Ord T) = True

The difficulty is that we can never return False, because you can always make T an instance of Ord “later”.  And you can’t have Satisfied (Ord T) returning True in one place and Falsie in another.  It can get stuck (not reduce) but it can’t return False.

I don’t know if this would be useful to you.

And for more complex instances lie

                instance Ord a => Ord [a]

I don’t know what you want to say for

                type instance Satisfied (Ord a) = ???

Simon

From: Libraries [mailto:libraries-bounces@haskell.org] On Behalf Of Ryan Newton
Sent: 15 October 2013 04:03
To: Pedro Magalhães (dreixel@gmail.com)
Cc: Haskell Libraries; Andres Löh; Ganesh Sittampalam; ghc-devs@haskell.org
Subject: Re: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

Hey, that's an awesome formulation!  Thanks Pedro.

Any idea how much work this would be to implement in GHC, if it did garner approval?

On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães <dreixel@gmail.com> wrote:

Hi,

On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall <dag.odenhall@gmail.com> wrote:

Here‘s a thought: doesn’t Generic already have an unused phantom type that's only there “just in case we need to add something in the future”?

No, it doesn't.

Just a thought: what if we had a type family

type family Derives (t :: k1) (c :: k2) :: Bool

which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code:

data MyData = MyData deriving (Eq, Generic)

deriving instance Show MyData

instance Ord MyData

GHC would automatically instantiate:

type instance Derives MyData Eq      = True
type instance Derives MyData Generic = True
type instance Derives MyData Show    = True
type instance Derives MyData Ord     = False

Would this be something Ryan could use for detecting safe instances for LVish?

Cheers,
Pedro

_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs