#7220 closed bug (fixed)

Confusing error message in type checking related to type family, fundep, and higher-rank type

Reported by: tsuyoshi Owned by: simonpj
Priority: normal Milestone: 7.8.1
Component: Compiler (Type checker) Version: 7.6.1-rc1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: typecheck/should_fail/T7220 Blocked By:
Blocking: Related Tickets:

Description

(This is related to, but different from, the message which I posted to glasgow-haskell-users mailing list: http://www.haskell.org/pipermail/glasgow-haskell-users/2012-September/022815.html.)

GHC 7.6.1-rc1 (7.6.0.20120810; 64-bit Windows) rejects the attached code (Test2.hs) with the following error message:

Test2.hs:24:52:
    Couldn't match expected type `Y'
                with actual type `TF (forall b. (C A b, TF b ~ Y) => b)'
    In the first argument of `f ::
                                (forall b. (C A b, TF b ~ Y) => b) -> X', namely
      `u'
    In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
    In an equation for `v':
        v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u

I am not sure whether the code is supposed to be accepted or rejected, but even if it is correct to reject the code, this error message does not look right to me. If I am not mistaken, the error message is saying that the type checker expects the argument of (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) to have type Y, but I cannot think of any reason why it should relate the type (forall b. (C A b, TF b ~ Y) => b) with Y.

The same code is available also at https://gist.github.com/3606856.

Attachments (1)

Test2.hs (1.4 KB) - added by tsuyoshi 20 months ago.

Download all attachments as: .zip

Change History (4)

Changed 20 months ago by tsuyoshi

comment:1 Changed 20 months ago by tsuyoshi

When I posted this report, I had been overlooking TF in the “actual type” part of the error message. Now the error message at least makes some sense.

(Although I do not fully understand why the code is rejected in the first place, I think that I have to understand the algorithm used by the type checker to understand this.)

I am not sure whether this bug report still makes sense or not. If not, please close it. Sorry about this.

comment:2 Changed 18 months ago by igloo

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

Simon, could you take a look at this please?

comment:3 Changed 18 months ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to typecheck/should_fail/T7220

"I cannot think of any reason why it should relate the type (forall b. (C A b, TF b ~ Y) => b) with Y". Here's why:

u :: (C A b, TF b ~ Y) => b
u = undefined

v :: X
v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u 
  • GHC instanatiates the occurence of u, given type just beta, where beta is a fresh unification variable. Plus constraints (C A beta, TF beta ~ Y).
  • Now it tries to unify beta with the expected arugment type of the (f :: sig) expression. This argument type is (forall b. (C A b, TF b ~ Y) => b)
  • So GHC (until today) would unify beta := forall b. (C A b, TF b ~ Y) => b.
  • So the constraint (TF beta ~ Y) turns into (TF (forall b. (C A b, TF b ~ Y) => b) ~ Y)`, and that's the error you saw.

But really GHC should not have taken the third step above (at least not without -XImpredicativeTypes). With the patch that fixes #6069 and #7264 it no longer does so, yielding instead

T7220.hs:24:6:
    Cannot instantiate unification variable `b0'
    with a type involving foralls: forall b. (C A b, TF b ~ Y) => b
      Perhaps you want -XImpredicativeTypes
    In the expression: f :: (forall b. (C A b, TF b ~ Y) => b) -> X
    In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u
    In an equation for `v':
        v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u

which isn't fantastic but is perhaps less confusing than before.

Note: See TracTickets for help on using tickets.