Implementing for-all and exists types

[LighghtEeloo]

At this stage we should consider bringing system-F to our language. Due to the fact that we are dealing with CBPV, we've decided to make for-all types computation types and exists types value types.

Sample syntax:

def id : Thunk(forall (X : VType) . X -> Ret X) = {
  fn (X : VType) -> fn (x : X) -> ret x
} end

! id @(Int) 42
# ans: 42

[LighghtEeloo]

Sample syntax for forall and exists:

data Seal (X : VType) (A : VType) where
| Seal(Thunk(A -> Ret X), Thunk(X -> Ret A))
end

def id : Thunk(forall (A : VType) . A -> Ret A) = {
    fn (A : VType) -> fn x -> ret x
} end

def nat : exists (X : VType) . Seal X Int = pack(
  Int, Seal(
    { ! id @(Int) },
    { ! id @(Int) },
  )
) end

match nat | pack(Nat, seal) ->
  match seal
  | Seal(of, to) ->
    do n <- ! of 0;
    do i <- ! to n;
    ! exit i
  end
end

[LighghtEeloo]

Though we've introduced for-all and exists types since e191814, they are a bit lengthy to use rn. It might be better to allow an implicit version of for-all typed terms optionally.

The only change I can smell of happens in the type checker. Since we are only checking type functions against for-all types, here's my proposal:

1. if both a type function and a forall type are met, instantiate both type variables with a fresh type as usual;
2. if a type function is met while no forall type is found, raise a type check error;
3. if a non-type-function term* is met in the face of a forall type, silently instantiate a type variable with the same name in the term context.

• we may restrict the term to have fn -> for a better (?) code style.

@maxsnew Would you kindly share your thoughts on whether this solution appears to be feasible?

[LighghtEeloo]

As discussed in the weekly meeting, with the successful implementation and integration of the explicit version of System-F, we are now in a good position to close this issue.

As a next step, a separate issue will be opened to address the implementation of implicit polymorphism. This new issue will focus on enhancing the language's expressiveness and user experience, leveraging the strong foundation laid by the explicit System-F implementation.