Strong normalization broken in an open context

[GoogleCodeExporter]

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

unfoldaux : (f : ∀ i → Nat i) → ∀ i → Nat i → Set1
unfoldaux f i zero = Set
unfoldaux f i (suc j n) = unfoldaux f j (f j)

Original issue reported on code.google.com by sanzhi...@gmail.com on 10 Feb 2015 at 7:24

[GoogleCodeExporter]

But this does not break normalization!

Original comment by andreas....@gmail.com on 10 Feb 2015 at 7:27

[GoogleCodeExporter]

Is this a problem?

unfoldauxNat' : (f : ∀ i → Nat i) → ∀ i → Set1
unfoldauxNat' f i = unfoldauxNat f i (f i)

problem : (f : ∀ i → Size< i) (g : ∀ i → Nat (f i)) → ∀ i → Set1
problem f g i = unfoldauxNat' (\ i → suc (f i) (g i)) i

Original comment by sanzhi...@gmail.com on 10 Feb 2015 at 7:35

[GoogleCodeExporter]

open import Common.Size
open import Common.Prelude

data Wrap (A : Set) : Set where
  wrap : A → Wrap A

module M (f : ∀ i → Wrap (Size< i)) where

  test : ∀ i → Wrap (Size< i) → ⊥
  test i (wrap j) = test j (f j)

module N (g : ∀ i → Size< i) where

  open M (λ i → wrap (g i))

  loop : Size → ⊥
  loop i = test i (wrap (g i))

-- module N's code leaves size constraint  (↑ g i) =< i : Size open, which should hold.
-- Thus, we almost loop. 

A culprit seems to be that Size : Set. It should live in its own universe.
Also, the use of a data constructor "wrap" fools Agda into accepting j as a size eligible for justifying termination.
This is a somewhat sloppy analysis Agda does here.

Original comment by andreas....@gmail.com on 10 Feb 2015 at 8:21

• Changed title: Strong normalization almost broken in an open context

[GoogleCodeExporter]

Here is a variant that actually uses an (empty) sized type D.

open import Common.Size
open import Common.Prelude

data D (i : Size) : Set where
  wrap : (j : Size< i) → D i

module M (f : ∀ i → D i) where

  test : ∀ i → D i → ⊥
  test i (wrap j) = test j (f j)

module N (g : ∀ i → Size< i) where

  f : ∀ i → D i
  f i = wrap (g i)

  open M f

  loop : Size → ⊥
  loop i = test i (f i)

Original comment by andreas....@gmail.com on 13 Feb 2015 at 11:16

[GoogleCodeExporter]

A bit more nicely, this test is written:

open import Common.Size
open import Common.Prelude

-- Note: the assumption of pred is absurd,
-- but still should not make Agda loop.

module _ (pred : ∀ i → Size< i) where

data D (i : Size) : Set where
  wrap : (j : Size< i) → D i

loop : ∀ i → D i → ⊥
loop i (wrap j) = loop j (wrap (pred j))
-- Loops during injectivity check

d : ∀ i → D i
d i = wrap (pred i)

absurd : ⊥
absurd = loop ∞ (d ∞)

Original comment by andreas....@gmail.com on 13 Feb 2015 at 12:40

• Changed title: Strong normalization broken in an open context

[GoogleCodeExporter]

Here is a variant that uses a size in the recursive call that origins from a subtree. (Andrea's original example.)

data D (i : Size) : Set where
  c : (j : Size< i) → D j → D i

module _ (pred : ∀ i → Size< i) (d : ∀ i → D i) where

  loop : ∀ i → D i → ⊥
  loop i (c j _) = loop j (c (pred j) (d (pred j)))

Original comment by andreas....@gmail.com on 14 Feb 2015 at 9:26

[GoogleCodeExporter]

I think I want to disallow functions into Size and Size< to prevent this exploit.

Original comment by andreas....@gmail.com on 14 Feb 2015 at 9:29

[GoogleCodeExporter]

I introduce a new sort SizeUniv to single out types Size and Size< and to prevent forming function spaces between them (so no function spaces in SizeUniv).

628fdcf

As a consequence, the SIZE builtins cannot have displayable Agda types any more:

531b71d

However, currently advance on this issue is stuck on the internal (hackish)
handling of sort metas, which are represented as level metas. This is also a
problem for double-checking meta solutions with CheckInternal.

I pushed my progress so far.

Original comment by andreas....@gmail.com on 15 Feb 2015 at 8:23

• Changed state: Started
• Added labels: Priority-High

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 15 Feb 2015 at 8:34

• Now blocked on: Task: refactor metas in contextual type theory style. Proper sort metas. #1432

[GoogleCodeExporter]

Fixed by e69bc91

TODO: proper implementation of PTS rules in the presence of sort metas.

Original comment by andreas....@gmail.com on 17 Mar 2015 at 12:06

• Changed state: Fixed

[GoogleCodeExporter]

Currently, one can work around the "no-functions-into-size" check with parametrized modules.
This is still accepted:

open import Common.Size

data ⊥ : Set where

module Pred (i : Size) where
  postulate
    pred : Size< i
open Pred

data D (i : Size) : Set where
  c : Size< i → D i

iter : ∀ i → D i → ⊥
iter i (c j) = iter j (c (pred j))

loop : Size → ⊥
loop i = iter i (c (pred i))

Original comment by andreas....@gmail.com on 17 Mar 2015 at 9:58

• Changed state: Accepted

[GoogleCodeExporter]

Fixed by forbidding size postulates in parametrized modules: f2740b9

Original comment by andreas....@gmail.com on 17 Mar 2015 at 12:00

• Changed state: Fixed

[GoogleCodeExporter]

-- One can still make Agda loop by defining pred with a hole.
-- However, I think this should maybe not be forbidden, 
-- as then abbreviation of sizes in where clauses become impossible.

open import Common.Size

data ⊥ : Set where

data D (i : Size) : Set where
  c : Size< i → D i

module _ (i : Size) where
  pred : Size< i
  pred = ?

-- The injectivity test loops here.
iter : ∀ i → D i → ⊥
iter i (c j) = iter j (c (pred j))

absurd : ⊥
absurd = iter ∞ (c (pred ∞))

Original comment by andreas....@gmail.com on 17 Mar 2015 at 12:07

[GoogleCodeExporter]

As a result of fixing this we have more BUILTIN pragmas which also introduces the constants.

For me, a pragma can be disregarded by some tools or alternative versions of Agda.

I know that the situation between builtins, primitives, and internal constructs is not really clear yet.

In particular while I understand that SizeUniv should be treated a bit like Set, Size, Size<, ↑_, and ∞ all have types and could then stay postulates.

Original comment by nicolas....@gmail.com on 3 Jul 2015 at 4:26

[GoogleCodeExporter]

Indeed, they could remain postulates, if this is desirable.

Maybe there is another way to fix this issue, as the SizeUniv does not really harmonize with the universe hierarchy (at least the current implementation).

One could restrict Size< to negative positions, as in (i : <Size j) -> ...
However, this still needs <Size to live in a different universe.

Original comment by andreas....@gmail.com on 6 Jul 2015 at 6:07

[jespercockx]

We could try re-enabling SizeUniv now that the sort system actually allows it.