Fix generic type inference#1074
Closed
Dragon-Hatcher wants to merge 5 commits into
Closed
Conversation
Adds TypeExprF.uvar (id : Nat) as a fresh per-call-site unification
variable for instantiating polymorphic user-defined functions.
Previously, inferType returned raw .tvar String nodes from a function's
stored declaration type. When two generic calls appeared as operands to a
builtin (e.g. right(a,a) + left(a,a)), the tvar names from different
declarations ("W" vs "T") were compared and rejected even though both
instantiated to the same concrete type.
The fix applies Hindley-Milner instantiation at each call site:
- freshenTVars replaces tvar nodes with fresh uvar nodes (one per unique
tvar name, unique ids across call sites via ElabState.nextUVarId)
- unifyTypes now solves uvar nodes, recording id→type in ElabState.uvarMap
- resolveUVars substitutes solved uvars to produce the concrete return type
- ExprInfo.resolvedType stores this resolved type so elabSyntaxArg uses
it instead of re-calling inferType (which would return raw tvars again)
uvar nodes are transient elaboration artifacts and never appear in the
final output tree; all downstream passes (Translate, Ion, ToExpr) panic
or error if they encounter one.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Adds test programs covering: - Identity function with int and bool - Nested generic calls (id(id(x)), id(left(a, b))) - Three type parameters (fst3, snd3, thd3) - Mixed concrete types (int vs bool as distinct type args) - Generics inside conditional expressions - Same generic called multiple times in one expression Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…l sites Adds differentInstantiationsPrg with three functions that verify each call site gets independent unification variables: - mixedId: id<T=int> and id<T=bool> in a single boolean expression - mixedLeft: left<T=bool,U=int> and left<T=int,U=bool> in one expression - chainDifferent: id wrapping left (int result) and id wrapping right (int result), where T instantiates to int via two independent paths Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Resolves conflict between the incoming tvar propagation in the arrow case of unifyTypes (which recurses into sub-components rather than passing through) and our uvar passthrough for fresh unification variables. Both cases are now distinct: tvar propagates into the arrow's domain and codomain; uvar passes through since it will be resolved after call-site elaboration completes. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Contributor
|
Closing since #1125 will bypass the issue for now |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fix generic type inference for user-defined polymorphic functions. See #1022 and #1050.
Calling multiple user-defined generic functions together in one expression would fail with a
spurious type error. For example:
The issue is that type inference in the DDM layer treated the polymorphic types as literal strings. So the return type of
leftis.tvar "T"and the return type ofrightis.tvar "U". As a result, swapping the names of the parameters on one of the functions would make the code compile.To fix this, each time we instantiate a function call, we replace each
.tvarwith a.uvarwith a unique index. When we infer a type for one of these.uvars, we store it in theElabState. An error is produced if identical.uvars get solved to two different types.