gallais / generic-syntax Goto Github PK

This is listed as the repo for the final version of the JFP paper:

https://gallais.github.io/publis.html

However, there is no JFP paper for this work. We've tried for well over a year now to contact all of you authors numerous times, creating a huge amount of work and overhead for us JFP staff. As of now, the paper has not been published and can't be.

I apologize for having to use this medium, but I'm hoping you are at least reading GitHub issues. What would it take to get one of you to respond to us?

Hi all,

I am looking to port the development to Agda v2.6.2 and standard library version 1.7. However, I encountered a type checking failure in the Data/Environment.agda module concerning the definition of data SEnv:

data SEnv (𝓥 : I ─Scoped) : Size → (Γ Δ : List I) → Set where
  [_]    : ∀{Γ} → ∀[ (Γ ─Env) 𝓥 ⇒ SEnv 𝓥 (↑ i) Γ ]
  _⊣_,,_ : ∀ Γ₂ {Γ₁} → ∀[ (Γ₂ ─Env) 𝓥 ⇒ ◇ (SEnv 𝓥 {!i!} Γ₁) ⇒ SEnv 𝓥 (↑ {!!}) (Γ₂ ++ Γ₁) ]

The problem snippet is (↑ i) and the remaining holes. In 2.6.2/v1.7, loading the file results in a type error because the type of i is I, not Size, and thus the typechecker generates a SizeUniv != Set error. However, Agda 2.6.1.3 only complains if you try to refine the goal with i producing the error:

generic-syntax/src/Data/Environment.agda:178,47-48
Generalizable variable Data.Environment.i is not supported here
when scope checking i

if, however, you place ↑ i directly in the type for [_] as in the above snippet and load the file, Agda 2.6.1.3 fails to complain that SizeUniv != Set.

Unless I misunderstand some use-case of Sized types and the known safety issues with their use, I cannot imagine this was intended. Should i : Size be the declaration of the generalized variable instead?