Better decidability via uncompared higher-kinded witnesses
Status: open (task from 2026-05-28 meeting)
Conjecture: higher-kinded witnesses in transparent existentials are never compared by equivalence, so the decidability argument can exploit this to get a stronger decidability result for the recursive modules system.
What would settle it
Find the place in the algorithm where higher-kinded witness equivalence would otherwise be needed and show it is avoidable; turn that into a decidability theorem (and clean up the appendix’s weird example — if OCaml mistakenly accepts it, report an issue).
Related
Double-Vision Recursive Modules · Locator-Anchored Signatures