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

[luna-spirito]

~~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 7f63aa8a1835ca1a782f18eb773c80ea2af4cd5f and, surprise-surprise, something is definitely off with this approach:~~ EDIT: There's something strange with Exists, subtype check. I tested relatively old commit 7f63aa8a1835ca1a782f18eb773c80ea2af4cd5f, 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

[luna-spirito]

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

https://github.com/Gabriella439/grace/blob/cd70563b5bc2793aa1ad905309c2c9f00550603c/src/Grace/Infer.hs#L246-L248

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.