Handling `Type`
Opened this issue · 1 comments
yalhessi commented
CoqSynth doesn't support synthesizing an expression of type Type
(it does return a result but it's unclear how it's incorrect without unification). Lfind also doesn't handle Type
variables.
yalhessi commented
The first major issue we run into here is with example generation. I'm not sure if it's necessary here to monomorphize in able to generate example (see https://softwarefoundations.cis.upenn.edu/qc-current/QuickChickInterface.html)
It looks from looking at https://softwarefoundations.cis.upenn.edu/qc-current/QC.html that QC could be able to handle polymorphic data types