Opened 22 months ago

Closed 8 months ago

#11431 closed bug (fixed)

GHC instantiates levity-polymorphic type variables with foralls

Reported by: gridaphobe Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.1
Keywords: TypeApplications, LevityPolymorphism Cc: simonpj, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider the following use of error.

ghci> :t error
error
  :: forall (v :: GHC.Types.Levity) (a :: TYPE v).
     (?callStack::GHC.Stack.Types.CallStack) =>
     [Char] -> a

ghci> :t error "bad" :: (forall a. a -> a) -> a
error "bad" :: (forall a. a -> a) -> a
  :: (?callStack::GHC.Stack.Types.CallStack) =>
     (forall a1. a1 -> a1) -> a

GHC is instantiating the type variable a in the output with (forall a. a -> a) -> a, which requires impredicative polymorphism. So this example should actually be rejected by the type checker.

Note that GHC also does this with open-kinded type variables, so the behavior with error and undefined has been around for a while. There are tests that depend on it, and a Note that describes the decision to accept these programs. Still, Simon PJ says perhaps we should really just reject these programs.

So here's a ticket to discuss the matter.

For more information, see the discussion starting at https://phabricator.haskell.org/D1739#51408.

Change History (7)

comment:1 Changed 22 months ago by goldfire

I think the current behavior is fine, if somewhat unexpected. (We should document it if we haven't.)

There is no such thing as a levity-polymorphic value. (If there were, how much space would it take up?) Thus, any levity-polymorphic expression must be bottom. So I don't see how a tiny bit of impredicativity just for bottoms can cause trouble.

comment:2 Changed 22 months ago by simonpj

I don't see how a tiny bit of impredicativity just for bottoms can cause trouble.

Impredicativity never causes trouble for the dynamic semantics; after all Core is impredicative. In contrast levity-polymorphism does.

Impredicativity does cause trouble for type inference -- see zillions of papers on the subject. In contrast levity-polymorphism does not. (Except in enforcing the restrictions that levity polyormophism must follow to avoid screwing up the dynamic semantics.)

There is no reason (that I can see) that the restrictions for levity polymorophism should be sufficient to avoid all type-inference/impredicativity difficulties. Maybe so, but it would be a coincidence.

There's an engineering issue too. Richard is about to eliminate RetTv. But RetTv is essential to the implementation that accepts the above program. Are we going to leave RetTv for this sole (ill-defined) purpose?

comment:3 in reply to:  2 Changed 22 months ago by goldfire

Replying to simonpj:

There's an engineering issue too. Richard is about to eliminate RetTv. But RetTv is essential to the implementation that accepts the above program. Are we going to leave RetTv for this sole (ill-defined) purpose?

Yes, I recognize that as an unfortunate consequence of this suggestion. But it wouldn't be ReturnTv -- it would go back to the old PolyTv, just a tyvar that's allowed to unify with a polytype.

Agreed that, if this works, it's a coincidence. That does seem to suggest that it doesn't work. My hope that it would work is because levity polymorphism is vanishingly rare.

In any case, I don't feel strongly.

comment:4 Changed 22 months ago by simonpj

Keywords: TypeApplications added

Tagging this with TypeApplications. Not strictly correct, but in the same general territory and I don't want to lose track of it.

comment:5 Changed 22 months ago by goldfire

It is very considerably easier not to instantiate levity-polymorphic variables with foralls. So that's what I'm doing right now.

comment:6 Changed 12 months ago by bgamari

Keywords: LevityPolymorphism added

comment:7 Changed 8 months ago by goldfire

Resolution: fixed
Status: newclosed

This seems resolved. GHC now allows no impredicative polymorphism, even for levity-polymorphic values. Closing the ticket.

Note: See TracTickets for help on using tickets.