ImpredicativeTypes type checking fails depending on syntax of arguments

g1 and g2 below type check, but g1', g2', and g2'' don't even though the types are exactly the same.

{-# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #-}
module Test where
f1 :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f1 (Just g) = Just (g [3], g "hello")
f1 Nothing  = Nothing

f2 :: [forall a. [a] -> [a]] -> Maybe ([Int], [Char])
f2 [g] = Just (g [3], g "hello")
f2 []  = Nothing

g1 = (f1 . Just) reverse
g1' = f1 (Just reverse)

g2 = f2 [reverse]
g2' = f2 ((:[]) reverse)
g2'' = f2 (reverse : [])

Compiling it with HEAD gives these errors:

[1 of 1] Compiling Test             ( test.hs, test.o )

test.hs:12:16:
    Couldn't match expected type ‛forall a. [a] -> [a]’
                with actual type ‛[a2] -> [a2]’
    In the first argument of ‛Just’, namely ‛reverse’
    In the first argument of ‛f1’, namely ‛(Just reverse)’

test.hs:15:17:
    Couldn't match expected type ‛forall a. [a] -> [a]’
                with actual type ‛[a0] -> [a0]’
    In the first argument of ‛: []’, namely ‛reverse’
    In the first argument of ‛f2’, namely ‛((: []) reverse)’

test.hs:16:12:
    Couldn't match expected type ‛forall a. [a] -> [a]’
                with actual type ‛[a1] -> [a1]’
    In the first argument of ‛(:)’, namely ‛reverse’
    In the first argument of ‛f2’, namely ‛(reverse : [])’

Trac metadata

Trac field	Value
Version	7.8.1-rc1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

Yes, I'm afraid that ImpredicativeTypes is a non-feature right now. As I wrote to the GHC users list yesterday:

ImpredicativeTypes is not properly finished. When I first implemented it I implemented a fairly ambitious design based on "boxy types" (see paper with that in the title). But it proved unsustainably complicated, both in the implementation and indeed for programmers to reason about which programs should be accepted and which should not.

So I took most of it out. There are some vestiges but to a first approximation it isn't really there at all.

My plan is to do something along the lines of QML (again, look at the paper), plus add explicit type application. But there are always too many other things to do.

This is swampy territory, and I have spent more time on it that I care to tell you without producing a design that I am satisfied with. So while I would be very happy if someone wants to start helping, you do need a good grasp of type inference first. It's not a project to learn on.

However the internal intermediate language, Core, is fully impredicative and always has been. No difficulties there.

Simon

mentioned in issue #9420 (closed)

mentioned in issue #9618 (closed)

added ImpredicativeTypes label

added Pnormal label

mentioned in merge request !3220 (closed)

mentioned in issue #18126

mentioned in commit 950241e2

mentioned in commit 7fc8834a

mentioned in commit ed8c31bc

mentioned in commit 5e0a1a60

mentioned in commit ecde8584

mentioned in commit c60e4c5a

mentioned in commit db113646

mentioned in commit ae1a310c

mentioned in commit df22930c

mentioned in commit 8a7d504b

mentioned in commit ab84e960

mentioned in commit 375a51c9

mentioned in commit 7192b723

mentioned in commit 70721a6b

mentioned in commit f985681c

mentioned in commit 2351f490

mentioned in commit 95c8e9fc

mentioned in commit da59b24e

mentioned in commit 3c40898d

mentioned in commit 62981125

mentioned in commit 9632f413

mentioned in commit f8aa5775

mentioned in commit 5d81a9b8

mentioned in commit b83009b1

mentioned in commit fcc9aab3

mentioned in commit 97cff919

This is fixed by

commit b83009b1eea18345786971274eff3735a5d28378
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Jul 15 23:50:42 2020 +0100

    Implement Quick Look impredicativity
    
    This patch implements Quick Look impredicativity (#18126), sticking
    very closely to the design in
        A quick look at impredicativity, Serrano et al, ICFP 2020   

except that left and right sections don't work with impredicativity. That is still to do.