You need to sign in or sign up before continuing.
Use high cost for `Decision` instances for `True` and `False`.
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.