I have a pattern matching construction where I know patterns and a type of scrutinee, and I want to generate all values/examples of this type to test, for example, that my pattern matching is exhaustive (It’s kind of complicated approach but it is a topic of another discussion).
So, for plain ADTs I know how to generate all values in increasing height order. But for GADTs the situation seems to be more complicated.
Can you recommend some papers about this, give links to useful code bases or share any useful ideas?
Inhabiting a GADT is quite closely related to solving a Prolog goal (in a restricted class of goals): each constructor of the GADT is a deduction rule (the constructor parameters are the requirements), and (unlike simple ADTs) the rule involves unification and existentials. You can implement this yourself, by implementing a simple proof search procedure with metavariables and unification, or try to rely on an existing prolog engine (for example Elpi?).