Impredicative instantiation of universally quantified variables in guarded positions fails in pattern synonyms
Consider the following declarations:
data T a b where
Blah :: forall a b. a -> b -> T a b
mustWork1 :: T (forall a. a -> a) Int -> Int
mustWork1 (Blah f x) = f x
mustWork1
works as it should. Unfortunately this isn't the case for mustWork2
.
pattern BlahSyn :: forall a b. () => () => a -> b -> T a b
pattern BlahSyn f x = Blah f x
mustWork2 :: T (forall a. a -> a) Int -> Int
mustWork2 (BlahSyn f x) = f x
Here is the error message for mustWork2
:
/Users/artin/Programming/projects/playground/src/Synonym.hs:123:12-22: error: [GHC-83865]
• Couldn't match type: forall a. a -> a
with: Int -> Int
Expected: T (forall a. a -> a) Int
Actual: T (Int -> Int) Int
• In the pattern: BlahSyn f x
In an equation for ‘mustWork2’: mustWork2 (BlahSyn f x) = f x
|
123 | mustWork2 (BlahSyn f x) = f x
| ^^^^^^^^^^^
Failed, no modules to be reloaded.