Opened 12 months ago

Closed 4 months ago

#13752 closed bug (fixed)

Odd pattern synonym type errors

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.2.1-rc2
Keywords: PatternSynonyms Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: patsyn/should_compile/T13752, T13752a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Suppose we have

newtype Arrange = Arrange {getArrange :: [Int] -> [Int]}

If I write

pattern Heh :: (c ~ ((~) Int)) => (forall a. c a => [a] -> [a]) -> Arrange
pattern Heh f <- Arrange f

I get

    • Couldn't match type ‘[Int] -> [Int]’
                     with ‘forall a. Int ~ a => [a] -> [a]’
      Expected type: forall a. c a => [a] -> [a]
        Actual type: [Int] -> [Int]
    • In the declaration for pattern synonym ‘Heh’

It surprises me that these don't match. I can hack around that a bit:

newtype Help = Help {getHelp :: forall a. Int ~ a => [a] -> [a]}

pattern Heh :: (c ~ ((~) Int)) => (forall a. c a => [a] -> [a]) -> Arrange
pattern Heh f <- ((\x -> Help (getArrange x)) -> Help f)

Now this compiles, and I can use it in a variety of ways, but not quite all. If I write

pattern Heh' :: ([Int] -> [Int]) -> Arrange
pattern Heh' f <- Heh f

I get

Haha.hs:78:23: error:
    • Couldn't match expected type ‘[Int] -> [Int]’
                  with actual type ‘forall a. Int ~ a => [a] -> [a]’
    • In the declaration for pattern synonym ‘Heh'’
   |
78 | pattern Heh' f <- Heh f
   |                       ^

This strikes me as perhaps even more surprising. I can hack around that too, of course, but yuck!

pattern Heh' :: ([Int] -> [Int]) -> Arrange
pattern Heh' f <- ((\(Heh g) -> g @ Int) -> f)

Change History (5)

comment:1 Changed 12 months ago by Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 12 months ago by Simon Peyton Jones <simonpj@…>

In c997738/ghc:

Pattern synonyms and higher rank types

This patch fixes two separate bugs which contributed to making
Trac #13752 go wrong

1.  We need to use tcSubType, not tcUnify,
    in tcCheckPatSynDecl.tc_arg.

    Reason: Note [Pattern synonyms and higher rank types]

2.  TcUnify.tc_sub_type had a special case designed to improve error
    messages; see Note [Don't skolemise unnecessarily].  But the
    special case was too liberal, and ended up using unification
    (which led to rejecting the program) when it should instead taken
    the normal path (which accepts the program).

    I fixed this by making the test more conservative.

comment:3 Changed 12 months ago by simonpj

Status: newmerge
Test Case: patsyn/should_compile/T13752, T13752a

A bit of a dark corner, but could merge.

comment:4 Changed 12 months ago by dfeuer

Wow, that was fast! Thanks! It may be a dark corner today. However, if my proposal to add type signatures to pattern synonym builders ends up going through with the committee-requested restriction to allow the signatures to vary only in constraints, I think we'll likely see more such code as people hack around the restriction.

comment:5 Changed 4 months ago by bgamari

Resolution: fixed
Status: mergeclosed

This was not merged into 8.2.2.

Note: See TracTickets for help on using tickets.