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