<html>
<head>
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>If you replace the offending ees≤m (which Agda highlighted in
red) with {!ees≤m!}, you'll notice that "Have" and "Goal" are
different. See especially the results for full normalization, "C-u
C-u C-c C-." When the Goal and Have don't match, that means Agda
won't be able to unify (unless the difference involves
metavariables AND Agda is able to satisfy constraints). Here's a
smaller version of your problem, not relying on standard library
imports:</p>
<p>case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B<br>
case x of f = f x<br>
<br>
postulate<br>
anything : ∀ {a} {A : Set a} → A<br>
X : Set<br>
F : X → Set<br>
<br>
record R : Set where<br>
constructor c<br>
field<br>
r : X<br>
<br>
postulate<br>
s : R<br>
<br>
foo : (r : R) → F (R.r r)<br>
foo _ = anything<br>
<br>
bar1 : F (R.r s)<br>
bar1 = let c x = s in<br>
let letted : F x<br>
letted = anything in<br>
{!letted!} -- works. notice that "Have" and "Goal" match<br>
<br>
bar2 : F (R.r s)<br>
bar2 = case s of λ {(c x) →<br>
let letted : F x<br>
letted = anything in<br>
{!letted!}} -- does not work because Have: F x, but Goal: F
(R.r s)<br>
</p>
<p>One way to get around your problem borrows from an idea I posted
<a
href="https://github.com/agda/agda/issues/426#issuecomment-254111273">here</a>.
We encourage Agda to "remember" that s = c x:</p>
<p>open import Agda.Builtin.Equality<br>
<br>
record Memoized {A : Set} (x : A) : Set where<br>
constructor _,_<br>
field<br>
value : A<br>
sound : value ≡ x<br>
<br>
remember : {A : Set} → (x : A) → Memoized x<br>
remember x = x , refl<br>
<br>
bar2a : F (R.r s)<br>
bar2a = case remember s of λ {(c x , refl) →<br>
let letted : F x<br>
letted = anything in<br>
{!letted!}} -- works<br>
</p>
There are possibly other ways to work around your problem. The
"inspect" idiom comes to mind, as well as the use of "with". Sorry
that's not much of an explanation of what's going on here. I don't
have much theoretical knowledge and only know how to deal with this
sort of thing from trial and error. Mostly error. Hopefully that
gives you some tools to proceed.<br>
<br>
<div class="moz-cite-prefix">On 01/24/2017 05:52 AM, Sergei
Meshveliani wrote:<br>
</div>
<blockquote
cite="mid:1485265968.3562.2.camel@one.mechvel.pereslavl.ru"
type="cite">
<pre wrap="">On Tue, 2017-01-24 at 16:46 +0300, Sergei Meshveliani wrote:
</pre>
<blockquote type="cite">
<pre wrap="">On Mon, 2017-01-23 at 13:19 -0800, Martin Stone Davis wrote:
</pre>
<blockquote type="cite">
<pre wrap="">That does look like strange behavior yet I'm guessing this is not a bug.
Would you revise the problem example to be as small as possible and only
relying on the Agda.Builtin.*?
</pre>
</blockquote>
<pre wrap="">
See the .agda file attached.
</pre>
</blockquote>
<pre wrap="">
Sorry, I need to comment:
the version (II) there is type-checked,
and the commented version (I) is not.
------
Sergei
</pre>
<blockquote type="cite">
<pre wrap="">
</pre>
<blockquote type="cite">
<pre wrap="">On 01/23/2017 03:35 AM, Sergei Meshveliani wrote:
</pre>
<blockquote type="cite">
<pre wrap="">People,
I have further problems with matching in let+case+let.
Consider the following two fragments.
open OfMax natDTO using (Maximum; maximum′; maximum ...)
open Maximum using (max; all≤max)
-- Maximum is a record with constructor maximum′
...
--------------------------------------------------------- (I) ---
; (tri≈ _ e≡e' _) →
let
es = map proj₂ mons
maxStruc = maximum e (e' ∷ es) -- : Maximum (e ∷ e' ∷ es)
m = max maxStruc
ee'es≤m = all≤max maxStruc
e'es≡ees = PE.sym $ PE.cong (_∷ es) e≡e'
ord-ees = PE.subst DecrOrderedList e'es≡ees ord-e'es
ees≤m : All (_≤ m) (e ∷ es)
ees≤m = DPrelude.anything
in
((pol′ ((a + b , e) ∷ mons) ord-ees) , ees≤m)
------------------------------------------------------------------
----------------------------------------------------------- (II) ---
...
; (tri≈ _ e≡e' _) →
let
es = map proj₂ mons
in
case maximum e (e' ∷ es)
of \
{ (maximum′ m _ ee'es≤m) →
let
e'es≡ees = PE.sym $ PE.cong (_∷ es) e≡e'
ord-ees = PE.subst DecrOrderedList e'es≡ees ord-e'es
ees≤m : All (_≤ m) (e ∷ es)
ees≤m = DPrelude.anything
debug : All (_≤ m) (e ∷ e' ∷ es) -- for more testing
debug = ee'es≤m
in
((pol′ ((a + b , e) ∷ mons) ord-ees) , ees≤m)
}
----------------------------------------------------------------------
The difference is that in (I) the fields of the result of `maximum' are
extracted explicitly, by applying their labels. And in (II) their values
are found by matching against the record of the result.
(I) is type-checked.
And (II) leads to the report
------------------------
Cannot instantiate the metavariable _295 to solution All (λ section
→ section ≤ m) (e ∷ map proj₂ mons) since it contains the variable
m which is not in scope of the metavariable or irrelevant in the
metavariable but relevant in the solution
when checking that the expression ees≤m has type
_B_295 upComR a e b e' mons ord-e'es .¬a e≡e' .¬c
(pol′ ((a + b , e) ∷ mons)
(PE.subst DecrOrderedList
(PE.sym $ PE.cong (λ section → section ∷ map proj₂ mons) e≡e')
ord-e'es))
------------------------
in Agda 2.5.2.
This report refers to the line after last "in".
I also add the two "debug" lines to make sure that the value of m
is valid in the body of "in".
Does this effect show a bug in Agda?
(Generally, matching against a record makes many programs nicer).
Thank you in advance for explanation,
------
Sergei
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<pre wrap="">
_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>