Opened 2 years ago

Closed 2 years ago

#14160 closed bug (wontfix)

Type inference breaking change in GHC 8.0.2

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: ImpredicativeTypes Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11319 Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

A regression reported by Milewski,

{-# LANGUAGE RankNTypes #-}
module Test where
  
import Data.Profunctor
  
proj :: Profunctor p => forall c. (forall a. p a a) -> p c c
proj e = e

f1 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b 
f1 f e = dimap f id (proj e)

Where these definitions no longer type check

-- • Couldn't match type ‘p c0 c0’ with ‘forall a1. p a1 a1’
--   Expected type: p c0 c0 -> p a a
--     Actual type: (forall a1. p a1 a1) -> p a a
-- • In the second argument of ‘(.)’, namely ‘proj’
--   In the expression: dimap id f . proj
--   In an equation for ‘f2’: f2 f = dimap id f . proj
-- • Relevant bindings include
--     f2 :: (a -> b) -> (forall c. p c c) -> p a b
--       (bound at 24:1)
f2 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b 
f2 f = dimap id f . proj

-- • Cannot instantiate unification variable ‘a0’
--   with a type involving foralls: (forall c. p c c) -> p a b
--     GHC doesn't yet support impredicative polymorphism
-- • In the expression: undefined
--   In an equation for ‘f3’: f3 f = undefined
-- • Relevant bindings include
--     f :: a -> b
--       (bound at 39:4)
--     f3 :: (a -> b) -> (forall c. p c c) -> p a b
--       (bound at 39:1)

f3 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b 
f3 f = undefined -- dimap id f . proj

Change History (6)

comment:1 Changed 2 years ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 2 years ago by RyanGlScott

Keywords: ImpredicativeTypes added

I grant that this breakage is surprising, but it is somewhat expected. The nub of the issue is once again impredicativity.

For the sake of being explicit, here is a version of the above code with no external dependencies (please make an effort to do this in future bug reports - it makes dissecting the problem much easier):

{-# LANGUAGE RankNTypes #-}
module Test where

class Profunctor p where
  dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

proj :: Profunctor p => forall c. (forall a. p a a) -> p c c
proj e = e

f1 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b
f1 f e = dimap f id (proj e)

Now it's worth noting that f2:

f2 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b 
f2 f = dimap id f . proj

Has never typechecked, even on old versions of GHC. The only thing from this program that used to typecheck is f3:

f3 :: Profunctor p => (a -> b) -> (forall c. p c c) -> p a b 
f3 f = undefined

Really, the issue can be condensed down to just this:

{-# LANGUAGE RankNTypes #-}
module Test where

-- Typechecks
f :: (forall a. a) -> b
f x = x

-- Typechecks on GHC 7.10.3, but not later versions
g :: (forall a. a) -> b
g = undefined
$ /opt/ghc/7.10.3/bin/ghci Bug.hs
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Test             ( Bug.hs, interpreted )
Ok, modules loaded: Test.
λ> :q
Leaving GHCi.
$ /opt/ghc/8.0.2/bin/ghci Bug.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Test             ( Bug.hs, interpreted )

Bug.hs:10:5: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving foralls: (forall a. a) -> b
        GHC doesn't yet support impredicative polymorphism
    • In the expression: undefined
      In an equation for ‘g’: g = undefined
    • Relevant bindings include
        g :: (forall a. a) -> b (bound at Bug.hs:10:1)
Failed, modules loaded: none.

The fact that the error message mentions impredicativity should be a solid clue that we're headed into murky territory. The issue is that we're trying to instantiate a type variable with (forall a. a) -> b, which of course is impredicative. GHC 7.10.3 and earlier, for whatever reason, allowed this, but it made type inference much more unpredictable, as noted in https://ghc.haskell.org/trac/ghc/ticket/12749#comment:2. GHC 8.0 prevented this unpredictability by preventing type variables from being instantiated with polytypes, but at the cost of disallowing functions like g.

For what it's worth, I don't think the solution is to re-allow g, but to instead allow a limited form of impredicativity that Simon Peyton Jones suggests in https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html. That is, we would allow writing polytypes in visible type arguments, so this would be permissible:

g :: (forall a. a) -> b
g = undefined @_ @((forall a. a) -> b)

comment:3 Changed 2 years ago by goldfire

Agreed that this is an "improvement" (as in, GHC is behaving closer to spec) from previous behavior.

Yes to allowing polytypes in visible type arguments.

No to accepting g = undefined. It's impredicative! :)

comment:4 Changed 2 years ago by RyanGlScott

In that case, it sounds like this particular bug is resolved as "wontfix".

We don't yet have a ticket for implementing the ability to visibly apply polytypes—should this ticket become that, or should we open a new one?

comment:5 Changed 2 years ago by goldfire

I'd say a new one.

comment:6 Changed 2 years ago by RyanGlScott

Resolution: wontfix
Status: newclosed

I was just about to open a new ticket with a title like "Figure out how to salvage ImpredicativeTypes", but then I discovered #11319, with the very apt title "ImpredicativeTypes even more broken than usual". I think this is a good place for this discussion (especially since it talks about TypeApplications), so I'll move the discussion there.

Note: See TracTickets for help on using tickets.