#11667 closed bug (fixed)

Incorrect pattern synonym types in error messages

Reported by: rdragon Owned by: rdragon
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 8.0.1-rc2
Keywords: PatternSynonyms Cc: simonpj, mpickering
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #11213 Differential Rev(s): Phab:D1967
Wiki Page:

Description

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 Phab: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

Change History (5)

comment:1 Changed 12 months ago by bgamari

Milestone: 8.0.2

There is a detailed comment describing the errors before and after rdragon's proposed solution on Phab:D1967.

comment:2 Changed 11 months ago by Ben Gamari <ben@…>

In 997312b/ghc:

Add `PatSynSigSkol` and modify `PatSynCtxt`

As the type of a pattern synonym cannot in general be represented by a
value of type Type, we cannot use a value `SigSkol (PatSynCtxt n) (Check
ty)` to represent the signature of a pattern synonym (this causes
incorrect signatures to be printed in error messages). Therefore we now
represent it by a value `PatSynSigSkol n` (instead of incorrect
signatures we simply print no explicit signature).

Furthermore, we rename `PatSynCtxt` to `PatSynBuilderCtxt`, and use
`SigSkol (PatSynBuilderCtxt n) (Check ty)` to represent the type of a
bidirectional pattern synonym when used in an expression context.
Before, this type was represented by a value `SigSkol (PatSynCtxt n)
(Check ty)`, which caused incorrect error messages.

Also, in `mk_dict_err` of `typecheck\TcErrors.hs` we now distinguish
between all enclosing implications and "useful" enclosing implications,
for better error messages concerning pattern synonyms. See `Note [Useful
implications]`.

See the Phabricator page for examples.

Reviewers: mpickering, goldfire, simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1967

GHC Trac Issues: #11667

comment:3 Changed 11 months ago by bgamari

Milestone: 8.0.28.0.1
Status: newmerge

comment:4 Changed 11 months ago by bgamari

comment:5 Changed 11 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.