[Agda] strange let-in-case-let

[Sergei Meshveliani]

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