Equality is incompatible with sized types

[andreasabel]

open import Size
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe

data ⊥ : Set where

data SizeLt (i : Size) : Set where
  [_] : (j : Size< i) → SizeLt i

module OneSize where 

  eq! : ∀ (i j : Size) → i ≡ j
  eq! _ _ = trustMe

  cast : ∀ i j → SizeLt i → SizeLt j
  cast i j = subst SizeLt (eq! i j)

  foo : ∀ i → SizeLt i → ⊥
  foo i [ j ] = foo j (cast i j [ j ])

  test : ⊥
  test = foo ∞ [ ∞ ]

The term test is looping.

[Saizan]

Without using trustMe, but proofs of equality to \infty instead.

open import Size
open import Relation.Binary.PropositionalEquality

data ⊥ : Set where

data SizeLt (i : Size) : Set where
  [_] : (j : Size< i) → SizeLt i

get : ∀ {i} → SizeLt i → Size
get [ j ] = j

module OneSize where

  eq! : ∀ (i j : Size) → i ≡ ∞ → j ≡ ∞ → i ≡ j
  eq! _ _ refl refl = refl

  cast : ∀ i j → i ≡ ∞ → j ≡ ∞ → SizeLt i → SizeLt j
  cast i j i∞ j∞ = subst SizeLt (eq! i j i∞ j∞)

  cast-∞ : ∀ i (j : SizeLt i)
           (i∞ : i ≡ ∞) (j∞ : get j ≡ ∞) →
            get (cast i (get j) i∞ j∞ j) ≡ ∞
  cast-∞ _ [ _ ] refl refl = refl

  foo : ∀ i → (j : SizeLt i) → i ≡ ∞ → get j ≡ ∞ → ⊥
  foo i [ j ] i∞ j∞ = foo j
                          (cast i j i∞ j∞ [ j ])
                          j∞
                          (cast-∞ i [ j ] i∞ j∞)

  test : ⊥
  test = foo ∞ [ ∞ ] refl refl

[andreasabel]

And the slightly dubious get function... Is this related to #1428?

[Saizan]

Isn't ∞ : Size< ∞ the most dubious part here? :)

[Saizan]

Without using the get function:

open import Size
open import Relation.Binary.PropositionalEquality

data ⊥ : Set where

data SizeLt∞ (i : Size) : Set where
  [_,_] : (j : Size< i) → j ≡ ∞ → SizeLt∞ i

module OneSize where

  cast : ∀ i j → i ≡ ∞ → j ≡ ∞ → SizeLt∞ i → SizeLt∞ j
  cast i j refl refl [ k , eq ] = [ k , eq ]

  foo : ∀ i → (j : SizeLt∞ i) → i ≡ ∞ → ⊥
  foo i [ j , j∞ ] i∞ = foo j (cast i j i∞ j∞ [ j , j∞ ]) j∞

  test : ⊥
  test = foo ∞ [ ∞ , refl ] refl

[UlfNorell]

Time to bring back the size universe?

[andreasabel]

The trouble with SizeUniv was that since the introduction of universe polymorphism much of the sort machinery relies on the fact that we have a linear hierarchy of sorts. This needs to be refactored properly to accommodate other PTSs than {Set i | i in Nat}.

[UlfNorell]

Without standard library

open import Agda.Builtin.Size renaming (ω to ∞)
open import Agda.Builtin.Equality

data ⊥ : Set where

data SizeLt∞ (i : Size) : Set where
  [_,_] : (j : Size< i) → j ≡ ∞ → SizeLt∞ i

cast : ∀ i j → i ≡ ∞ → j ≡ ∞ → SizeLt∞ i → SizeLt∞ j
cast i j refl refl [ k , eq ] = [ k , eq ]

foo : ∀ i → (j : SizeLt∞ i) → i ≡ ∞ → ⊥
foo i [ j , j∞ ] i∞ = foo j (cast i j i∞ j∞ [ j , j∞ ]) j∞

test : ⊥
test = foo ∞ [ ∞ , refl ] refl

[nad]

And the slightly dubious get function...

Is the following code not supposed to work?

------------------------------------------------------------------------
-- Size elimination

-- A trick is used to implement size elimination. This trick was
-- suggested to me by Andrea Vezzosi.

-- A data type wrapping Size<_.
--
-- If this wrapper is removed from the definition of elim below, then
-- that definition is rejected.

data [Size<_] (i : Size) : Set where
  box : Size< i → [Size< i ]

-- A projection.

unbox : ∀ {i} → [Size< i ] → Size< i
unbox (box j) = j

-- Size elimination.

elim :
  ∀ {p}
  (P : Size → Set p) →
  (∀ i → ((j : [Size< i ]) → P (unbox j)) → P i) →
  ∀ i → P i
elim P f i = f i λ { (box j) → elim P f j }

[nad]

The fact that ∞ : Size< ∞ seems to be problematic. Is this a fundamental problem, or can the problem be contained by, say, letting sizes live in a separate universe (so that we cannot talk about equality of sizes, for instance)?

[Saizan]

Avoiding equality of sizes does not seem to be enough, though if we would only allow irrelevant size quantification in datatypes it might. (Personally I'd rather get rid of ∞ : Size< ∞ ! But it's not like I have a design ready either)

open import Agda.Builtin.Size renaming (ω to ∞)
open import Agda.Builtin.Equality

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst                                                                                                                    

data ⊥ : Set where

data Nat (i : Size) : Set where
  zero : ∀ (j : Size< i) → Nat i
  suc : ∀ (j : Size< i) → Nat j → Nat i

data SizeLt (i : Size) : Set where
  [_] : (j : Size< i) → SizeLt i

SizeLt∞ : (i : Size) → Set
SizeLt∞ i = Σ (SizeLt i) \ { [ j ] → zero j ≡ zero ∞ }

Type : Size → Nat ∞ → Set
Type i (zero j) = SizeLt∞ i → SizeLt∞ j
Type i (suc j _) = SizeLt∞ i → SizeLt∞ j

cast : ∀ i (n : Nat ∞) → n ≡ zero ∞ → Type i n
cast i .(zero ∞) refl ([ k ] , eq) = [ k ] , eq

foo : ∀ i → (j : SizeLt∞ i) → ⊥
foo i ([ j ] , j∞) = foo j (cast i (zero j) j∞ ([ j ] , j∞))

test : ⊥
test = foo ∞ ([ ∞ ] , refl)

[nad]

Andreas and I briefly discussed removing ∞ : Size< ∞ the other day. As I recall the main problem is that the force projection would no longer have type D′ ∞ → D ∞. (For a typical coinductive definition involving a data type D and a coinductive record type D′ with a field force : {j : Size< i} → D j.)

[nad]

One way to think about sized types, that might not be entirely compatible with the current implementation, is that there are two kinds of definitions: those that have (possibly) not been completed yet (of size i), and completed definitions (of size ∞). Once a definition has been completed it should be fine to ignore all sizes, and it should also be fine to turn a completed definition into a potentially incomplete one.

[nad]

As I recall the main problem is that the force projection would no longer have type D′ ∞ → D ∞.

I guess it would help if the isomorphism between D′ ∞ and D′ (ssuc ∞) was available to the programmer in some way.

[jespercockx]

I see two options here to go forward:

• Bring back SizeUniv (which should actually be doable now)
• Remove / restrict ∞ < ∞

[nad]

Would a size universe fix all problems with ∞ < ∞?

[nad]

@Saizan suggested the following approach: Get rid of ∞ < ∞, but support it via special typing rules for certain projections/constructors for which it makes sense (like the typical construction with a force projection, but perhaps not the Thunk type used by the standard library).

@Saizan, could you define more explicitly what "makes sense" means?

[jespercockx]

Would a size universe fix all problems with ∞ < ∞?

I don't think so.

[Saizan]

@nad here's a first approximation.

We should recognize for which sized types we have F ∞ = F (∞ +1) so that we can "downcast" as needed.

Typically it would be (co)inductive record/data types that follow the usual pattern of having recursive occurrences at a smaller size. We should implement some checker for this, possibly quite close to the one that enables size subtyping.

Then e.g. for a typical coinductive type

mutual
  data D (i : Size) : Set where
     con : (x : S) -> (P x -> R i) -> D i
  record R (i : Size) : Set where
     coinductive
     force : (j : Size< i) -> D j

We would have to also allow force {∞} : R ∞ -> (j : Size< (∞ +1)) -> D j

Dually for constructors

mutual
  data W (i : Size) : Set where
     sup : (j : Size< i) (x : S) -> (P x -> W j) -> W i

we also have sup {∞} : (j : Size< (∞ +1)) -> (x : S) -> (P x -> W j) -> W ∞.

The way this is specified in the ICFP13 paper is to use "bound normalization": a meta operation "bnm(s)" such that bnm(s) = ∞ +1 whenever s = ∞ or higher, and otherwise just s. Then have the following typing rule

sup {s} : (j : Size< bnm(s)) -> (x : S) -> (P x -> W j) -> W s

[nad]

I think you inadvertently used too much shadowing in the rule.

Should this typing rule be used everywhere, both in patterns and in expressions?

[Saizan]

Fixed the shadowing.

Yes, it should be used both in patterns and in expressions.

There's still a mismatch with the ICFP13 paper, because of the difference between \forall, \exists and \Pi, \Sigma. I wonder if that's exploitable.

[nad]

Could you be a little more explicit about this mismatch?

[Saizan]

In Agda we can project the j out of a Nat i like so

data Nat (i : Size) : Set where
  zero : (j : Size< i) → Nat i
  suc : (j : Size< i) → Nat j → Nat i

f : ∀ {i} → Nat i → Size
f (zero j  ) = j
f (suc  j _) = j

which is not possible in the ICFP13 paper, because it's an extension of System F and Size is just a kind. In turn quantification over sizes is modeled by union/intersection and I believe this is necessary to reach a fixpoint.

The above is in line with the fact that those (j : Size< i) -> ... should be irrelevant quantifications, and Nat should be shape-irrelevant.

[nad]

Does coinduction have similar (potential) problems?

I guess the definition of f could be prevented through the use of a special size universe.

Is shape-irrelevance well-understood now?

[nad]

I discussed this with @Saizan now, and he mentioned that bnm does not commute with substitution. This makes me wonder whether this construction breaks subject reduction. @andreasabel?

[jespercockx]

I guess nothing will happen with the sized types situation before the release, which is unfortunate but understandable because:

1. We have a lot of other new features that are ready to be released
2. The current situation is not any worse than with the previous releases

So I will just bump this and other sized-types issues to the next release. Hopefully we'll get a fix soon...

[JLimperg]

For the record: Getting rid of ∞ < ∞ is not enough since it also follows from ∞ = ∞ + 1 together with i < i + 1.

module _ where

open import Size
open import Induction.WellFounded

data _<_ : Size → Size → Set where
  gt : ∀ (i : Size) (j : Size< i) → j < i

<-suc : (i : Size) → i < (↑ i)
<-suc i = gt (↑ i) i

∞<∞ : ∞ < ∞
∞<∞ = <-suc ∞

-- The rest of the proof is from #3026

data ⊥ : Set where

<-wf : WellFounded _<_
<-wf i = acc (go i)
  where
    go : ∀ (i j : Size) → (j < i) → Acc _<_ j
    go i j (gt .i j') = <-wf j

acc-∞ : Acc _<_ ∞
acc-∞ = <-wf ∞

foo : Acc _<_ ∞ → ⊥
foo (acc a) = foo (a ∞ ∞<∞)

bad : ⊥
bad = foo acc-∞

[Saizan]

Right, what's actually possibly sound is that Nat ∞ = Nat (∞ + 1), though that might still be problematic.

[JLimperg]

Afaict, the question of when it's safe to instantiate a size variable with ∞ is already discussed in Hughes' original paper, Sec. 3.7. I don't yet understand the details, but we may find inspiration there.

[JoeyEremondi]

Just to make sure I'm understanding what's going on here, does this mean that --sized makes Agda inconsistent even with --safe enabled? I knew that it was incompatible with guardedness but this is new to me.

[JLimperg]

As of 2.6.1, the proof of False given above compiles with {-# OPTIONS --safe --sized #-}. This looks like a --safe bug to me.

[nad]

Yes, one could argue that --safe is broken due to this problem. We could fix it by not allowing --sized-types when --safe is active, but this would break quite a bit of code. It might be better to fix this issue (even if the fix also breaks code).

Contributions are welcome!

[JLimperg]

It would certainly be nice if this issue could be fixed, but I don't see that happening quickly. It's a problem with the axioms (i.e. not just a technicality), has been known for years, and despite some efforts from various people, there's no clear plan for fixing it. (If I had an idea, I'd gladly implement it.)

In the meantime, I would advocate for updating --safe and especially the docs (which afair don't mention this issue). The resulting breakage can be fixed by removing --safe from affected projects, which reflects the reality of the situation -- sized types are currently unsafe. Anything else is imo not a good look for the safe fragment of a theorem prover.

[nad]

I don't think we should disable --sized-types in safe mode until #3118 has been fixed.

[Saizan]

@JLimperg what do you think of the design I sketched above, based on the ICFP13 paper? i.e. getting rid of oo < oo and oo + 1 = oo and instead rely on the typing with bnm(_) for constructors.

[nad]

I'd just like to note that the problems are not restricted to Size<_. Here is a variant of the example that @JLimperg posted above:

{-# OPTIONS --safe --sized-types #-}

open import Agda.Builtin.Size
open import Induction.WellFounded

data _<_ : Size → Size → Set where
  <-suc : (i : Size) → i < (↑ i)

∞<∞ : ∞ < ∞
∞<∞ = <-suc ∞

data ⊥ : Set where

<-wf : WellFounded _<_
<-wf i = acc λ { j (<-suc .j) → <-wf j }

acc-∞ : Acc _<_ ∞
acc-∞ = <-wf ∞

¬-acc-∞ : Acc _<_ ∞ → ⊥
¬-acc-∞ (acc a) = ¬-acc-∞ (a ∞ ∞<∞)

bad : ⊥
bad = ¬-acc-∞ acc-∞

[andreasabel]

Here is a variant of https://github.com/agda/agda/issues/2820#issuecomment-503639453 that uses Size< as a set and ↑∞ = ∞:

open import Agda.Builtin.Size

data _<_ : Size → Size → Set where
  gt : ∀ (i : Size) (j : Size< i) → j < i

∞<↑∞ : ∞ < (↑ ∞)
∞<↑∞ = gt (↑ ∞) ∞

data ⊥ : Set where

data Acc (i : Size) : Set where
  acc : (∀ j → j < i → Acc j) → Acc i

<-wf : ∀ (i j : Size) → j < i → Acc j
<-wf i j (gt .i .j) = acc (<-wf j)  -- By unification, we get j : Size< i

acc-∞ : Acc ∞
acc-∞ = <-wf (↑ ∞) ∞ ∞<↑∞

∞<∞ : ∞ < ∞
∞<∞ = ∞<↑∞  -- Uses ↑∞ = ∞ (or, equivalently, ∞ < ∞)

foo : Acc ∞ → ⊥
foo (acc f) = foo (f ∞ ∞<∞)  -- Structural recursion, does not use sized types.

bad : ⊥
bad = foo acc-∞

Besides ∞ < ∞, the questionable parts are the definition of data type _<_ and pattern matching on it in <-wf. Concerning the second of these: the termination checker needs to more carefully establish that there is always a witness for j < i. Usually, this comes from matching on something inductive or comatching on something coinductive whose size is i (and the size of the respective substructures is j).

Note that this simplification is rejected by the termination checker:

  data Acc (i : Size) : Set where
    acc : (∀ (j : Size< i) → Acc j) → Acc i

  <-wf : ∀ i (j : Size< i) → Acc j
  <-wf i j = acc (<-wf j)

Thus, the wrapping of Size< into a data type successfully fools the termination checker.

(Note sure about this: One could also blame the unifier that it refines the type Size of j to Size< i without warning the termination checker.)