Re: Changes to Typeable

On Sun, Oct 14, 2012 at 2:34 PM, Gábor Lehel wrote:

So apologies for constantly suggesting new things, but if we have,

- All Typeable instances for type constructors are generated by the compiler, and - All Typeable instances for composite types (if that's the word?) are via instance (Typeable f, Typeable a) => Typeable (f a), and - User-written instances, and therefore overlap, are disallowed,

how difficult would it be to add:

foo :: Typeable (f a) => Dict (Typeable f, Typeable a) -- data Dict c where Dict :: c => Dict c

i.e. to make it possible to go in the other direction, and deduce that if a composite type is Typeable, its components must also be?

(alternate encoding: foo :: Typeable (f a) => ((Typeable f, Typeable a) => r) -> r)

Use case: nothing very serious, if it would take significant work, it's not worth it.

Update: I think there's at least one way: class Typeable a where proxyTypeOf :: Proxy a -> TypeRep split :: (a ~ f i) => Dict (Typeable f, Typeable i) -- split :: (a ~ f i) => ((Typeable f, Typeable i) => r) -> r instance (Typeable f, Typeable i) => Typeable (f i) where split = Dict -- split x = x and all the compiler-generated instances for type constructors would just not define split. Which if it were a user writing the code would generate a warning about unimplemented methods (or inaccessible code if they /did/ implement it), but it's not a user writing it, and nothing bad can happen, because the constraint has to hold before you can call the method (so there's no way to hit a bottom). (This would require an extension or two, but if we're already depending on PolyKinds that doesn't seem like a huge deal? And presumably a libraries proposal...)

On Fri, Oct 5, 2012 at 9:06 AM, Simon Peyton-Jones wrote:

...

| Does this imply forbidding user-written instances of Typeable? If yes, | then I guess some currently accepted programs would also be rejected | (those with manual instances)?

Yes, that's the idea; I should have said that. Allowing users to write instances leads to potential un-soundness when doing dynamic type casts, so it has always been a Bad Idea.

Simon

-- Your ship was destroyed in a monadic eruption.

-- Your ship was destroyed in a monadic eruption.