Odd pattern synonym type errors

Suppose we have

newtype Arrange = Arrange {getArrange :: [Int] -> [Int]}

If I write

pattern Heh :: (c ~ ((~) Int)) => (forall a. c a => [a] -> [a]) -> Arrange
pattern Heh f <- Arrange f

I get

    • Couldn't match type ‘[Int] -> [Int]’
                     with ‘forall a. Int ~ a => [a] -> [a]’
      Expected type: forall a. c a => [a] -> [a]
        Actual type: [Int] -> [Int]
    • In the declaration for pattern synonym ‘Heh’

It surprises me that these don't match. I can hack around that a bit:

newtype Help = Help {getHelp :: forall a. Int ~ a => [a] -> [a]}

pattern Heh :: (c ~ ((~) Int)) => (forall a. c a => [a] -> [a]) -> Arrange
pattern Heh f <- ((\x -> Help (getArrange x)) -> Help f)

Now this compiles, and I can use it in a variety of ways, but not quite all. If I write

pattern Heh' :: ([Int] -> [Int]) -> Arrange
pattern Heh' f <- Heh f

I get

Haha.hs:78:23: error:
    • Couldn't match expected type ‘[Int] -> [Int]’
                  with actual type ‘forall a. Int ~ a => [a] -> [a]’
    • In the declaration for pattern synonym ‘Heh'’
   |
78 | pattern Heh' f <- Heh f
   |                       ^

This strikes me as perhaps even more surprising. I can hack around that too, of course, but yuck!

pattern Heh' :: ([Int] -> [Int]) -> Arrange
pattern Heh' f <- ((\(Heh g) -> g @ Int) -> f)

Trac metadata

Trac field	Value
Version	8.2.1-rc2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture