Opened 4 years ago

Closed 16 months ago

#11319 closed bug (fixed)

ImpredicativeTypes even more broken than usual

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.11
Keywords: ImpredicativeTypes Cc: goldfire, a.serranomena@…
Operating System: Linux Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T11319
Blocked By: Blocking:
Related Tickets: #14859 Differential Rev(s):
Wiki Page:

Description

I don't have the latest version of GHC, trying to derive Functor A and Foldable A is fine but when I derive Traversable A in the attachment Error.hs:

{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, ImpredicativeTypes #-}

import Data.Functor     (Functor)
import Data.Foldable    (Foldable)
import Data.Traversable (Traversable)

data A a = A
  deriving (Functor, Foldable, Traversable)

GHC barks at me (verbose log attached):

/tmp/Error.hs:8:32: error:
     Couldn't match type forall a1. A a1 with A b
      Expected type: f (A b)
        Actual type: f (forall a. A a)
     In the expression: pure A
      In an equation for traverse: traverse f A = pure A
      When typechecking the code for traverse
        in a derived instance for Traversable A:
        To see the code I am typechecking, use -ddump-deriv
      In the instance declaration for Traversable A
     Relevant bindings include
        f :: a -> f b (bound at /tmp/Error.hs:8:32)
        traverse :: (a -> f b) -> A a -> f (A b)
          (bound at /tmp/Error.hs:8:32)

With -ddump-deriv we get this (unqualified) instance:

  instance Traversable A where
    traverse f_a2Le A = pure A

which by itself causes the same problem in the attachment Error2.hs:

{-# LANGUAGE DeriveFunctor, DeriveFoldable, ImpredicativeTypes #-}

import Data.Functor     (Functor)
import Data.Foldable    (Foldable)
import Data.Traversable (Traversable)

data A a = A
  deriving (Functor, Foldable)

instance Traversable A where
  traverse f A = pure A

Works fine in GHC-7.10.2 and GHC-7.10.0.20150316 and GHC-7.4 (with some additional imports), is this an ImpredicativeTypes regression?

Attachments (4)

Error.hs (252 bytes) - added by Iceland_jack 4 years ago.
Derives Traversable
Error2.hs (318 bytes) - added by Iceland_jack 4 years ago.
Handwritten instance of Traversable, cleaned up output of -ddump-deriv
Error.log (3.5 KB) - added by Iceland_jack 4 years ago.
ghc-7.11.20151226 -v -ignore-dot-ghci --interactive /tmp/Error.hs &> /tmp/Error.log
Error2.log (3.4 KB) - added by Iceland_jack 4 years ago.
ghc-7.11.20151226 -v -ignore-dot-ghci --interactive /tmp/Error2.hs &> /tmp/Error2.log

Download all attachments as: .zip

Change History (18)

Changed 4 years ago by Iceland_jack

Attachment: Error.hs added

Derives Traversable

Changed 4 years ago by Iceland_jack

Attachment: Error2.hs added

Handwritten instance of Traversable, cleaned up output of -ddump-deriv

Changed 4 years ago by Iceland_jack

Attachment: Error.log added

ghc-7.11.20151226 -v -ignore-dot-ghci --interactive /tmp/Error.hs &> /tmp/Error.log

Changed 4 years ago by Iceland_jack

Attachment: Error2.log added

ghc-7.11.20151226 -v -ignore-dot-ghci --interactive /tmp/Error2.hs &> /tmp/Error2.log

comment:1 Changed 4 years ago by Iceland_jack

GHCi (version 7.11.20151226) and Glasgow Haskell Compiler (version 7.11.20151226, stage 2 booted by GHC version 7.8.4).

comment:2 Changed 4 years ago by rwbarton

Cc: goldfire added
Summary: ImpredicativeTypes cause trouble (affects deriving of Traversable)ImpredicativeTypes even more broken than usual

Nothing special about deriving here, try:

{-# LANGUAGE ImpredicativeTypes #-}

f :: Applicative f => f (Maybe a)
f = pure Nothing

main = return ()

{-
Error.hs:4:5: error:
    • Couldn't match type ‘forall a1. Maybe a1’ with ‘Maybe a’
      Expected type: f (Maybe a)
        Actual type: f (forall a. Maybe a)
    • In the expression: pure Nothing
      In an equation for ‘f’: f = pure Nothing
    • Relevant bindings include
        f :: f (Maybe a) (bound at Error.hs:4:1)
-}

This is with an up-to-the-minute version of HEAD, that contains the relevant-looking Phab:1715.

As ImpredicativeTypes is unsupported anyways, perhaps we should just take the opportunity to kill it?

comment:3 Changed 4 years ago by goldfire

It would make sense that the type-checker rewrite from visible type application would break impredicativity even more than usual. Given its already-quite-broken state, I didn't try to salvage it.

I don't want to completely kill it, though, as it sometimes is useful, if just for experimentation. And visible types lets you climb out of any hole you get in. For example, this works:

{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, TypeApplications #-}

module Bug where

f :: forall a f. Applicative f => f (Maybe a)
f = pure (Nothing @a)

All that said, I'll take a look at this one, as it would be nice to be less broken. And my hunch is that this will be quite easy to fix.

comment:4 Changed 4 years ago by simonpj

Cc: a.serranomena@… added

This is definitely fallout from Visible Type Application. The program in comment:3 typechecks fine without ImpredicativeTypes (indeed it does in Haskell 98!) and surely ImpredicativeTypes should be a conservative extension.

But let's not invest much in "fixing" ImpredicativeTypes which is simply not supported at the moment. Alejandro Serrano (cc'd) is working on impredicativity right now, so I've added him to the cc list.

Alejandro, what are you doing will be significantly affected by the "lazy instantiation" approach of Visible Type Application (see paper), so you might want to look carefully. VTA is in GHC now!

comment:5 Changed 4 years ago by goldfire

Upon further thought, the new behavior is actually less broken than the old behavior, for a certain definition of broken.

Consider the typing rule for function applications, as in the "Practical Type Inference" and "Visible Type Application" papers (they're the same, in this respect):

G |- e1 => s1 -> s2
G |- e2 <= s1
---------------- App
G |- e1 e2 => s2

Here, => indicates type inference, while <= indicates type checking. There is no type checking rule for applications. So this means that any type expected by the context is simply not propagated down when checking the individual pieces.

Given this fact, we can think about pure Nothing in a vacuum, without any type expected by its context. We see pure :: forall f. Applicative f => forall a. a -> f a. We guess a type (call it s) for a and then check Nothing against s. Without ImpredicativeTypes, s is constrained to be a tau-type -- that is, with no foralls anywhere. Thus, Nothing :: forall a. Maybe a must be instantiated to Nothing :: Maybe t for some t. But with ImpredicativeTypes, s can have foralls. So GHC doesn't instantiate, as it has no good reason to. It infers pure @f @(forall a. Maybe a) Nothing :: f (Maybe (forall a. Maybe a)). This is fully correct behavior. Then, when GHC checks that inferred type against the expected type f (Maybe b) (for some known skolem b) the check fails.

So, the behavior we see is entirely predictable given the published typing rules when you relax the restriction around tau-types. And that's why I say it's less broken than the old behavior.

On the other hand, it is sad that ImpredicativeTypes fails to accept Haskell98. Simon has cooked up a scheme that, I believe, will fix this case (written up at wiki:Typechecking), but that won't make it for 8.0, I would think. (Unless Simon wants to implement that plan in short order!) The key bit is that it comes up with a "checking" (that is, <=) rule for function application that propagates information down, forcing instantiation of Nothing, as desired.

In any case, this isn't a quick fix and so I will remove it from my queue, as investing time in patching together ImpredicativeTypes seems less useful than other ways of using that precious resource.

comment:6 Changed 4 years ago by Reid Barton <rwbarton@…>

In b7dfbb4/ghc:

Add test for #11319

comment:7 Changed 4 years ago by rwbarton

Test Case: typecheck/should_compile/T11319

comment:8 Changed 4 years ago by goldfire

Just to note that most of wiki:Typechecking is indeed in HEAD and 8.0 now. The bit that I believe would fix this ticket is ExpFun, which is not implemented.

comment:9 Changed 2 years ago by dfeuer

Simon, are you still hoping to make ImpredicativeTypes work, or should this be closed as WONTFIX, or something else?

Last edited 2 years ago by dfeuer (previous) (diff)

comment:10 Changed 2 years ago by simonpj

Leave it open as a useful test case. Alejandro is still thinking about impredicativity, making some progress.

comment:11 Changed 2 years ago by RyanGlScott

Since this ticket was originally opened, SPJ started a very relevant discussion on the GHC devs mailing list about a way to salvage ImpredicativeTypes. It wouldn't make the original program in this ticket typecheck again, but it would provide a way to possibly suggest a workaround in error messages.

To quote SPJ:

When you have -XImpredicativeTypes

  • You can write a polytype in a visible type argument; eg. f @(forall a. a->a)
  • You can write a polytype as an argument of a type in a signature e.g. f :: [forall a. a->a] -> Int

And that’s all. A unification variable STILL CANNOT be unified with a polytype. The only way you can call a polymorphic function at a polytype is to use Visible Type Application.

So using impredicative types might be tiresome. E.g.

type SID = forall a. a->a



xs :: [forall a. a->a]

xs = (:) @SID id ( (:) @SID id ([] @ SID))

In short, if you call a function at a polytype, you must use VTA. Simple, easy, predictable; and doubtless annoying. But possible.

However, this should undoubtedly go through a GHC proposal. At the very least, it's unclear to me whether SPJ's intention was to require actually enabling -XImpredicativeTypes in order to visibly apply a polytype (the title of the GHC devs discussion, "Getting rid of -XImpredicativeTypes", makes me think "no", but the actual contents of the discussion that I quoted would suggest "yes").

comment:12 Changed 2 years ago by goldfire

Agreed about the proposal. Let's hash out the details there.

comment:13 Changed 2 years ago by Iceland_jack

I also noticed this paper (Guarded impredicative polymorphism) from Simon's website as "in submission", how does it relate? :)

comment:14 Changed 16 months ago by RyanGlScott

Resolution: fixed
Status: newclosed

Note that:

Therefore, let's close this, and move the discussion about the latter point to #14859.

Note: See TracTickets for help on using tickets.