| 12345678910111213141516171819202122232425262728 |
- {-# OPTIONS --allow-unsolved-metas #-}
- -- {-# OPTIONS -v tc.record.eta:20 -v tc.eta:100 -v tc.constr:50 #-}
- -- Andreas, 2013-05-15 reported by nomeata
- module Issue846 where
- open import Issue846.Imports
- opt-is-opt2 : ∀ n s → n mod 7 ≡ 1' → winner n s opt ≡ false
- opt-is-opt2 0 s ()
- opt-is-opt2 (suc n) s eq =
- let (pick k 1≤k k≤6) = s (suc n)
- in
- cong not (opt-is-opt (suc n ∸ k) s (lem-sub-p n k eq {!1≤k!} {!!} ))
- -- The problem here was that the first hole was solved by
- -- 'nonEmpty' by the instance finder,
- -- which is called since the first hole is an unused argument.
- -- 'nonEmpty' of course does not fit, but the instance finder
- -- did not see it and produced constraints.
- -- The eta-contractor broke on something ill-typed.
- -- Now, the instance finder is a bit smarter due to
- -- improved equality checking for dependent function types.
- -- Unequal domains now do not block comparison of
- -- codomains, only block the domain type.
|
