[Agda] Suspicious normalisation

[Marko Dimjašević]

Dear Agda community,

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))


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?


-- 
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/20200925/0149141f/attachment.sig>