Agsy/Auto crashes with Prelude.!!: index too large

[Trebor-Huang]

When trying to formalize some very dependent inductive-recursive types, Agda crashes when trying to C-c C-a a hole:

data Context : Set
data Type : Context -> Set
data Var : ∀ Γ -> Type Γ -> Set

variable
    Γ Δ Ξ : Context
    α β : Type Γ

data Context where
    ∅ : Context
    _◂_ : ∀ Γ -> Type Γ -> Context
infixl 5 _◂_

data Type where
    ⋆ : Type Γ
    var : Var Γ ⋆ -> Type Γ
    Π_ : Type (Γ ◂ ⋆) -> Type Γ
    _⇒_ : Type Γ -> Type Γ -> Type Γ

data Ren : Context -> Context -> Set
rent : Ren Δ Γ -> Type Γ -> Type Δ  -- renaming on types
𝔭 : Ren (Γ ◂ α) Γ

data Ren where
    stop : Ren ∅ ∅
    drop : Ren Γ Δ -> Ren (Γ ◂ α) Δ
    keep : (ρ : Ren Γ Δ) -> Ren (Γ ◂ rent ρ α) (Δ ◂ α)

data Var where
    𝔮 : Var (Γ ◂ α) (rent 𝔭 α)
    𝕤_ : Var Γ α -> Var (Γ ◂ β) (rent 𝔭 α)

fetch : (ρ : Ren Γ Δ) -> Var Δ α -> Var Γ (rent ρ α)
fetch ρ 𝔮 = {!   !}  -- Here
fetch ρ (𝕤 i) = {!   !}

rent ρ ⋆ = ⋆
rent ρ (var i) = {!   !} -- var (fetch ρ i)
rent ρ (Π t) = Π {!   !}
rent ρ (t ⇒ s) = rent ρ t ⇒ rent ρ s

The hole is marked with --Here. However, if the hole below in rent is filled with the expression in the comment then the issue disappears.

Agda version: v2.6.2.1-af5bfc0 installed with cabal. I'm using OS X, on VSCode.

[nad]

I replaced every (?) occurrence of (Prelude.!!) with a new function that provides better error messages. The following call to (!!) uses an index that is out of bounds:

agda/src/full/Agda/Auto/Typecheck.hs

Line 25 in cf7ea79

return (weak (v + 1) (snd $ ctx !! v), id)

[nad]

The comment on the previous line looks suspicious to me:

agda/src/full/Agda/Auto/Typecheck.hs

Lines 24 to 25 in cf7ea79

	Var v -> -- assuming within scope
	return (weak (v + 1) (snd $ ctx !! v), id)

Perhaps one could simply fail if the variable is out of scope.

[andreasabel]

Amelia, I unassigned you since you have enough on your plate already, and this issue doesn't require your expertise.

[andreasabel]

Perhaps one could simply fail if the variable is out of scope.

This is what I implemented.