[Agda] Suspicious normalisation

[Marko Dimjašević]

Hi Guillaume,

On Fri, 2020-09-25 at 13:21 +0200, Guillaume Brunerie wrote:
> It seems perfectly reasonable to me that it reduces.
> The thing is that it has an unsolved implicit argument of type
> Data.Empty.⊥, so there would be unsolvable yellow if you try to use this
> term in a consistent context, but there is no reason why that should
> prevent it from normalizing.


Why is it an unsolved argument?

Perhaps I could use some reading on solving (implicit) arguments, but my
understanding is that the type becomes either Data.Empty.⊥ or Data.Unit.⊤
and at that point it should be clear if the first explicit argument to
function ƛ′_⇒_ is valid or not.

I don't have anything highlighted in yellow due to the definition of ƛ′_⇒_.
The only place where it is actually used is in a definition of plus′, for
which you'd need the full version of Term [1]:

plus′ : Term
plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
          case′ m
            [zero⇒ n
            |suc m ⇒ `suc (+ · m · n) ]
  where
  +  =  ` "+"
  m  =  ` "m"
  n  =  ` "n"


This type-checks and loads just fine.


> Depending on your use case, maybe you can use an instance argument
> instead of an implicit argument, this way it will fail instead of
> reducing, but work when the first argument is a variable.


Thank you for the suggestion! I tried using an instance argument, but the
outcome is the same: everything type-checks just fine and there are no
yellow highlights.


[1] Use the definition of Term as in https://plfa.github.io/Lambda/


-- 
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
Mastodon: https://mamot.fr/@mdimjasevic
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200927/0fdb7f0e/attachment.sig>