Hi, is it not allowed simply because none has needed it yet, or is there a deeper theoretical problem with it? I’m asking because the implementation of Coercible behaves as if there is an instance instance forall a. (Coercible (t1 a) (t2 a)) => Coercible (forall a. t1 a) (forall a. t2 a) and if were theoretically dubious, I’d like to know about it :-) Greetings, Joachim Am Dienstag, den 07.01.2014, 10:11 -0500 schrieb Andrew Gibiansky:

Ah, I see. I wasn't aware that constraints had to be over monotypes. I figured that since you could write a function

f :: (forall a. a -> a) -> Bool

Then you could also do similar things with a class.

(The reason I was doing this was that I wanted a typeclass to match something like "return 'a'" without using IncoherentInstances or other sketchiness, and found that trying to have a typeclass with an instance for 'forall m. Monad m => m Char` gave me this error.)

Thanks! Andrew

On Tue, Jan 7, 2014 at 5:18 AM, Roman Cheplyaka wrote: * Andrew Gibiansky [2014-01-06 22:17:21-0500] > Why is the following not allowed? > > {-# LANGUAGE ExistentialQuantification, ExplicitForAll, RankNTypes, > FlexibleInstances #-} > > class Class a where > test :: a -> Bool > > instance Class (forall m. m -> m) where > test _ = True > > main = do > putStrLn $ test id > > Is there a reason that this is forbidden? Just curious.

I believe the rule is that all constraints (including class constraints) range over monotypes.

What are you trying to achieve?

You can do this, for example:

newtype Poly = Poly (forall a . a -> a) instance Class Poly where test = const True

main = print $ test $ Poly id

BTW, this has nothing to do with ExistentialQuantification.

Roman

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org

I think allowing polytype instances would lead to incoherence. This is, of course, OK with Coercible (where incoherence is rife and completely appropriate). But, consider

instance Foo (forall a. [a]) where ... instance Foo [Int] where ...

bar :: Foo b => b -> ...

quux = bar []

Which instance should be used in the call to `bar`? Perhaps those two instances would just be considered overlapping. Another related issue is that making polytype instances useful seems to require impredicativity. Recall that impredicativity means allowing type variables to take on polytype values. (Normally, type variables are always instantiated to monotypes.) Type inference in the presence of impredicativity is wonky at best. A colleague (Hamidhasan Ahmed) is working on allowing explicit type applications, which would greatly help with impredicative inference. When that's working, I think polytype instances may make more sense. Though, in the end, I agree that this takes some Careful Thought. Richard On Jan 7, 2014, at 10:16 AM, Joachim Breitner wrote:

Hi,

is it not allowed simply because none has needed it yet, or is there a deeper theoretical problem with it?

I’m asking because the implementation of Coercible behaves as if there is an instance instance forall a. (Coercible (t1 a) (t2 a)) => Coercible (forall a. t1 a) (forall a. t2 a) and if were theoretically dubious, I’d like to know about it :-)

Greetings, Joachim

Am Dienstag, den 07.01.2014, 10:11 -0500 schrieb Andrew Gibiansky:

...

Ah, I see. I wasn't aware that constraints had to be over monotypes. I figured that since you could write a function

f :: (forall a. a -> a) -> Bool

Then you could also do similar things with a class.

(The reason I was doing this was that I wanted a typeclass to match something like "return 'a'" without using IncoherentInstances or other sketchiness, and found that trying to have a typeclass with an instance for 'forall m. Monad m => m Char` gave me this error.)

Thanks! Andrew

On Tue, Jan 7, 2014 at 5:18 AM, Roman Cheplyaka wrote: * Andrew Gibiansky [2014-01-06 22:17:21-0500]

...

Why is the following not allowed?

{-# LANGUAGE ExistentialQuantification, ExplicitForAll, RankNTypes, FlexibleInstances #-}

class Class a where test :: a -> Bool

instance Class (forall m. m -> m) where test _ = True

main = do putStrLn $ test id

Is there a reason that this is forbidden? Just curious.

I believe the rule is that all constraints (including class constraints) range over monotypes.

What are you trying to achieve?

You can do this, for example:

newtype Poly = Poly (forall a . a -> a) instance Class Poly where test = const True

main = print $ test $ Poly id

BTW, this has nothing to do with ExistentialQuantification.

Roman

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe