Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unique TypeVariables #66

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

gardspirito
Copy link
Contributor

Ensures there aren't any conflicting type variables.

Closes #64.

@gardspirito
Copy link
Contributor Author

This PR does not perform necessary substitutions for check phase:

>>> let test : (forall (x : Type). x -> x) = let test2 : (forall (x : Type). x -> x) = \x -> let y : x = x in y in test2 in test
Not a subtype

The following type:

  x0

(input):1:63: 
  │
1 │ let test : (forall (x : Type). x -> x) = let test2 : (forall (x : Type). x -> x) = \x -> let y : x = x in y in test2 in test
  │                                                               ↑

… cannot be a subtype of:

  x

(input):1:98: 
  │
1 │ let test : (forall (x : Type). x -> x) = let test2 : (forall (x : Type). x -> x) = \x -> let y : x = x in y in test2 in test
  │                                                                                                  ↑

I guess there must be a better approach.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

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