Higher-rank types are weirdly not instantiated

[Nadrieril]

The following code:

type Proxy a = | Proxy
let foo: forall b. (forall a. Proxy a) -> Proxy b
    = \p -> p

gives the following two errors:

error: Expected the following types to be equal
Expected: rankn.Proxy b
Found: forall a . rankn.Proxy a
1 errors were found during unification:
Could not generalize the variable bound to `b` as the variable was used outside its scope
- <rankn>:4:13
4 |     = \p -> p
  |             ^

error: Expected the following types to be equal
Expected: (forall a . rankn.Proxy a) -> rankn.Proxy b
Found: forall c . (forall a . rankn.Proxy a) -> c
1 errors were found during unification:
Types do not match:
    Expected: (forall a . rankn.Proxy a) -> rankn.Proxy b
    Found: forall c . (forall a . rankn.Proxy a) -> c
- <rankn>:4:7
4 |     = \p -> p
  |       ^^^^^^^

Instead of instanciating the forall-quantified type, it seems to be trying to generalize the bound type variable. I have no clue what the second error is on about.
Moveover, there is no way to help the compiler, because adding a type annotation fails similarly.
A related issue is that annotating a bound polymorphic variable with its own type fails too:

let foo id: (forall a. a -> a) -> () = 
    let id': forall a. a -> a = id
    in ()

I don't know if this is a know case that the type system cannot handle or a bug, but I found it surprising (and annoying).

[Marwes]

I fixed the other two issues with higher-rank issues. This one will need some extra work to make sure that I don't introduce any unsoundness. For instance, it interacts closely with the following where I don't want the type forall m . m to be propagated to the argument m of make.

let make m =
    let m2: forall m . m = m
    let _ = m2 1
    m
make 2

gluon/check/tests/fail.rs

Lines 283 to 288 in 2562070

	let make m =
	let m2: m = m
	let _ = m2 1
	m
	make 2

[Nadrieril]

Thanks a lot !

[Marwes]

Should have been closed by 67a502f 🤷‍♂️