#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