Cubical Agda crashes when printing empty system

[kangrongji]

The follwing codes type-checks well:

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

open import Agda.Primitive
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' : Level

-- The `contr` operator in [CCHM] 5.1.

Contr : Type ℓ → SSet ℓ
Contr X = {φ : I}(u : Partial φ X) → X [ φ ↦ u ]

Contr→isContr : {X : Type ℓ} → Contr X → isContr X
Contr→isContr contr .fst = outS (contr empty)
Contr→isContr contr .snd x i = outS (contr (λ { (i = i0) → outS (contr empty) ; (i = i1) → x }))

isContr→Contr : {X : Type ℓ} → isContr X → Contr X
isContr→Contr iscontr {φ = φ} u = inS (hcomp (λ i → λ { (φ = i1) → iscontr .snd (u 1=1) i }) (iscontr .fst))

-- The `equiv` operator in [CCHM] 5.3.

Equiv : {X : Type ℓ}{Y : Type ℓ'}(f : X → Y) → SSet (ℓ-max ℓ ℓ')
Equiv {X = X} {Y = Y} f = {y : Y}{φ : I}(p : Partial φ (fiber f y)) → fiber f y [ φ ↦ p ]

open isEquiv

Equiv→isEquiv : {X : Type ℓ}{Y : Type ℓ'}{f : X → Y} → Equiv f → isEquiv f
Equiv→isEquiv equiv .equiv-proof _ = Contr→isContr equiv

isEquiv→Equiv : {X : Type ℓ}{Y : Type ℓ'}{f : X → Y} → isEquiv f → Equiv f
isEquiv→Equiv isequiv {y = y} = isContr→Contr (isequiv .equiv-proof _)

EquivId : {X : Type ℓ} → Equiv (idEquiv X .fst)
EquivId = isEquiv→Equiv (idEquiv _ .snd)

-- Proof of univalence axiom using Glue type, c.f. [CCHM] 7.2.

module _
  {Y : Type ℓ'}{φ : I}
  (Te : Partial φ (Σ[ X ∈ Type ℓ ] X ≃ Y))
  where

  EquivUnglue : Equiv {X = Glue Y Te} (unglue φ)
  EquivUnglue {y = y} {φ = ψ} p = inS (u , v)
    where
    extend : (φ=1 : IsOne φ) → Equiv (Te φ=1 .snd .fst)
    extend φ=1 = isEquiv→Equiv (Te φ=1 .snd .snd)

    ext : Partial φ (Glue Y Te)
    ext (φ = i1) = outS (extend 1=1 p) .fst

    ext-path : I → Partial (φ ∨ ψ) Y
    ext-path i (φ = i1) = outS (extend 1=1 p) .snd (~ i)
    ext-path i (ψ = i1) = p 1=1 .snd (~ i)

    u : Glue Y Te
    u = glue ext (hcomp ext-path y)

    v : unglue φ u ≡ y
    v i = hfill ext-path (inS y) (~ i)

  isEquivUnglue : isEquiv (unglue φ)
  isEquivUnglue = Equiv→isEquiv EquivUnglue

  unglueEquiv : (Glue Y Te ≃ Y) [ _ ↦ (λ { (φ = i1) → Te 1=1 .snd }) ]
  unglueEquiv =
    inS (_ , hcomp (λ i → λ
      { (φ = i1) → isProp→PathP (λ i → isPropIsEquiv _) isEquivUnglue (Te 1=1 .snd .snd) i })
    isEquivUnglue)

  GlueEquiv : (Σ[ X ∈ Type ℓ ] X ≃ Y) [ φ ↦ Te ]
  GlueEquiv = inS (_ , outS unglueEquiv)

isContrEquiv : (Y : Type ℓ) → isContr (Σ[ X ∈ Type ℓ ] X ≃ Y)
isContrEquiv Y = Contr→isContr GlueEquiv

-- J rule for equivalences

JEquiv :
  {ℓ ℓ' : Level}{Y : Type ℓ}
  (P : (X : Type ℓ) → X ≃ Y → Type ℓ')
  (p : P _ (idEquiv _))
  {X : Type ℓ}(e : X ≃ Y) → P _ e
JEquiv P p e =
  subst (λ x → P (x .fst) (x .snd)) (isContr→isProp (isContrEquiv _) (_ , idEquiv _) (_ , e)) p

But when I try to normalize JEquiv (by C-c C-n), an error occurs:

NonEmpty.fromList: empty list

Agda thought some lists must be non-empty, and it turns out not that case :)

[dolio]

Here's a shorter way to trigger (probably) the same error.

module Whatever where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

p : I → Type₁
p i = Glue Type (λ { (i = i0) → (Type , idEquiv _) })

P : Type ≡ Glue Type _
P i = p i

Filling it in to:

P : Type ≡ Glue Type {i0} (λ())
P i = p i

avoids the error. So it probably has something to do with inferring the empty system.

[andreasabel]

Thanks for the smaller reproducer!
The crash happens here:

agda/src/full/Agda/Syntax/Translation/InternalToAbstract.hs

Lines 822 to 823 in 5d30d8e

	elims (A.ExtendedLam exprNoRange dInfo erased x $
	List1.fromList cls)

This means that an extended lambda without clauses is generated somewhere.

[andreasabel]

Fixed in #5994 by reifying empty systems to absurd lambdas.