[Agda] Suspicious normalisation

[Fredrik Nordvall Forsberg]

Dear Marko,

On 25/09/2020 12:00, Marko Dimjašević wrote:
> I cannot understand why can an expression
> 
>    ƛ′ two ⇒ two
> 
> be normalised (by running C-c C-n) at all for the code snippet below. It
> normalises to:
> 
>    ƛ′ `suc (`suc `zero) ⇒ (`suc (`suc `zero))

Note that the only reduction that has happened here is is that the two 
arguments has been replaced by their definition `suc (`suc `zero); in 
particular, the function ƛ′_⇒_ is stuck, and has not reduced, for two 
reasons:

1. its first argument does not match its only defining pattern (` x);
2. its implicit argument is still an unsolved meta, so its unknown if it 
matches its only defining pattern tt yet.

You can see more clearly what is going on either by toggling the display 
of implicit arguments in the Agda menu, in which case the "normalised" 
term is

ƛ′_⇒_ (`suc (`suc `zero)) {_19} (`suc (`suc `zero))

[here _19 is the unsolved meta of type ⊥]

or by writing the term as a definition in your source file, eg

test = ƛ′ two ⇒ two

in which case you can see the yellow highlighting because of the same 
unsolved meta.

You replied to Guillaume:
> I don't have anything highlighted in yellow due to the definition of ƛ′_⇒_.

Indeed, the definition of ƛ′_⇒_ is fine; it is in its use ƛ′ two ⇒ two 
that you have an unsolved implicit argument.

Best wishes,
Fred

> 
> module LambdaVar where
> 
> open import Data.Bool using (Bool; true; false; T)
> open import Data.String using (String)
> open import Data.Unit using (tt)
> 
> Id : Set
> Id = String
> 
> infix  5  ƛ_⇒_
> infix  8  `suc_
> infix  9  `_
> 
> data Term : Set where
>    `_                      :  Id → Term
>    ƛ_⇒_                    :  Id → Term → Term
>    `zero                   :  Term
>    `suc_                   :  Term → Term
> 
> 
> two : Term
> two = `suc `suc `zero
> 
> var? : Term → Bool
> var? (` _)  =  true
> var? _      =  false
> 
> ƛ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
> ƛ′_⇒_ (` x) {tt} N = ƛ x ⇒ N
> 
> 
> Shouldn't it be impossible to normalise ƛ′ two ⇒ two due to the implicit
> argument to ƛ′_⇒_ that doesn't allow Term t to be anything but a variable?