search

mzacho / refinement-types

A refinement type checker for simply typed lamda calculus with inductive data-types and well-founded recursive functions
MIT License
0 stars 1 forks source link

SUB-BASE can capture free variables with the binder #22

Open mzacho opened 9 months ago

mzacho commented 9 months ago

Found a bug in our implementation of SUB-BASE: Consider checking if int{x: True} is a subtype of int{v: x > v} in the environment where x:int. Then the x in the predicate, that refers to the x from the environment is incorrectly captured by the binder: Forall x:int: True => x > x. So v1 should be a fresh var in the rule

mkarup commented 9 months ago

Yeah, ran into that too yesterday trying to implement binary search trees. Had a type declaration where the binders were named the same as what I called the binders in the switch expression. I spent a lot of time trying to debug what in the world I was doing wrong until I noticed this issue.

mzacho commented 8 months ago

Hehe, avoiding variable capture is surprisingly hard to get right! Just found another bug like this, tried to describe in #23.

Cool you're implementing binary search trees! I'm doing insertion sort! :)