Regression in type inference with RankNTypes

Consider the following code:

{-# LANGUAGE RankNTypes #-}
module Test where

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

In GHC 7.10.3:

*Main> :t \g -> foo g
\g -> foo g :: ((forall a. f a) -> f r) -> f r

In GHC 8.0.1:

*Main> :t \g -> foo g

<interactive>:1:11: error:
    • Couldn't match expected type ‘(forall a. f a) -> f r’
                  with actual type ‘t’
      ‘t’ is a rigid type variable bound by
        the inferred type of it :: t -> f r at <interactive>:1:1
    • 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 <interactive>:1:2)

changed weight to 7

added Tbug Trac import typechecker labels

changed title from Regression in type inference with RankNTypes to Regression in type inference with ImpredicativeTypes

changed the description

changed weight to 3

Your example relies on -XImpredicativeTypes. Please note that this language extension is entirely unsupported.

That said, you can make you example work by running :set -XImpredicativeTypes on the GHCi prompt.

Trac metadata

Trac field	Value
Priority	high → low

added ImpredicativeTypes label

closed

This is a bug in 7.10.

Basically, a lambda-bound variable like \g above can never get a higher rank type (one involving a forall), unless there is an enclosing type signature so that it's clear at the binding site what its type should be.

I don't know any way to fix this. Do not rely on -XImpredicativeTypes; it is an incomplete, inconsistent and generally broken feature that I should probably remove. I just don't know how to do a better job, sorry!

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

changed title from Regression in type inference with ImpredicativeTypes to Regression in type inference with RankNTypes

changed the description

My example doesn't require -XImpredicativeTypes only -XRankNTypes!

As I understand it the 'bug' in 7.10 was that it did infer polymorphic types for lambda-bound variables even with -XImpredicativeTypes disabled.

It does look like there's a bug in the error message. The message I want to see here is that t must be monomorphic, not that it is rigid.

mentioned in issue #12563 (closed)

Yes, that error message is unfortunate. But I agree with 8.0 that your code should be rejected. I have filed #12563 (closed) requesting an error message improvement.

added Plow label