[GHC] #9569: Tuple constraints don't work right

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Consider this program: {{{ {-# LANGUAGE RankNTypes, ConstraintKinds, KindSignatures, DataKinds, TypeFamilies #-} module Wrong where import GHC.Prim data Proxy (c :: Constraint) class Deferrable (c :: Constraint) where defer :: Proxy c -> (c => a) -> a deferPair :: (Deferrable c1, Deferrable c2) => Proxy (c1,c2) -> ((c1,c2) => a) -> a deferPair = undefined instance (Deferrable c1, Deferrable c2) => Deferrable (c1,c2) where -- defer p f = deferPair p f -- Succeeds defer = deferPair -- Fails }}} The first (commented-out) definition of `defer` in the instance declaration succeeds; but the second fails with an utterly bogus message {{{ ConstraintBug.hs:27:13: Could not deduce (c1 ~ (c1, c2)) from the context (Deferrable c1, Deferrable c2) }}} The reason is that when type-checking the method defintion we try to unify {{{ ((c1,c2) => a) ~ ((gamma1, gamma2) => alpha) }}} where * the LHS comes from instantiating the signature `(c => a)` (from the class decl) with `(c1,c2)/c` from the instance. * the RHS comes from instantiating the type of `deferPair` with fresh unification variables. The difficulty is that in the type of `deferPair`, the concrete syntax {{{ deferPair :: ...((c1,c2) => a)... }}} is really just syntactic sugar for {{{ deferPair :: ...(c1 => c2 => a)... }}} i.e. curried. But the function in the instantiated signature really has one constraint argument, a pair, not two. It's not clear how to fix this. It would actually be more consistent if {{{ f :: (Eq a, Show a) => blah }}} really did take a pair of dictionaries, rather than two curried dictionaries. But that would be a pretty big change, forced by a corner case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => polykinds/T9569, typecheck/should_compile/T9569a -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Resolution: | Keywords:
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets:
Test Case: |
polykinds/T9569, |
typecheck/should_compile/T9569a |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones

#9569: Tuple constraints don't work right
-------------------------------------+-------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Resolution: | Keywords:
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets:
Test Case: |
polykinds/T9569, |
typecheck/should_compile/T9569a |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => fixed Comment: Ha! Fixed at last. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by luite): The commit for this changes behaviour of impredicative types, the following does not typecheck anymore: {{{#!hs {-# LANGUAGE ImpredicativeTypes #-} f :: ((forall a. a -> a) -> b) -> b f x = x id g :: ((a -> b) -> c) -> ((a -> b) -> c) g = id h :: ((forall a. a -> a) -> b) -> b h = g f }}} I get the following error: {{{ test.hs:10:7: Couldn't match expected type ‘forall a. a -> a’ with actual type ‘a0 -> a0’ In the first argument of ‘g’, namely ‘f’ In the expression: g f Failed, modules loaded: none. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): GHC's behaviour for `-XImpredicativeTypes` is wildly unpredicatable; it's really not a supported feature at all. Does it matter to you? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by luite): I just wanted to check if this is not an unexpected side effect of the patch, since I didn't see any mention of this. I avoid `-XImpredicativeTypes` in my own code, but GHCJS indirectly depends on the `monad-control` and `lifted-base` packages, which fail to build now because they do use it, so I can't test GHCJS anymore on the latest head. I haven't found a workaround yet. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): OK, well `monad-control` and `lifted-base` are living (very) dangerously. I make no claims whatever about GHC's support for impredicativity. Might be worth talking to the maintainers about fixing that; it's usually a question of adding some newtype wrappers. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by luite): I'll let them know, but I might first do some quick and dirty patching of the dependencies to get my stuff working again. I've been working on a new code generator with much reduced (dangerous) dependencies (and other improvements like a typed intermediate rep) to avoid problems like this, but unfortunately didn't have it ready in time for 7.10. I've been increasingly unhappy with current approach of developing against the stable GHC API, porting everything to the next version at the end of the cycle, so I'll announce/discuss some changes on `ghc-devs` for the next iteration. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by basvandijk): Maintainer of `monad-control` here. Do I get the following right (I haven't looked at this in detail yet): To work around not having to use the unstable `ImpredicativeTypes` I should turn the [https://github.com/basvandijk/monad- control/blob/master/Control/Monad/Trans/Control.hs#L143 Run] type synonym into a `newtype`. Then at every call site of [https://github.com/basvandijk/monad- control/blob/master/Control/Monad/Trans/Control.hs#L127 liftWith] I need to unwrap the `newtype` to be able to apply the inner function. ? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by basvandijk): * cc: basvandijk (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Bas, I'm not sure. I don't see anything impredicative about `Run`, just higher rank. Moreover, I see no mention of `-XImpredicativeTypes` in the LANGUAGE extensions or cabal file. So I'm confused. What's the problem here? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by basvandijk): I think I was confused. The problem is not in `monad-control` but in `lifted-base` (which depends on `monad-control`). If I remove the `{-# LANGUAGE ImpredicativeTypes #-}` from `Control.Exception.Lifted` I get the following error on [https://github.com/basvandijk/lifted- base/blob/master/Control/Exception/Lifted.hs#L268 mask]: {{{ Control/Exception/Lifted.hs:268:8: Cannot instantiate unification variable ‘a2’ with a type involving foralls: (forall a. m a -> m a) -> m b Perhaps you want ImpredicativeTypes In the expression: liftBaseOp E.mask . liftRestore In an equation for ‘mask’: mask = liftBaseOp E.mask . liftRestore }}} Is this easy solvable (preferably without changing the API)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): I'd eta-expand `mask`. Using `(.)` on higher rank types ''does'' require impredicativity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9569: Tuple constraints don't work right -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: Test Case: | polykinds/T9569, | typecheck/should_compile/T9569a | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by basvandijk): Thanks for the advice. I'm now using: {{{ mask :: MonadBaseControl IO m => ((forall a. m a -> m a) -> m b) -> m b mask f = control $ \runInBase -> E.mask $ \g -> runInBase $ f $ liftBaseOp_ g }}} without using `ImpredicativeTypes`. @luite I will make a point release of `lifted-base` with this fix. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9569#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC