Opened 12 years ago

Last modified 2 years ago

#1330 new bug

Impredicativity bug: Church2 test gives a rather confusing error with the HEAD

Reported by: igloo Owned by: simonpj
Priority: lowest Milestone:
Component: Compiler (Type checker) Version: 6.7
Keywords: TypeErrorMessages, ImpredicativeTypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: Church2
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The Church2 test gives a rather confusing error with the HEAD:

Church2.hs:27:14:
    Couldn't match expected type `CNat'
           against inferred type `(a -> a) -> a -> a'
      Expected type: CNat -> CNat
      Inferred type: CNat -> CNat
    In the first argument of `n', namely `(mul m)'
    In the expression: n (mul m) n1

In particular the lines

      Expected type: CNat -> CNat
      Inferred type: CNat -> CNat

are confusing, and I'm not sure why it's giving two expected/inferred pairs of types.

Change History (22)

comment:1 Changed 12 years ago by simonpj

Sigh. This a great example of why typechecking for impredicative polymorphism is so darn tricky. Here is what is happening. The call n (mul m) n1 means that we try to check (mul m) expecting it to have type CNat -> CNat. Not knowing (yet) what type to instantiate mul to, we instantiate it to type box(a). So now we are faced with the task of checking

  box(a) -> box(a)  <=  CNat -> CNat

If you follow through the rules of Fig 3 ofthe paper, we find that, from the argument side of the arrows we must equate box(a) and CNat. That leaves us with the following problem:

  box(CNat) -> box(CNat)   <=   CNat -> CNat

Looking now at the resultside of the arrow we get

  box(CNat)   <=   CNat

You might think that this is obviously possible, but rule SKOL says to instantiate the CNat onn the right; and that soon leads the reported mis-match.

The trouble is that GHC does as much zonking as possible before reporting the error, and does not show the boxes. Result: we display two identical-looking types.

I'm not sure how to fix this, and in any case I'm unhappy with the impredicative-polymoprhism story. So I'm going to leave this as one more reason why the current story is unsatisfactory, and hope that Stephanie and Dimitrios eventually show the way forward!

Meanwhile, better make this an expected failure.

Simon

comment:2 Changed 12 years ago by igloo

Owner: set to simonpj

comment:3 Changed 12 years ago by simonpj

Summary: Church2 test gives a rather confusing error with the HEADImpredicativity bug: Church2 test gives a rather confusing error with the HEAD

comment:4 Changed 12 years ago by guest

comment:5 Changed 12 years ago by simonpj

Milestone: 6.8 branch6.10 branch

Again deferring to 6.10 when I hope we'll have sorted out impredicativity.

Simon

comment:6 Changed 11 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:7 Changed 11 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:8 Changed 10 years ago by igloo

Milestone: 6.10 branch6.12 branch

comment:9 Changed 9 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:10 Changed 9 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:11 Changed 9 years ago by igloo

Milestone: 7.0.17.0.2

comment:12 Changed 8 years ago by igloo

Milestone: 7.0.27.2.1

comment:13 Changed 8 years ago by igloo

Milestone: 7.2.17.4.1

comment:14 Changed 8 years ago by igloo

Milestone: 7.4.17.6.1
Priority: lowlowest

comment:15 Changed 7 years ago by igloo

Milestone: 7.6.17.6.2

comment:16 Changed 5 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:17 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:18 Changed 5 years ago by thoughtpolice

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:19 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:20 Changed 4 years ago by thomie

Milestone: 8.0.1

comment:21 Changed 2 years ago by simonpj

Keywords: TypeErrorMessages added
Type of failure: None/Unknown

comment:22 Changed 2 years ago by simonpj

Keywords: ImpredicativeTypes added
Note: See TracTickets for help on using tickets.