[GHC] #15416: Higher rank types in pattern synonyms
#15416: Higher rank types in pattern synonyms -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 (Type checker) | Keywords: | Operating System: Unknown/Multiple PatternSynonyms | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE RankNTypes, PatternSynonyms, ViewPatterns #-} }}} Consider the following two pattern synonyms: {{{#!hs pattern N :: () => () => forall r. r -> (a -> r) -> r pattern N <- ((\f -> f Nothing Just) -> Nothing) where N = \n j -> n pattern J :: a -> forall r. r -> (a -> r) -> r pattern J x <- ((\f -> f Nothing Just) -> Just x) where J x = \n j -> j x }}} The pattern synonym type declaration syntax is very fragile and awkward wrt quantifiers but that's a story for another ticket. Now consider four ways to write the same function: using pattern synonyms we've defined above vs. using the exact view patterns they were defiend with; and using a series of equations vs. an explicit `case of`: {{{#!hs fooVPEqns, fooVPCase, fooPSEqns, fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a fooVPEqns ((\f -> f Nothing Just) -> Nothing) = Nothing fooVPEqns ((\f -> f Nothing Just) -> Just x) = Just x fooVPCase v = case v of ((\f -> f Nothing Just) -> Nothing) -> Nothing ((\f -> f Nothing Just) -> Just x) -> Just x fooPSEqns N = Nothing fooPSEqns (J x) = Just x fooPSCase v = case v of N -> Nothing J x -> Just x }}} Three of these compile and work fine, the fourth breaks: {{{#!hs QuantPatSyn.hs:22:9: error: • Couldn't match expected type ‘r0 -> (a -> r0) -> r0’ with actual type ‘forall r. r -> (a0 -> r) -> r’ • In the pattern: N In a case alternative: N -> Nothing In the expression: case v of N -> Nothing J x -> Just x • Relevant bindings include v :: forall r. r -> (a -> r) -> r (bound at QuantPatSyn.hs:21:11) fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a (bound at QuantPatSyn.hs:21:1) | 22 | N -> Nothing | ^ QuantPatSyn.hs:23:9: error: • Couldn't match expected type ‘r0 -> (a -> r0) -> r0’ with actual type ‘forall r. r -> (a -> r) -> r’ • In the pattern: J x In a case alternative: J x -> Just x In the expression: case v of N -> Nothing J x -> Just x • Relevant bindings include v :: forall r. r -> (a -> r) -> r (bound at QuantPatSyn.hs:21:11) fooPSCase :: (forall r. r -> (a -> r) -> r) -> Maybe a (bound at QuantPatSyn.hs:21:1) | 23 | J x -> Just x | ^^^ }}} The exact wording of the error message (the appearance of `forall` in the "actual type") makes me think this is an error on the typechecker's side: the part of the typechecker that handles pattern synonyms doesn't handle higher rank types correctly. Another symptom can be observed with the following: {{{#!hs pattern V :: Void -> (forall r. r) pattern V x <- ((\f -> f) -> x) where V x = absurd x barVPEqns, barVPCase, barPSEqns, barPSCase :: (forall r. r) -> Void barVPEqns ((\f -> f) -> x) = x barVPCase v = case v of ((\f -> f) -> x) -> x barPSEqns (V x) = x barPSCase v = case v of V x -> x }}} {{{#!hs QuantPatSyn.hs:43:9: error: • Cannot instantiate unification variable ‘r0’ with a type involving foralls: forall r. r GHC doesn't yet support impredicative polymorphism • In the pattern: V x In a case alternative: V x -> x In the expression: case v of { V x -> x } | 43 | V x -> x | ^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15416 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15416: Higher rank types in pattern synonyms -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): You are treading on thin ice. Consider this {{{ f1 :: (forall a. a->a) -> Int f1 (x :: forall b. b->b) = x 3 f2 :: (forall a. a->a) -> Int f2 x = case x of (y :: forall b. b->b) -> y 3 }}} You might expect `f1` and `f2` to behave the same, because `f2` only replaces inline pattern matching with a case-expression. But `f1` as accepted and `f2` is rejected thus {{{ * Couldn't match expected type `a0 -> a0' with actual type `forall b. b -> b' * When checking that the pattern signature: forall b. b -> b fits the type of its context: a0 -> a0 In the pattern: y :: forall b. b -> b In a case alternative: (y :: forall b. b -> b) -> y 3 | 10 | (y :: forall b. b->b) -> y 3 }}} Very similar to the failure you see. Why? * In `f1` the higher-rank type inference machinery "pushes down" the type of the argument, from `f1`'s type signature, into the pattern `(x :: forall b. b->b)`. * But in `f2`, the variable `x` indeed gets type `forall b. b->b` (via this same push-down mechanism, but then ''that type gets instantiated at the call site of `x`''. So the scrutinee of the `case` has type `alpha -> alpha`, for some as-yet-unknown type `alpha`. And that, of course, is not polymorphic enough. * The type inference engine never generalises the scrutinee of a `case`. (I suppose one could revisit that, though I do not know how.) I hope that explains why your fourth example breaks. When we first did pattern synonyms I expected the types to always be of form {{{ K :: t1 -> ... -> tn -> T s1 .. sm }}} where `T` is a data type. We loosened that up a bit to allow arbitrary return types. (I forget what the motivation was; I wonder if anyone else remembers? There may be a ticket.) What you are doing is putting a `forall` in that return position. I never considered that! It would be interesting to see a compelling motivation for doing this. Eg why don't you say this? {{{ pattern N :: forall a r. () => () => r -> (a -> r) -> r pattern J :: forall a r. a -> r -> (a -> r) -> r }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15416#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15416: Higher rank types in pattern synonyms -------------------------------------+------------------------------------- Reporter: mniip | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mniip): Replying to [comment:1 simonpj]:
You are treading on thin ice. Consider this {{{ f1 :: (forall a. a->a) -> Int f1 (x :: forall b. b->b) = x 3
f2 :: (forall a. a->a) -> Int f2 x = case x of (y :: forall b. b->b) -> y 3 }}} You might expect `f1` and `f2` to behave the same, because `f2` only
inline pattern matching with a case-expression.
But `f1` as accepted and `f2` is rejected thus {{{ * Couldn't match expected type `a0 -> a0' with actual type `forall b. b -> b' * When checking that the pattern signature: forall b. b -> b fits the type of its context: a0 -> a0 In the pattern: y :: forall b. b -> b In a case alternative: (y :: forall b. b -> b) -> y 3 | 10 | (y :: forall b. b->b) -> y 3 }}} Very similar to the failure you see. Why?
* In `f1` the higher-rank type inference machinery "pushes down" the type of the argument, from `f1`'s type signature, into the pattern `(x :: forall b. b->b)`.
* But in `f2`, the variable `x` indeed gets type `forall b. b->b` (via
replaces this same push-down mechanism, but then ''that type gets instantiated at the call site of `x`''. So the scrutinee of the `case` has type `alpha -> alpha`, for some as-yet-unknown type `alpha`.
And that, of course, is not polymorphic enough.
Wouldn't `alpha` be a unification variable in this case and therefore be polymorphic just enough?
* The type inference engine never generalises the scrutinee of a `case`. (I suppose one could revisit that, though I do not know how.)
I hope that explains why your fourth example breaks.
When we first did pattern synonyms I expected the types to always be of
Consider if desugaring came before typechecking. This wouldn't be a problem because this isn't a case-of in the Core sense. Can't say I have a solution but maybe it's worth taking a look at typechecking a ''haskell'' case-of based on what ''Core'' constructs it desugars into? form
{{{ K :: t1 -> ... -> tn -> T s1 .. sm }}}
where `T` is a data type. We loosened that up a bit to allow arbitrary return types. (I forget what the motivation was; I wonder if anyone else remembers? There may be a ticket.)
That does indeed explain the extreme awkwardness of the current syntax. The part where `P => Q => A -> B -> C` bizzarely stands for `P => ((Q *> (A, B)) <-> C)`.
What you are doing is putting a `forall` in that return position. I never considered that! It would be interesting to see a compelling motivation for doing this. Eg why don't you say this? {{{ pattern N :: forall a r. () => () => r -> (a -> r) -> r pattern J :: forall a r. a -> r -> (a -> r) -> r }}}
Because then reversing the equations gets you `forall a r` I can match on a scrutinee of type `r -> (a -> r) -> r` and bind a variable of type `a`. This is clearly not what we want here (`r` is rigid, but we demand `r ~ Maybe`), and the definition of `J` doens't typecheck under that signature. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15416#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC