stchang
[WIP] Infer instantiations for polymorphic arguments to polymorphic functions [rebase of Alex Knauth's PR on bitbucket]
Hello,
I took @AlexKnauth somewhat outdated PR https://bitbucket.org/stchang/macrotypes/pull-requests/21 and rebased it onto master. There were a few simple conflicts, so it's possible that I accidentally discarded or damaged part of the original patch.
The changes are only applied to the macrotypes/ subfolder for now. Is there an automated translation between the macrotypes/ and turnstile/ folders, or is the procedure simply to manually apply the changes in both directories?
After a few adjustments, most tests seem to succeed (I still have a few to fix).
it seems incapable of typechecking (Cons (λ ([x : X]) x) Nil), regardless of how many ann and inst I add to the expression. I suspect that this is because the ∀ are now lifted outwards as much as possible, but the solve and add-constraints probably need some adjustment to work with that.
The reason why (Cons (λ ([x : Y]) x) Nil) would not typecheck was because the Y in → Y Y appeared in a contravariant position, and the relaxed value restriction (from http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf) says that polymorphic type variables cannot be generalisable if they appear in a contravariant position.
However, I suspect that this restriction only concerns type variables which were in the original signature of the function being called, not type variables which belong to arguments.
The last commit (9d812c0) therefore checks whether the X which may cause an error belongs to #'Xs (the stx-list of type variables from the (∀ (tyvar …) τ) signature of the function being called), instead of checking whether the X belongs to #'Xs* (the stx-list of type variables which appear in the signature + those which appear in the types of arguments).
I am not 100% sure this is the right thing to do, however, and cannot guarantee that this does not open the door to unsoundness with weird edge cases.
Yes, the examples in macrotypes and turnstile are independent. It has helped some people to be able to look at the two implementations side-by-side. It does result in somewhat more maintenance work but usually any changes are similar.
Is this still WIP?
Yes, it's still WIP. Sorry for the delay, hopefully I'll be able to finish it soon.