Allow restricted higher-rank polymorphism

[evincarofautumn]

It should be possible to write this function:

def trip (a a (a a -> a) -> (a & a & a)):
  -> { a b f }
  a b f@
  a b f@
  a b f@
  pair pair

But its type is:

∀r s a. r a a (s a a → s a) → r (a & a & a))

When it should be the rank-2:

∀r a. r a a (∀s. a a → s a) → r (a & a & a))

So the compiler complains because f is applied to different stack types.

[strager]

Why not this?

def trip (a a (a a -> a) -> (a & a & a)):
  -> { a b f }
  a b f@  // fat
  dup dup
  pair pair

Or is it just a bad example?

[kchaloux]

There is already a workaround for it:

def trip (a a (a a -> a) -> (a & a & a)):
  -> { a b c }
  a b f@ -> x
  a b f@ -> y
  a b f@ -> z
  x y z pair pair

But the behavior that most would probably expect would be for invocations of f to still be valid when applied multiple times, the same way any normal local can be pushed onto the stack multiple times after it is bound.