Opened 2 months ago

Last modified 2 months ago

#8808 new bug

ImpredicativeTypes type checking fails depending on syntax of arguments

Reported by: guest Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.1-rc1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

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 : [])’

Change History (1)

comment:1 Changed 2 months ago by simonpj

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

Note: See TracTickets for help on using tickets.