<div dir="ltr"><div>Oh, sorry. It seems that this code works well indeed. The problem occurs in the code I give below. The reason is that I import both Data.List and Data.Vec. But since xs has type List ℕ, it should be obvious which constructor to use.</div><div>PS: I'm using Agda 2.5.1.1.</div><div><br></div><div>open import Data.Nat</div><div>open import Data.Vec</div><div>open import Data.List</div><div>open import Relation.Binary.PropositionalEquality</div><div><br></div><div>A : (xs : List ℕ) → Set</div><div>A xs = 0 ∷ xs ≡ 0 ∷ xs</div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div>Regards,</div><div dir="ltr">Valery Isaev<br></div></div></div></div></div>
<br><div class="gmail_quote">2016-09-26 7:27 GMT+03:00 Roman <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">My Agda (version 2.6.0) infers everything properly.<br>
</blockquote></div><br></div>