Skip to content

Make a type-annotated binder shadow a like-named constant#184

Open
kings-crown wants to merge 1 commit into
jrh13:masterfrom
kings-crown:obfus
Open

Make a type-annotated binder shadow a like-named constant#184
kings-crown wants to merge 1 commit into
jrh13:masterfrom
kings-crown:obfus

Conversation

@kings-crown

Copy link
Copy Markdown
Contributor

A bound variable may legitimately share its name with a constant, and
the binder should win within its scope. This already worked for
un-annotated varstructs via ignore_constant_varstruct, but broke as soon
as the binder carried a type annotation:

new_definition `test_const = T`;;            (* test_const : bool *)
`forall (test_const:num). test_const > 0`;;
(* typechecking error (initial type assignment): test_const has
   type bool, it cannot be used with type num *)

Cause: in typify's Absp branch the varstruct was typed first, and only
then was a resulting Constp rewritten back to a Varp. With an annotation
the constant-resolution clause unifies the constant's generic type
(bool) against the annotation (num) and raises before that post-hoc
rescue can run.

Fix: seed the varstruct's constant-named binders into venv before typing
it, so they take typify's "already a bound variable" clause rather than
being resolved to the like-named constant. This generalizes the old
rescue: it also covers type-annotated binders such as
\(Q1:num#num#num#num). ... and tuple varstructs. Only binder-position
constant names are seeded, so free occurrences still resolve to the
constant. With ignore_constant_varstruct=false the previous behaviour is
preserved exactly.

Patch constructed with the help of (mostly) Claude Code.

@kings-crown kings-crown reopened this Jun 15, 2026
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