[GHC] #8808: ImpredicativeTypes type checking fails depending on syntax of arguments
#8808: ImpredicativeTypes type checking fails depending on syntax of arguments -------------------------------------+------------------------------------- Reporter: guest | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1-rc1 checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: Unknown/Multiple | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- 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 : [])’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8808 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8808: ImpredicativeTypes type checking fails depending on syntax of arguments ----------------------------------------------+---------------------------- Reporter: guest | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: Resolution: | 7.8.1-rc1 Operating System: Unknown/Multiple | Keywords: Type of failure: GHC rejects valid program | Architecture: Test Case: | Unknown/Multiple Blocking: | Difficulty: Unknown | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8808#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8808: ImpredicativeTypes type checking fails depending on syntax of arguments -------------------------------------+------------------------------------- Reporter: guest | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.1-rc1 checker) | Keywords: Resolution: | ImpredicativeTypes Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => ImpredicativeTypes -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8808#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC