Higher-ranked polymorphism without explicit application or subtyping?

Question

So, I'm familiar with two main strategies of having higher-ranked polymorphism in a language:

• System-F style polymorphism, where functions are explicitly typed, and instantiation happens explicitly though type application. These systems can be impredicative.
• Subtyping-based polymorphism, where a polymorphic type is a subtype of all of its instantiations. To have decidable subtyping, polymorphism must be predicative. This paper provides an example of such a system.

However, some languages, like Haskell, have impredicative higher-ranked polymorphism without explicit type applications.

How is this possible? How can type-checking "know" when to instantiate a type without an explicit instantiation or cast, and without a notion of subtyping?

Or, is typechecking even decidable in such a system? Is this a case where language like Haskell implement something undecidable that happens to work for most peoples' use cases.

EDIT:

To be clear, I'm interested in the uses, not definitions, of polymorphically-typed values.

For example, suppose we have:

f : forall a . a -> a
g : (forall a . a -> a) -> Int
val = (g f, f True, f 'a')

How can we know that we need to instantiate f when it's applied, but not when it's given as an argument?

Or, to separate ourselves from function types:

f : forall a . a
g : (forall a . a) -> Int
val = (g f, f && True, f + 0)

Here, we can't even distinguish the use of f as applying it versus passing it: it's instantiated when passed as an argument to && and +, but not g.

How can a theoretical system distinguish these two cases without a magical "you can convert any polymorphic type to its instance" rule? Or with a rule like that, can we know when to apply it, to keep decidability?

Answer 1

The Dunfield & Krishnaswami paper's introduction refers to Practical type inference for arbitrary-rank types

As can be seen, it scales well to advanced type systems; moreover, it is easy to implement, and yields relatively high-quality error messages (Peyton Jones et al. 2007)

In System F-ish approach there is also a "subtyping" relation. See section 3.3 Subsumption.

---

I'd also emphasize that Haskell doesn't have impredicative types (or inference for them). See: https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html for pointers.

• 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.

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

I.e. id id will always be elaborated as

forall a. id @(a -> a) (id @a)

not

id @(forall a. a -> a) id

Yet, you can write the latter explictly, if you enable ImpredicativeTypes.

Answer 2

To check the application of a function like g : (forall a. a -> a) -> Int to f, we need to check that f : forall a. a -> a.

Instead of matching quantifiers (which would be quite brittle), we introduce a fresh, rigid (i.e., non-unifiable) variable, say a1, and we need to check that f : a1 -> a1, and now we can carry on as usual, instantiating f at a1 (modulo additional checks to ensure that a1 does not escape its scope).

The actual algorithm is detailed in the paper phadej linked.

Or, is typechecking even decidable in such a system? Is this a case where language like Haskell implement something undecidable that happens to work for most peoples' use cases.

The general problem of type inference in the presence of higher-ranked polymorphism remains undecidable. However, with full type annotations it becomes a (mostly?) decidable type checking problem. GHC's algorithm must thus be incomplete, but tries to cover as much ground as it can in the middle of these two situations, with the help of a few sparse type annotations.