# Higher-ranked polymorphism without explicit application or subtyping?

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?

• Haskell will never infer a polytype for a type variable, unless it's explicitly provided by the user. E.g. \f -> (f True, f 'a') won't type check, even if it can be assigned the type (forall t. t->t) -> (Bool, Char) – chi May 14 '17 at 6:45
• @chi I'm interested in the uses, not definitions, of polymorphic values, see my edit for an example of what I mean. Sorry if this wasn't clear at first. – jmite May 14 '17 at 7:08
• There should be some Simon Peyton-Jones paper which explains the inference algorithm (I can't point which one, though). But probably the inference engine can see that g expects a polytype, and prevents the instantiation of f. – chi May 14 '17 at 7:57
• – phadej May 14 '17 at 20:56

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.

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