Skip to content

Fixes for implicit type vars and datatype decls in smt-lib#254

Merged
Gbury merged 1 commit into
masterfrom
implicit_type_params_and_datatype_decls
Feb 12, 2026
Merged

Fixes for implicit type vars and datatype decls in smt-lib#254
Gbury merged 1 commit into
masterfrom
implicit_type_params_and_datatype_decls

Conversation

@Gbury

@Gbury Gbury commented Feb 11, 2026

Copy link
Copy Markdown
Owner

Two fixes:

  • do not create an instance of an implicit type variable when checking whether something is shadowed. Otherwise, that instance might be wrongly assumed to be used, and in the case of a datatype declaration that does not allow implicit type variables, this will raise a spurious error
  • in datatype declarations, only explicit type variables are allowed, which was already correctly handled, but a shadowing warning was still emitted when one of the explicit type variables had the same name as one of the implicit one. In this case, there is no need for the warning as the implicit type variable cannot be used

This will close #253

Two fixes:
- do not create an instance of an implicit type variable when checking
  whether something is shadowed. Otherwise, that instance might be
  wrongly assumed to be used, and in the case of a datatype declaration
  that does not allow implicit type variables, this will raise a
  spurious error
- in datatype declarations, only explicit type variables are allowed,
  which was already correctly handled, but a shadowing warning was still
  emitted when one of the explicit type variables had the same name as
  one of the implicit one. In this case, there is no need for the
  warning as the implicit type variable cannot be used
@Gbury Gbury force-pushed the implicit_type_params_and_datatype_decls branch from 936a3c5 to 1f7d8ed Compare February 11, 2026 16:38
@Gbury Gbury merged commit 3a2518a into master Feb 12, 2026
38 of 39 checks passed
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.

[SMT2.7] Shadowing type var in par

1 participant