Constraint handling rules with binders, patterns and generic quantification*. Issue 5 (22nd August 2017) - SERRANO, ALEJANDRO; HAGE, JURRIAAN
Abstract: Constraint handling rules provide descriptions for constraint solvers. However, they fall short when those constraints specify some binding structure, like higher-rank types in a constraint-based type inference algorithm. In this paper, the term syntax of constraints is replaced by λ-tree syntax, in which binding is explicit, and a new ∇ generic quantifier is introduced, which is used to create new fresh constants.