exists (a : Type). a <: forall (a : Type). a

[gardspirito]

I was trying to introduce impredicative instantiation for my fork of FFG. I thought that it's easy to do, given η-law is sacrificed, if I just expand <:∀R and <:∃L cases of subtype (correct me if I'm wrong). While I was doing that, I suddenly realized that subtype handles Forall and Exists in an exactly same manner.

So I built 7f63aa8 and, surprise-surprise, something is definitely off with this approach:
EDIT: There's something strange with Exists, subtype check. I tested relatively old commit 7f63aa8, and here's what I've got:

let test
    : exists (a : Type). a
	= 3
in test : forall (a : Type). a

❯ nix shell github:Gabriella439/grace/7f63aa8a1835ca1a782f18eb773c80ea2af4cd5f

❯ grace interpret test.ffg --annotate
3 : forall (a : Type) . a

[gardspirito]

Yeah, I should study the problem before I write. But I guess I found the source.

grace/src/Grace/Infer.hs

Lines 246 to 248 in cd70563

	(Type.VariableType{ name = a0 }, Type.VariableType{ name = a1 })
	| a0 == a1 -> do
	wellFormedType _Γ _A0

Comparison is performed by name, but matching names don't necessarily mean that two variables are one and the same.
exists a. a <: forall a. a
=> forall a. (a <: forall a. a)
=> forall a. (forall a. (a <: a))

Typechecker looks at this, sees two same names and assumes that this is the same variable.
If we change the source code to:

let test
    : exists (a : Type). a
	= 3
in test : forall (a2 : Type). a2

it stops compiling, because it now sees that a ≠ a2.

EDIT: I guess that just a substitute must be made on each Variable declaration.