search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 22 forks source link

Name clashes between bound variables and symbols: prefer resolving to bound variables #543

Open ComFreek opened 3 years ago

ComFreek commented 3 years ago

The following unexpectedly typechecks successfully:

theory TestCase : ur:?LF =
  a : type ❙
  b : type ❙
  x : a ❙
  f : b ⟶ a ❘ = [x: b] x ❙
❚

Problem: This should not typecheck. It typechecks because the token x in the definiens of f is resolved to a reference to the constant x : a and not to the variable bound in [x]. Such weird resolutions (from the user's POV) also happen in right-hand sides of view assignments.

Suggestion: Always prefer resolving tokens to bound variables over resolving them to symbols or notations.