Skip to content

Conversation

oshimayuki1124
Copy link
Contributor

When evaluating the following expression:

let g = fun x -> ((fun y -> y): ? -> ?) x

type abstractions are inserted as:

let g = fun 'x10, 'x11, 'x10 -> fun (x: 'x11) -> ((fun (y: 'x10) -> y): 'x10 -> 'x10 => ? -> ?) (x: 'x11 => ?)

As seen here, the type variable 'x10 appears twice. This duplication happens because the return values of closure_tyvars_let_decl and closure_tyvars2 are not mutually exclusive.

To address this, I made the following changes:

  • Introduced a new function closure_tyvars_let_decl2, which behaves like closure_tyvars2 but excludes tv_exp v1 instead of ftv_exp v1.
  • Renamed closure_tyvars_let_decl to closure_tyvars_let_decl1.

This change does not affect practical behavior, but it may be relevant in theoretical contexts.

Let me know if you have any feedback or if this can be merged.

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.

1 participant