Skip to content

Use high cost for `Decision` instances for `True` and `False`.

Robbert Krebbers requested to merge robbert/decision_true_false_cost into master

This fixes issue #165 (closed).

What happens is that it needs to solve Decision (@elem_of ... ?instance x xs) where ?instance is an evar representing an unresolved type class. Now instead of solving ?instance first, Coq applies False_dec and uses HO-unification to instantiate ?instance with λ _ _, False, i.e., something nonsensical.

By increasing the cost of the True and False instances we make sure Coq first uses the elem_of_dec instance.

Merge request reports