[Agda] strange let-in-case-let
Martin Stone Davis
martin.stone.davis at gmail.com
Wed Jan 25 03:50:44 CET 2017
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:
case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x
postulate
anything : ∀ {a} {A : Set a} → A
X : Set
F : X → Set
record R : Set where
constructor c
field
r : X
postulate
s : R
foo : (r : R) → F (R.r r)
foo _ = anything
bar1 : F (R.r s)
bar1 = let c x = s in
let letted : F x
letted = anything in
{!letted!} -- works. notice that "Have" and "Goal" match
bar2 : F (R.r s)
bar2 = case s of λ {(c x) →
let letted : F x
letted = anything in
{!letted!}} -- does not work because Have: F x, but Goal: F (R.r s)
One way to get around your problem borrows from an idea I posted here
<https://github.com/agda/agda/issues/426#issuecomment-254111273>. We
encourage Agda to "remember" that s = c x:
open import Agda.Builtin.Equality
record Memoized {A : Set} (x : A) : Set where
constructor _,_
field
value : A
sound : value ≡ x
remember : {A : Set} → (x : A) → Memoized x
remember x = x , refl
bar2a : F (R.r s)
bar2a = case remember s of λ {(c x , refl) →
let letted : F x
letted = anything in
{!letted!}} -- works
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.
On 01/24/2017 05:52 AM, Sergei Meshveliani wrote:
> On Tue, 2017-01-24 at 16:46 +0300, Sergei Meshveliani wrote:
>> On Mon, 2017-01-23 at 13:19 -0800, Martin Stone Davis wrote:
>>> 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.*?
>>>
>> See the .agda file attached.
>
> Sorry, I need to comment:
>
> the version (II) there is type-checked,
> and the commented version (I) is not.
>
> ------
> Sergei
>
>
>
>>> On 01/23/2017 03:35 AM, Sergei Meshveliani wrote:
>>>> 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
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170124/d4d9a800/attachment.html>
More information about the Agda
mailing list