#7268 closed bug (fixed)

Explicit type signatures for top level record pattern matches polymorphism fail

Reported by: TristanAllwood Owned by:
Priority: normal Milestone: 7.8.1
Component: Compiler (Type checker) Version: 7.4.1
Keywords: Cc: martijn@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Difficulty: Unknown
Test Case: typecheck/should_compile/T7268 Blocked By:
Blocking: Related Tickets:

Description

Consider the following module, which declares a record with two fields (X), an instance of this record (x), and then (at the top level) pattern matches the fields of x to create two new functions.

{-# LANGUAGE RankNTypes #-}
module Foo where

data X
  = X { a :: forall a . a -> a , b :: Int -> Int }

x :: X
x = X { a = id, b = succ }

succ' :: Int -> Int

X { a = id', b = succ' } = x

If we ask ghci what the type of id' is, we get told:

:t id'
id' :: a -> a

However adding this type explicitly, gives the following:

Foo.hs:15:9:
    Couldn't match expected type `forall a. a -> a'
                with actual type `a -> a'
    In the pattern: X {a = id', b = succ'}
    In a pattern binding: X {a = id', b = succ'} = x
Failed, modules loaded: none.

This can happen in practice when using (e.g.) Parsec's TokenParser?.

Change History (7)

comment:1 Changed 12 months ago by igloo

  • Difficulty set to Unknown
  • Milestone set to 7.8.1
  • Owner set to simonpj

Thanks for the report. Simon, could you take a look at what the expected behaviour is here, please?

comment:2 Changed 11 months ago by MartijnVanSteenbergen

  • Cc martijn@… added

Some more info and examples can be found in #7891.

Notably, for the program above, an extra indirection makes it ok again to give a type signature:

id'' :: a -> a
id'' = id'

comment:3 Changed 11 months ago by simonpj@…

commit 0452021e726ab44f3866faacf7817ac116bb58db

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed May 15 10:15:47 2013 +0100

    Fix typechecking of pattern bindings that have type signatures (Trac #7268)
    
    Pattern bindings are jolly tricky to typecheck, especially if there are
    also type signatures involved.  Trac #7268 pointed out that I'd got it
    wrong; this fixes it.  See Note [Typing patterns in pattern bindings] in TcPat.

 compiler/typecheck/TcBinds.lhs |   21 ++++------
 compiler/typecheck/TcPat.lhs   |   81 +++++++++++++++++++++------------------
 2 files changed, 52 insertions(+), 50 deletions(-)

comment:4 Changed 11 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to typecheck/should_compile/T7268

Excellent point thank you. Pattern bindings are devilish tricky. Fixed now. I added a regression test for #7891 as well.

Simon

comment:5 Changed 11 months ago by MartijnVanSteenbergen

I'm really happy with this fix, thank you very much!

comment:6 Changed 11 months ago by MartijnVanSteenbergen

  • Owner simonpj deleted
  • Resolution fixed deleted
  • Status changed from closed to new

Hi Simon, looking at testcase T7891, wouldn't it be better to uncomment line 12 so that it becomes an actual regression test?

comment:7 Changed 11 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed

I'm glad it's helpful. Thanks for pointing out the bug in the regression test...I've just pushed a fix.

Simon

Note: See TracTickets for help on using tickets.