[Agda] strange let-in-case-let

[Martin Stone Davis]

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.*?


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