[GHC] #13735: RankNTypes don't work with PatternSynonyms
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple PatternSynonyms | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs data PLambda a = Var a | Int Int | Bool Bool | If (PLambda a) (PLambda a) (PLambda a) | Add (PLambda a) (PLambda a) | Mult (PLambda a) (PLambda a) | Eq (PLambda a) (PLambda a) | Lam (a -> PLambda a) | App (PLambda a) (PLambda a) newtype Lam = L { un :: forall a. PLambda a } }}} {{{#!hs llam :: (forall a. a -> PLambda a) -> Lam llam f = L (Lam f) }}} works fine, but does not with pattern synonyms: {{{ -- $ ghci -ignore-dot-ghci tirr.hs -- GHCi, version 8.2.0.20170507: http://www.haskell.org/ghc/ :? for help -- [1 of 1] Compiling Main ( tirr.hs, interpreted ) -- -- tirr.hs:20:25: error: -- • Couldn't match expected type ‘forall a. a -> PLambda a’ -- with actual type ‘a0 -> PLambda a0’ -- • In the declaration for pattern synonym ‘LLam’ -- • Relevant bindings include -- a :: a0 -> PLambda a0 (bound at tirr.hs:20:25) -- | -- 20 | pattern LLam a = L (Lam a) -- | ^ -- Failed, modules loaded: none. -- Prelude> pattern LLam :: (forall a. a -> PLambda a) -> Lam pattern LLam a = L (Lam a) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Another infelicity of the interaction between `PatternSynonyms` and `RankNTypes` is that this unidirectional version typechecks: {{{#!hs {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} module Bug where data PLambda a = Var a | Int Int | Bool Bool | If (PLambda a) (PLambda a) (PLambda a) | Add (PLambda a) (PLambda a) | Mult (PLambda a) (PLambda a) | Eq (PLambda a) (PLambda a) | Lam (a -> PLambda a) | App (PLambda a) (PLambda a) newtype Lam = L { un :: forall a. PLambda a } pattern LLam a <- L (Lam a) }}} And this is what GHCi says about the inferred type of `LLam`: {{{ GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Ok, modules loaded: Bug. λ> :i LLam pattern LLam :: (a -> PLambda a) -> Lam -- Defined at Bug.hs:13:1 }}} But this does not work in an expression context: {{{#!hs {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} module Bug where data PLambda a = Var a | Int Int | Bool Bool | If (PLambda a) (PLambda a) (PLambda a) | Add (PLambda a) (PLambda a) | Mult (PLambda a) (PLambda a) | Eq (PLambda a) (PLambda a) | Lam (a -> PLambda a) | App (PLambda a) (PLambda a) newtype Lam = L { un :: forall a. PLambda a } llam f = L (Lam f) }}} {{{ GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:13:17: error: • Couldn't match expected type ‘a -> PLambda a’ with actual type ‘p’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by a type expected by the context: forall a. PLambda a at Bug.hs:13:10-18 • In the first argument of ‘Lam’, namely ‘f’ In the first argument of ‘L’, namely ‘(Lam f)’ In the expression: L (Lam f) • Relevant bindings include f :: p (bound at Bug.hs:13:6) llam :: p -> Lam (bound at Bug.hs:13:1) | 13 | llam f = L (Lam f) | ^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -18,1 +18,1 @@ - {{{ + {{{#!hs New description: {{{#!hs data PLambda a = Var a | Int Int | Bool Bool | If (PLambda a) (PLambda a) (PLambda a) | Add (PLambda a) (PLambda a) | Mult (PLambda a) (PLambda a) | Eq (PLambda a) (PLambda a) | Lam (a -> PLambda a) | App (PLambda a) (PLambda a) newtype Lam = L { un :: forall a. PLambda a } }}} {{{#!hs llam :: (forall a. a -> PLambda a) -> Lam llam f = L (Lam f) }}} works fine, but does not with pattern synonyms: {{{#!hs -- $ ghci -ignore-dot-ghci tirr.hs -- GHCi, version 8.2.0.20170507: http://www.haskell.org/ghc/ :? for help -- [1 of 1] Compiling Main ( tirr.hs, interpreted ) -- -- tirr.hs:20:25: error: -- • Couldn't match expected type ‘forall a. a -> PLambda a’ -- with actual type ‘a0 -> PLambda a0’ -- • In the declaration for pattern synonym ‘LLam’ -- • Relevant bindings include -- a :: a0 -> PLambda a0 (bound at tirr.hs:20:25) -- | -- 20 | pattern LLam a = L (Lam a) -- | ^ -- Failed, modules loaded: none. -- Prelude> pattern LLam :: (forall a. a -> PLambda a) -> Lam pattern LLam a = L (Lam a) }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Re comment:1, it's unsurprising that {{{ llam f = L (Lam f) }}} with no type signature, does not work. Because `f` needs to have a polytype, and it won't without a type sig. But re the original Description, I agree that the bidirectional definition should go through. I'll take a look. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment:
But re the original Description, I agree that the bidirectional definition should go through
I was wrong. Actually what is happening is quite reasonable. GHC is rejecting a unidirectional pattern with a signature (bidirectional is red herring): {{{ pattern LLam :: (forall a. a -> PLambda a) -> Lam pattern LLam x <- L (Lam x) }}} Why rejected? Well, if `LLam` had the type claimed by the signature, this would be ok {{{ f1 (LLam x) = (x 'c', x True) }}} since `x :: forall a. a -> PLambda a`. But if you expand the syononym, thus {{{ f2 (L (Lam x)) = (x 'c', x True) }}} it's clear that `f2` should be rejected. (And it is; try it.) If you doubt that it should be, try to desugar it: {{{ f2 = \(v:Lam). case v of L (w :: forall b. PLambda b) -> case (w @ty) of Lam (x :: ty -> PLambda ty) -> (x 'c', x True) }}} We pattern match on `f2`'s argument to extract a polymorphic `w`. Then we must apply `w` to some type `ty` before we can do any more; but now the `x` we get from pattern matching is not polymorphic. Conclusion: it's working fine. I'll close, but re-open if you disagree -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): There is where my intuition breaks down. Writing this works, so higher- rank types + pattern synonyms are fine {{{#!hs newtype A = A (forall xx. xx -> xx) pattern PatA :: (forall xx. xx -> xx) -> A pattern PatA a = A a a :: A -> A a (PatA f) = A f }}} but I don't understand why this is different {{{#!hs newtype Endo a = Endo (a -> a) newtype B = B (forall xx. Endo xx) pattern PatB :: (a -> a) -> PatB pattern PatB f <- B (Endo f) b :: B -> forall xx. xx -> xx b (B (Endo f)) = f }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): It's quite different! As I suggest above, try writing it without the pattern synonym! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Ah what confused me was that they both (''seemingly'') allow extracting a polymorphic function {{{#!hs type Id = forall xx. xx -> xx one :: A -> Id one (A f) = f two :: B -> Id two (B (Endo f)) = f }}} But this doesn't work: (like your `f2 (L (Lam x)) = (x 'c', x True)` example demonstrates) {{{#!hs -- works einn :: A -> (Int -> Int, () -> ()) einn (A f) = (f, f) -- fails tveir :: B -> (Int -> Int, () -> ()) tveir (B (Endo f)) = (f, f) }}} With your desugaring and #11350 {{{#!hs A (\@x -> id @x) B (\@x -> Endo @x (id @x)) }}} it becomes clearer to me. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): A coworker at work helped me reach this {{{#!hs newtype A = A (forall xx. xx -> xx) newtype Endo a = Endo { appEndo :: a -> a } newtype B = B (forall xx. Endo xx) pattern PatB :: (forall xx. xx -> xx) -> B pattern PatB f <- ((\(B f) -> A (appEndo f)) -> A f) where PatB f = B (Endo f) }}} which works, similarly with `PLambda` {{{#!hs data PLambda a = Lam { unLam :: a -> PLambda a } | ... newtype LAM = LAM (forall xx. xx -> PLambda xx) newtype Lam = L (forall a. PLambda a) get :: Lam -> LAM get (L f) = LAM (unLam f) pattern LLAM :: (forall a. a -> PLambda a) -> Lam pattern LLAM f <- (get -> LAM f) where LLAM f = L (Lam f) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Your `get` is partial, so matching on `LLAM` will throw an exception (instead of failing) when it doesn't match. It's possible to accomplish your purpose thus: {{{#!hs data Yeah = Yeah (forall a. a -> PLambda a) | Nah getYeah :: Lam -> Yeah getYeah l@(L (Lam _)) = Yeah (case l of L (Lam f) -> f; _ -> error "impossible") getYeah _ = Nah pattern LLam :: (forall a. a -> PLambda a) -> Lam pattern LLam x <- (getYeah -> Yeah x) }}} It's pretty ugly, though. You have to first pattern match to determine that the constructor is `Lam`, then pattern match on the same value again under the `Yeah` constructor to capture the polymorphism. If there's a way to avoid that, I don't see it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I think what you'd really want would be to have something like {{{#!hs data PLambda' = Var' (forall a. a) | ... | Lam' (forall a. a -> PLambda a) | ... }}} and then have some non-disgusting way to produce a function {{{#!hs convert :: Lam -> PLambda' }}} As I said, though, I don't see a nice way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): `f (B endo) = A (appEndo endo)` works while this doesn't {{{#!hs f :: B -> A f (B (appEndo -> f)) = A f }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:12 Iceland_jack]:
`f (B endo) = A (appEndo endo)` works while this doesn't
{{{#!hs f :: B -> A f (B (appEndo -> f)) = A f }}}
That's not surprising. We don't have impredicative types, so `appEndo x` always produces a monomorphic result. You have to unpack the `Endo` under the `A` constructor. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13735: RankNTypes don't work with PatternSynonyms -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: invalid | Keywords: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Very cool -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13735#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC