On Thu, Apr 10, 2014 at 9:27 AM, Albert Y. C. Lai wrote:

Yes, GHC accepts "X => Y => Z" and makes it "(X, Y) => Z". In fact, go

wilder:

whee :: Show a => Eq a => a => Bool whee x = x == x && null (show x)

It is valid and it means (Show a, Eq a) => a -> Bool. Try it!

What extensions do you have turned on? I'm trying this is ghci (7.6.3) and I can't get it to work even with DataKinds and ConstraintKinds. Jason

On Thu, Apr 10, 2014 at 10:21 AM, Kim-Ee Yeoh wrote:

No problems here:

# ghci GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Prelude> let whee :: Show a => Eq a => a => Bool; whee x = x == x && null (show x) Prelude> :t whee whee :: (Eq a, Show a) => a -> Bool

It seems to be an issue with giving everything on a single line: $ ghci GHCi, version 7.6.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer-gmp ... linking ... done. Loading package base ... linking ... done. Prelude λ> let whee x = x == x && null (show x) :: Show a => Eq a => a => Bool <interactive>:2:14: Couldn't match expected type `a -> Bool' with actual type `Bool' In the expression: x == x && null (show x) :: Show a => Eq a => a => Bool In an equation for `whee': whee x = x == x && null (show x) :: Show a => Eq a => a => Bool I see now to make it work as a one liner I could do it this way: Prelude λ> :t (\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool (\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool :: (Eq a, Show a) => a -> Bool Thanks!

On Thu, Apr 10, 2014 at 10:45 AM, Kim-Ee Yeoh wrote:

And to recover the named binding:

let whee = (\x -> x == x && null (show x)) :: Show a => Eq a => a => Bool

Right, or even: Prelude λ> :t let whee x = x == x && null (show x) in whee :: Show a => Eq a => a => Bool let whee x = x == x && null (show x) in whee :: Show a => Eq a => a => Bool :: (Eq a, Show a) => a -> Bool Which is what I think I meant to type initially but then confused myself and also misread the type error :) Jason

On Thu, Apr 10, 2014 at 1:43 PM, Felipe Lessa wrote:

Em 10-04-2014 13:27, Albert Y. C. Lai escreveu:

...

My understanding is that when the type checker has to support all those generalizations like ConstraintKind, DataKinds, etc etc, it becomes so general that some traditional distinctions vanish.

What? Shouldn't that be a bug?

It "should be" but I suspect actually treating it as one is rather difficult now that it's possible for `a` there to be a Constraint or etc., in which case it is on the correct side of the =>. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

On Thu, Apr 10, 2014 at 1:59 PM, Felipe Lessa wrote:

Em 10-04-2014 14:45, Brandon Allbery escreveu:

...

It "should be" but I suspect actually treating it as one is rather difficult now that it's possible for `a` there to be a Constraint or etc., in which case it is on the correct side of the =>.

What you're saying is that it would be difficult to ban this on the parser level. However, somewhere inside GHC this `a` that was used as a constraint got promoted to being an argument. This is where it should have been stopped on its track.

Actually, what I'm saying is that it might be difficult to reliably catch it at that point; consider that the parse leading to that interpretation may not exist within ghc at that point, only an AST that may have been rearranged by uses of ConstraintKinds so as to lose its direct relationship to the parse that initially led to it. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

I also find this scary. Even this works: Prelude> let whee :: (Show a, Eq a, a) => Bool; whee x = x == x && null (show x) Prelude> :t whee whee :: (Eq a, Show a) => a -> Bool But: Prelude> let test :: (Eq a) => a => b => a; test = undefined <interactive>:35:13: Illegal polymorphic or qualified type: (b) => a Perhaps you intended to use -XRankNTypes or -XRank2Types In the type signature for `test': test :: Eq a => a => b => a Prelude> :set -XRankNTypes Prelude> let test :: (Eq a) => a => b => a; test = undefined <interactive>:8:13: Illegal constraint: b (Use -XConstraintKinds to permit this) In the type signature for `test': test :: Eq a => a => b => a So this is what I'd also expect for "a" to happen. I think this is a bug. Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com Registered in England & Wales, OC335890 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England

Sorry for continuing to reply to myself. But all this seems fixed in 7.8.1: Prelude> let whee :: (Show a, Eq a, a) => Bool; whee x = x == x && null (show x) <interactive>:5:28: Expected a constraint, but 'a' has kind '*' In the type signature for 'whee': whee :: (Show a, Eq a, a) => Bool Prelude> let whee :: (Show a, Eq a) => a => Bool; whee x = x == x && null (show x) <interactive>:6:31: Expected a constraint, but 'a' has kind '*' In the type signature for 'whee': whee :: (Show a, Eq a) => a => Bool Cheers, Andres On Thu, Apr 10, 2014 at 8:37 PM, Andres Löh wrote:

And even more:

Prelude> let test :: (Eq a, a, Eq b, b) => a; test = const Prelude> :t test test :: (Eq a, Eq b) => a -> b -> a Prelude> let test :: (Eq a, Eq b, a, b) => a; test = const Prelude> :t test test :: (Eq a, Eq b) => a -> b -> a Prelude> let test :: (a, b, Eq a, Eq b) => a; test = const

<interactive>:19:35: Predicate `a' used as a type In the type signature for `test': test :: (a, b, Eq a, Eq b) => a

Cheers, Andres

-- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com

Registered in England & Wales, OC335890 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England

-- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com Registered in England & Wales, OC335890 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England

I don't have a GHC 7.8 handy. Can you check to see if:

whee :: Show a => Eq a => (a -> Bool)

works over there?

Yes, it does. I also see no problem with this one. Even this works (but funnily enough, it requires RankNTypes, even though it translates to the same type): let whee :: a -> Show a => Eq a => Bool; whee = undefined None of these are kind errors though. And while I don't know if it's clearly specified what exactly is possible, it makes sense to me to allow these. Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com Registered in England & Wales, OC335890 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England

Em 10-04-2014 15:40, Andres Löh escreveu:

Sorry for continuing to reply to myself. But all this seems fixed in 7.8.1:

Great, thanks! -- Felipe.