Composition of Glue Type Causes Infinite Loop

[kangrongji]

I try to type-check the following codes, which is no more than comp for Glue:

{-# OPTIONS --cubical --safe #-}
module Test where

open import Agda.Primitive
open import Cubical.Core.Everything

compGlue :
  {ℓ ℓ' : Level}{Y : I → Type ℓ'}
  {φ : I → I}(Te : (i : I) → Partial (φ i) (Σ[ X ∈ Type ℓ ] X ≃ Y i))
  {ψ : I}(x : (i : I) → Partial ψ (Glue (Y i) (Te i)))(x₀ : Glue (Y i0) (Te i0) [ ψ ↦ x i0 ])
  → Glue (Y i1) (Te i1) [ ψ ↦ x i1 ]
compGlue {Y = Y} {φ} Te {ψ} x x₀ = comp (λ i → Glue (Y i) (Te i)) x (outS x₀)

Unfortunately no result comes out, but an error shows agda: Heap exhausted (I was using the default 3.6G setting). I enlarge the memory to 10G, then the memory is used up in seconds and I decide to just close it. It seems the type-checker doesn't halt (or it needs an absurd amount of memory).

Btw, the code shouldn't pass the tyck, so I anticipate an error message about incorrect types.

[kangrongji]

Oh, I think the problem is related to {φ : I → I}. It's all well if replace it by a constant {φ : I}.

[andreasabel]

Here is a version without the cubical library:

{-# OPTIONS --cubical --safe #-}

open import Agda.Primitive            renaming (Set to Type)
open import Agda.Primitive.Cubical    renaming (primComp to comp)
open import Agda.Builtin.Sigma
open import Agda.Builtin.Cubical.Sub  renaming (primSubOut to outS)
open import Agda.Builtin.Cubical.Glue using    (primGlue; _≃_)

Glue : ∀ {ℓ ℓ'} (A : Type ℓ) {φ : I}
       → (Te : Partial φ (Σ (Type ℓ') (_≃ A)))
       → Type ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

compGlue :
  {ℓ ℓ' : Level}
  (Y    : I → Type ℓ')
  (φ    : I → I)
  (Te   : (i : I) → Partial (φ i) (Σ (Type ℓ) (_≃ Y i)))
  (ψ    : I)
  (x    : (i : I) → Partial ψ (Glue (Y i) (Te i)))
  → Sub (Glue (Y i0) (Te i0)) ψ (x i0)
  → Sub (Glue (Y i1) (Te i1)) ψ (x i1)

compGlue Y φ Te ψ x x₀ = comp (λ i → Glue (Y i) (Te i)) x (outS x₀)

Agda seems to recursively revisit the problem:

  outS x₀ = x i0 _ : primGlue (Y i0) (λ .x₁ → Te i0 _ .fst) (λ .x₁ → Te i0 _ .snd)

This seems to be a regression in 2.6.2, since 2.6.1 answers:

primGlue (Y i1) (λ .x₁ → Te i1 _ .fst) (λ .x₁ → Te i1 _ .snd) 
  !=< 
  Sub (Glue (Y i1) (Te i1)) ψ (x i1)
when checking that the expression
comp (λ i → Glue (Y i) (Te i)) x (outS x₀) has type
  Sub (Glue (Y i1) (Te i1)) ψ (x i1)

[andreasabel]

Bisection blames ae31526 (ping @Saizan)
Date: Thu Feb 4 10:36:02 2021 +0100
[ fix #4949 ] Use the right type when comparing glue elements

Command used:

agda-bisect --with-cabal=cabal-3.2 -w ghc-8.8.4 --good v2.6.1 --bad v2.6.2 Issue5955.agda \
  --must-fail --timeout 15 --cabal-option '--ghc-option=-O0'