Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#12557 closed bug (invalid)

Regression in type inference with RankNTypes

Reported by: slindley Owned by:
Priority: low Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: ImpredicativeTypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by slindley)

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)

Change History (5)

comment:1 Changed 3 years ago by thomie

Description: modified (diff)
Keywords: ImpredicativeTypes added
Priority: highlow
Summary: Regression in type inference with RankNTypesRegression in type inference with ImpredicativeTypes

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.

comment:2 Changed 3 years ago by simonpj

Resolution: invalid
Status: newclosed

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!

comment:3 Changed 3 years ago by slindley

Description: modified (diff)
Summary: Regression in type inference with ImpredicativeTypesRegression in type inference with RankNTypes

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.

comment:4 Changed 3 years ago by slindley

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.

comment:5 Changed 3 years ago by goldfire

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

Note: See TracTickets for help on using tickets.