Termination checker still incompatible with univalence

[andreasabel]

Reported by @Saizan. Lifted from:

• Coinduction incompatible with univalence [WAS: Structural termination order incompatible with univalence] #1023 (comment)

{-# OPTIONS --without-K #-}

data Zero : Set where

data Id (X : Set) : Set where
  i : X → Id X

mutual
  data WOne : Set where wrap : Id FOne -> WOne
  FOne = Zero -> WOne

data _<->_ (X : Set) : Set -> Set₁ where
  Refl : X <-> X

postulate
  iso : WOne <-> FOne

mutual
  noo : (X : Set) -> (WOne <-> X) -> Id X -> Zero
  noo .WOne Refl (i (wrap f)) = noo FOne iso f

absurd : Zero
absurd = noo FOne iso (i \ ())

[nad]

I don't know why this was not labelled with false. It is easy to flesh out the example into one that type-checks with --erased-cubical --safe.

[andreasabel]

NB: Since this reproducer does a match of Refl, it should not be portable to Cubical Agda. However, I don't know enough to state this with certainty.

@nad wrote:

I don't know why this was not labelled with false. It is easy to flesh out the example into one that type-checks with --erased-cubical --safe.

Could you please do this? Currently we cannot place the safe label here, being short of a reproducer.

[szumixie]

Path can be converted to <->, so it still works in Cubical Agda:

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

data Zero : Set where

data Id (X : Set) : Set where
  i : X → Id X

mutual
  data WOne : Set where wrap : Id FOne -> WOne
  FOne = Zero -> WOne

data _<->_ (X : Set) : Set -> Set₁ where
  Refl : X <-> X

isom : Iso WOne FOne
isom =
  iso
    (λ _ ())
    (λ f → wrap (i f))
    (λ _ → funExt λ ())
    (λ { (wrap (i _)) → cong (λ f → wrap (i f)) (funExt λ ()) })

eq : WOne <-> FOne
eq = subst (λ X → WOne <-> X) (isoToPath isom) Refl

noo : (X : Set) -> (WOne <-> X) -> Id X -> Zero
noo .WOne Refl (i (wrap f)) = noo FOne eq f

absurd : Zero
absurd = noo FOne eq (i \ ())

[andreasabel]

Thanks, @szumixie !

[anuyts]

mutual
  noo : (X : Set) -> (WOne <-> X) -> Id X -> Zero
  noo .WOne Refl (i (wrap f)) = noo FOne iso f

The pattern Refl forces X to be WOne, which may cause transport of any arguments whose type mentions X. By univalence, transport may involve arbitrarily complex functions. Indeed, the recursive call noo FOne iso f really boils down to noo WOne Refl (iso* f) (where iso* is a quick notation for transport). In order to make sure that the induction is structural, we need to ensure that the transport commutes with the nesting of constructors that we're peeling off. For example, if iso*(f) = i (wrap g), i.e. f = isoinv*(i (wrap g)), then we know by definition of transport of parametrized inductive types that

f = isoinv* (i (wrap g)) = i (isoinv* (wrap g))

However, we cannot commute isoinv* with wrap. As such, the nesting i (wrap [hole]) does not commute with transport w.r.t. X, and therefore should not qualify as proof of structural induction.
I'm confused what to do with indices (transport along an index creates an hcomp transport constructor), but as far as parameters are concerned, I think this paradox might be solved by requiring i (wrap [hole]) to be well-typed for X a variable, i.e. before equating it to WOne (but maybe after generalizing it from another more concrete expression).

[anuyts]

It seems for indices, the necessary checks are in place?

{-# OPTIONS --cubical-compatible #-}

data E1 : Set where

data E2 : Set where

data Indexed : Set → Set₁ where
  e2 : Indexed E2

data _<->_ (X : Set) : Set -> Set₁ where
  Refl : X <-> X

oops : (X : Set) → X <-> E1 → Indexed X → Set
oops .E1 Refl i = {!!}

Pattern match on i:

I'm not sure if there should be a case for the constructor e2,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  E2 ≟ E1
when checking that the expression ? has type Set

although if you ask me it should bind a transport pattern.

[anuyts]

Intriguingly (to me at least), this already raises a termination error:

{-# OPTIONS --without-K #-}

data Zero : Set where

record Unit : Set where
  constructor tt

data Id (X : Set) : Set where
  i : X → Id X

data _<->_ (X : Set) : Set -> Set₁ where
  Refl : X <-> X

postulate
  iso : ∀{X} → Id X <-> X

noo : (X Y : Set) -> (Id X <-> Y) -> Y -> Zero
noo X .(Id X) Refl (i x) = noo X X iso x

absurd : Zero
absurd = noo Unit Unit iso tt

Termination checking failed for the following functions:
  noo
Problematic calls:
  noo X X iso x

[andreasabel]

Intriguingly (to me at least), this already raises a termination error:

Likely because there is a workaround in place for #1023, but it was shown to be incomplete in the current issue.

[andreasabel]

This isn't a problem with --type-based-termination.
Proposal: disallow --syntax-based-termination when --cubical and --safe are on. (Or at least warn.)

[nad]

Proposal: disallow --syntax-based-termination when --cubical and --safe are on. (Or at least warn.)

The new type-based termination checker has not been released yet. I don't think we should "force" people to use it before it has seen considerable use.