Generating constraints to solve dependently-typed metavariables?
Question
In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments.
There are many papers which describe, given a unification problem in the pattern fragment, how to find a solution if one exists. Examples include are (Gundry-McBride), (Abel-Pientka), and the original Miller paper.
What I'm wondering is, given a dependently typed program containing metavariables (or implicit arguments), how does one go about generating the problems that are passed to the unification solver?
No correct solution
Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange