gallais
Unsound use of Sized types in Environment module
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?
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
