Unsound use of Sized types in Environment module

[cmcl]

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?

[gallais]

Ah yes, that's an interesting one: in 2.6.1.3, Size is a Set like any other so
i : ?I (under the assumption ?I : Set) is accepted just fine and I is solved to
be Size. In 2.6.2, Size is not a Set anymore and so that unification cannot happen.

I suppose we could replace all the i of type I with σ and change the variable block
like so:

-    i σ : I
+    i : Size
+    σ : I