[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