Opened 3 years ago

Closed 17 months ago

#12563 closed bug (fixed)

Bad error message around lack of impredicativity

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T12563
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

(Broken out from #12557.)

Consider

foo :: ((forall a. f a) -> f r) -> f r
foo g = undefined

x = \g -> foo g

Compiling this code produces

Scratch.hs:24:15: error:
    • Couldn't match expected type ‘(forall (a :: k). f a) -> f r’
                  with actual type ‘t’
      ‘t’ is a rigid type variable bound by
        the inferred type of x :: t -> f r at Scratch.hs:24:1-15
    • In the first argument of ‘foo’, namely ‘g’
      In the expression: foo g
      In the expression: \ g -> foo g
    • Relevant bindings include
        g :: t (bound at Scratch.hs:24:6)
        x :: t -> f r (bound at Scratch.hs:24:1)

The code should be rejected. But, really, the problem is that the type of a lambda-bound variable can't be a polytype (unless the type is obvious at the binding site). We should improve this error message.

Change History (3)

comment:1 Changed 17 months ago by RyanGlScott

This appears to be fixed, as of GHC 8.2.2:

$ /opt/ghc/8.2.2/bin/ghci Bug.hs -XRankNTypes
GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:4:15: error:
    • Cannot instantiate unification variable ‘p0’
      with a type involving foralls: (forall a. f0 a) -> f0 r0
        GHC doesn't yet support impredicative polymorphism
    • In the first argument of ‘foo’, namely ‘g’
      In the expression: foo g
      In the expression: \ g -> foo g
    • Relevant bindings include
        g :: p0 (bound at Bug.hs:4:6)
        x :: p0 -> f0 r0 (bound at Bug.hs:4:1)
  |
4 | x = \g -> foo g
  |               ^

I'll add a regression test.

comment:2 Changed 17 months ago by Ryan Scott <ryan.gl.scott@…>

In 819b9cfd/ghc:

Add regression tests for #11515 and #12563

Happily, both of these issues appear to have been fixed in GHC 8.2.
Let's add regression tests for them to ensure that they stay fixed.

comment:3 Changed 17 months ago by RyanGlScott

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T12563
Note: See TracTickets for help on using tickets.