Make sure you're not importing an overloaded constructor. i.e. sometimes even if the goal and variable signature look the same, one may be in fact be using an overloaded constructor of a different type.<br><br><div class="gmail_quote">
On Mon, Nov 15, 2010 at 9:42 AM, Ondrej Rypacek <span dir="ltr"><<a href="mailto:ondrej.rypacek@gmail.com">ondrej.rypacek@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi all,<br>
is this normal:<br>
<br>
Goal: _≡_ {IdObj G n} (⟦_⟧Obj {G} {n} x) (⟦_⟧Obj {G} {n} x')<br>
Have: _≡_ {IdObj G n} (⟦_⟧Obj {G} {n} x) (⟦_⟧Obj {G} {n} x')<br>
<br>
I.e. I have what is asked of me, but yet the goal wouldn't be accepted<br>
? With an error which an error which doesn't make sense to me, and<br>
I've tripple-checked everything, so am really puzzled.<br>
<br>
The source is a bit complicated to be posted here, so I wanted to<br>
check whether this is possible at all (and if there are some likely<br>
causes) before trying to come up with a simpler example.<br>
<br>
Cheers,<br>
Ondrej<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br><br clear="all"><br>-- <br>Respectfully,<br>Larry Diehl<br><br>