#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