Opened 3 years ago

Closed 3 years ago

#9954 closed bug (invalid)

Required constraints are not inferred for pattern synonyms involving GADTs

Reported by: cactus Owned by: cactus
Priority: normal Milestone:
Component: Compiler (Type checker) Version:
Keywords: PatternSynonyms Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #9953 Differential Rev(s):
Wiki Page:

Description

Let's say we have the following setup:

{-# LANGUAGE GADTs, PatternSynonyms, ViewPatterns #-}

data T a where
  MkT1 :: a -> T a
  MkT2 :: a -> T (Maybe a)

f :: (Eq a) => a -> a
f = id

Then the following definition works as expected:

pattern P1 x <- MkT1 (f -> x)

with the following inferred type:

λ» :i P1
pattern P1 :: () => Eq t => t -> T t

However, trying to do the same with {{MkT2}} doesn't work:

pattern P2 x <- MkT2 (f -> x)

this results in

Could not deduce (Eq a1) arising from a use of ‘f’
from the context (t ~ Maybe a1)
  bound by a pattern with constructor
             MkT2 :: forall a. a -> T (Maybe a),
           in a pattern synonym declaration

Change History (2)

comment:1 Changed 3 years ago by simonpj

This looks absolutely correct to me. Try it with an ordinary function, without the synonym:

boo :: T a -> Bool
boo (MkT2 (f -> x)) = True

and you get

T9954.hs:12:12:
    Could not deduce (Eq a1) arising from a use of `f'
    from the context a ~ Maybe a1
      bound by a pattern with constructor:
                 MkT2 :: forall a. a -> T (Maybe a),
               in an equation for `boo'
      at T9954.hs:12:6-18
    Possible fix:
      add (Eq a1) to the context of the data constructor `MkT2'
    In the expression: f
    In the pattern: f -> x
    In the pattern: MkT2 (f -> x)

And indeed, from where can we conjure up equality on the existentially-bound type?

So to me this looks like precisely the correct behaviour.

Siimon

comment:2 Changed 3 years ago by simonpj

Resolution: invalid
Status: newclosed
Note: See TracTickets for help on using tickets.