Why does Program
fail if there are implicit typeclasses holes that cannot be resolved? Is there a way to make Program
turn them into obligations instead?
https://github.com/coq/coq/issues/12147 seems relevant and has a workaround
Definition disable_tc {T : Type} (x : id T) : T := x.
Notation notc_hole := (disable_tc _).
even if that _will_ be annoying for implicit arguments
This doesn't help when I can't figure out where the typeclass hole is in the first place, unfortunately, and I want obligations to help me figure out where they are. (I can stuff the type and code in refine
in a Goal
, but that doesn't work as well when the code is relying on the casts that Program
inserts...)
Last updated: Oct 13 2024 at 01:02 UTC