## Incorrect pattern synonym types in error messages

Here are some examples of incorrect pattern synonym types in error messages.

- *Example 1**

```
{-# LANGUAGE PatternSynonyms #-}
module Mod1 where
pattern Pat :: Eq a => Maybe a
pattern Pat <- Just 42
```

This gives the error (note the missing `Eq a =>`

):

```
Mod1.hs:4:21: error:
* Could not deduce (Num a) arising from the literal `42'
from the context: Eq a
bound by the type signature for pattern synonym `Pat':
Maybe a
at Mod1.hs:4:9-11
Possible fix:
add (Num a) to the context of
the type signature for pattern synonym `Pat':
Maybe a
* In the pattern: 42
In the pattern: Just 42
In the declaration for pattern synonym `Pat'
```

- *Example 2**

```
{-# LANGUAGE PatternSynonyms, GADTs #-}
module Mod1 where
data T where MkT :: a -> T
pattern Pat :: () => b ~ Bool => a -> b -> (b, T)
pattern Pat x y = (y, MkT x)
```

We get the error (note the missing contexts and the incorrect quantification `forall b`

, missing `a`

):

```
Mod1.hs:6:27: error:
* Couldn't match type `b' with `Bool'
arising from the "provided" constraints claimed by
the signature of `Pat'
`b' is a rigid type variable bound by
the type signature for pattern synonym `Pat':
forall b. a -> b -> (b, T)
at Mod1.hs:5:16
* In the declaration for pattern synonym `Pat'
* Relevant bindings include y :: b (bound at Mod1.hs:6:20)
```

- *Example 3**

```
{-# LANGUAGE PatternSynonyms #-}
module Mod1 where
pattern Pat :: Eq a => Show a => a -> Maybe a
pattern Pat x <- Just x
```

We get the error:

```
Mod1.hs:4:23: error:
* Could not deduce (Show a)
arising from the "provided" constraints claimed by
the signature of `Pat'
from the context: Eq a
bound by the type signature for pattern synonym `Pat':
a -> Maybe a
at Mod1.hs:4:9-11
* In the declaration for pattern synonym `Pat'
```

Here we could perhaps remove the whole "from the context ... at Mod1.hs:4:9-11" part, as it doesn't make much sense to tell the user that we could not deduce a "provided" constraint from the "required" context.

- *Example 4**

```
{-# LANGUAGE PatternSynonyms, GADTs #-}
module Mod1 where
data T a where MkT :: (Num a, Show a) => a -> T a
pattern Pat :: (Eq a) => (Show a) => T a
pattern Pat = MkT 42
```

This gives the error (note that the signature in the error is of the pattern synonym `Pat`

when used in an expression context):

```
Mod1.hs:6:15: error:
* Could not deduce (Num a) arising from a use of `MkT'
from the context: (Eq a, Show a)
bound by the type signature for pattern synonym `Pat':
(Eq a, Show a) => T a
at Mod1.hs:6:1-20
Possible fix:
add (Num a) to the context of
the type signature for pattern synonym `Pat':
(Eq a, Show a) => T a
* In the expression: MkT 42
In an equation for `$bPat': $bPat = MkT 42
```

The problems in these four examples are caused by the use of `SigSkol (PatSynCtxt n) (Check ty)`

for representing pattern synonym types (and the types of bidirectional pattern synonyms when used in an expression context).

A possible solution can be found in D1967.

Simon notes the following:

Example 3 raises an interesting point we can debate once we have a ticket. Namely, is this ok?

`pattern Pat :: Ix a => Ix a => a -> Maybe a pattern Pat x <- Just x`

## Trac metadata

Trac field | Value |
---|---|

Version | 8.0.1-rc2 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | mpickering, simonpj |

Operating system | |

Architecture |