Guardedness checker inconsistency with copatterns

[GoogleCodeExporter]

Bug found by Dmitriy Traytel.

{-# OPTIONS --sized-types --copatterns #-}
module False where

open import Size

record Stream (A : Set) : Set where
  coinductive
  field
    shd : A
    stl : Stream A
open Stream public

map : ∀ {A B : Set} → (A → B) → Stream A → Stream B
shd (map f a) = f (shd a)
stl (map f a) = map f (stl a)

data Mu-Stream : Size → Set where
  inn : ∀ {i} → Stream (Mu-Stream i) → Mu-Stream (↑ i)

iter : ∀ {A} → (Stream A → A) → ∀ {i} → Mu-Stream i → A
iter s (inn t) = s (map (iter s) t)

wit : Stream (Mu-Stream ∞)
shd wit = inn wit  -- SHOULD BE REJECTED
stl wit = wit

data ⊥ : Set where

false : ⊥
false = iter shd (inn wit)

It is a bug in the untyped guardedness check.

  wit : Stream (Mu-Stream ∞)
  shd wit = inn wit
  stl wit = wit

Since (shd wit) is not a recursive position for streams, the recursive call to
wit should be banned here. Only (stl wit) is a recursive position.

Original issue reported on code.google.com by andreas....@gmail.com on 19 Jun 2014 at 6:46

[GoogleCodeExporter]

If termination checking was on sizes only, wit would not go through:

{-# OPTIONS --sized-types --copatterns #-}
module _ where

open import Common.Size

record Stream (A : Set) {i : Size} : Set where
  coinductive
  field
    head : A
    tail : ∀{j : Size< i} → Stream A {j}
open Stream public

data Mu-Stream : Size → Set where
  inn : ∀ {i} → Stream (Mu-Stream i) → Mu-Stream (↑ i)

wit : ∀{i} → Stream (Mu-Stream ∞) {i}
head (wit {i}) = inn (wit {∞})
tail (wit {i}) {j} = wit {j}

Original comment by andreas....@gmail.com on 19 Jun 2014 at 6:54

[GoogleCodeExporter]

Fixed by 66dfc9e with test case 150cfbe.

Original comment by andreas....@gmail.com on 1 Jul 2014 at 2:23

• Changed state: Fixed

[GoogleCodeExporter]

Original comment by andres.s...@gmail.com on 18 Jul 2014 at 5:36

• Added labels: Milestone-2.4.0.2

[GoogleCodeExporter]

By playing around with test/fail/Issue1209.agda with Pierre Hyvernat, I found a
slight variation brings the issue back:

-- Andreas, 2014-01-07 Issue reported by Dmitriy Traytel
-- Andreas, 2015-04-15 Issue resurrected with Pierre Hyvernat

{-# OPTIONS --copatterns #-}

module _ where

open import Common.Size
open import Common.Prelude
open import Common.Product

record Stream (A : Set) : Set where
  coinductive
  field
    force : A × Stream A
open Stream

map :  ∀{A B} → (A → B) → Stream A → Stream B
force (map f s) = let  a , as = force s  in  f a , map f as

-- This type should be empty, as Stream A is isomorphic to ℕ → A.
data D : (i : Size) → Set where
  lim : ∀ i → Stream (D i) → D (↑ i)

-- Emptiness witness for D.
empty : ∀ i → D i → ⊥
empty .(↑ i) (lim i s) = empty i (proj₁ (force s))

-- BAD: But we can construct an inhabitant.
inh : Stream (D ∞)
force inh = lim ∞ inh , inh -- Should be rejected by termination checker.

absurd : ⊥
absurd = empty ∞ (lim ∞ inh)

Original comment by andreas....@gmail.com on 15 Apr 2015 at 9:28

• Changed state: Accepted
• Removed labels: Milestone-2.4.0.2

[GoogleCodeExporter]

Same problem for musical coinduction

open import Common.Coinduction renaming (∞ to Delay)
open import Common.Size
open import Common.Product

data ⊥ : Set where

record Stream (A : Set) : Set where
  inductive
  constructor delay
  field
    force : Delay (A × Stream A)
open Stream

head : ∀{A} → Stream A → A
head s = proj₁ (♭ (force s))

-- This type should be empty, as Stream A is isomorphic to ℕ → A.
data D : (i : Size) → Set where
  lim : ∀ i → Stream (D i) → D (↑ i)

-- Emptiness witness for D.
empty : ∀ i → D i → ⊥
empty .(↑ i) (lim i s) = empty i (head s)

-- BAD: But we can construct an inhabitant.
inh : Stream (D ∞)
inh = delay (♯ (lim ∞ inh , inh)) -- Should be rejected by termination checker.

absurd : ⊥
absurd = empty ∞ (lim ∞ inh)

Original comment by andreas....@gmail.com on 15 Jul 2015 at 7:59

• Added labels: Coinduction, SizedTypes

[GoogleCodeExporter]

See also https://lists.chalmers.se/pipermail/agda/2011/003339.html

-- npouillard, 2011-10-04

open import Coinduction renaming (∞ to co)
open import Size

data ⊥ : Set where

data Mu-co : Size → Set where
  inn : ∀ {i} → co (Mu-co i) → Mu-co (↑ i)

iter : ∀ {i} → Mu-co i → ⊥
iter (inn t) = iter (♭ t)

bla : Mu-co ∞
bla = inn (♯ bla)

false : ⊥
false = iter bla

Original comment by andreas....@gmail.com on 15 Jul 2015 at 8:10

[GoogleCodeExporter]

This variant is due to Nisse, I think:

{-# OPTIONS --copatterns #-}

open import Size
open import Data.Product

data ⊥ : Set where

record Delay (A : Set) : Set where
  coinductive
  constructor ♯
  field ♭   : A × (⊥ → Delay A)  -- Make it recursive to please termination checker
open Delay

data D : Size → Set where
  inn : ∀ i → Delay (D i) → D (↑ i)

iter : ∀{i} → D i → ⊥
iter (inn i t) = iter (proj₁ (♭ t))

-- Should be rejected by termination checker
bla : Delay (D ∞)
♭ bla = inn ∞ bla , λ()

false : ⊥
false = iter (proj₁ (♭ bla))

Original comment by andreas....@gmail.com on 15 Jul 2015 at 8:46

[GoogleCodeExporter]

Version with mutual definition:

{-# OPTIONS --copatterns #-}

open import Size

data ⊥ : Set where

mutual
  data D : Size → Set where
    inn : ∀ i → D' i → D (↑ i)

  record D' (i : Size) : Set where
    coinductive
    constructor ♯
    field ♭   : D i
open D'


iter : ∀{i} → D i → ⊥
iter (inn i t) = iter (♭ t)

-- Should be rejected by termination checker
bla : D' ∞
♭ bla = inn ∞ bla

false : ⊥
false = iter (♭ bla)

Original comment by andreas....@gmail.com on 15 Jul 2015 at 8:57

[GoogleCodeExporter]

The symmetric version is correctly rejected, as coinductive projections are not size-preserving. Maybe we should just make inductive constructors not guardedness-preserving.
Only that then copatterns are in general only usable with sizes.

{-# OPTIONS --copatterns #-}

open import Size

data ⊥ : Set where

mutual
  data D (i : Size) : Set where
    inn : D' i → D i

  record D' (i : Size) : Set where
    coinductive
    field ♭   : {j : Size< i} → D j
open D'

bla : ∀{i} → D' i
♭ bla = inn bla

-- Should be rejected by termination checker
iter : D ∞ → ⊥
iter (inn t) = iter (♭ t)

false : ⊥
false = iter (♭ bla)

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

[jespercockx]

I guess this deserves the false label?

[nad]

Maybe we should just make inductive constructors not guardedness-preserving.
Only that then copatterns are in general only usable with sizes.

Perhaps we could hide the old guardedness machinery under a flag:

           --guardedness                               enable constructor-based guarded corecursion (inconsistent with --sized-types)
           --guardedness-preserving-type-constructors  treat type constructors as inductive constructors when checking productivity, implies --guardedness
           --sized-types                               use sized types (default, inconsistent with --guardedness)
           --no-sized-types                            disable sized types

We should reject the combination of --guardedness and --sized-types (or the absence of --no-sized-types) when --safe is active. Perhaps other combinations should also be rejected.

[jespercockx]

I agree, the combination of --guardedness, --sized-types, and --safe should be rejected. Maybe we should also make --sized-types imply --no-guardedness by default (but still allow the user to override it with an explicit --guardedness flag).

[nad]

I think the default should be something that we believe is safe, to avoid leading people astray.

[nad]

Blocked by #3451.

[nad]

I tried to fix this by (basically) replacing guardedness with Order.Unknown in the following line when --guardedness is not active:

agda/src/full/Agda/Termination/TermCheck.hs

Line 1048 in 94b9736

return $ addGuardedness guardedness (size es) (size pats) matrix

Is this all that is needed? The test suite points to a potential problem. For instance, take Issue1375.agda. The following is the previous error message:

agda/test/Fail/Issue1375.err

Lines 1 to 14 in 94b9736

	Issue1375.agda:5,1-17,25
	Termination checking failed for the following functions:
	Type
	Problematic calls:
	Type
	(at Issue1375.agda:9,12-16)
	Term type
	(at Issue1375.agda:11,10-14)
	type
	(at Issue1375.agda:11,15-19)
	Unsolved interaction metas at the following locations:
	Issue1375.agda:16,34-38
	Issue1375.agda:16,52-56
	Issue1375.agda:17,21-25

The new error message does not include the problematic call to type. Does anyone know why?

[nad]

@andreasabel?

[nad]

The standard library mixes the two forms of corecursion. For instance, Codata.Conat provides conversions to and from Codata.Musical.Conat.Coℕ. @MatthewDaggitt and @gallais, how would you like to address this? It is possible to activate both constructor-based guarded corecursion and corecursion based on sized types in one module, but not if --safe is active.

[nad]

Note also that --sized-types and --guardedness will presumably both become infective (#2487).

[nad]

Some further questions:

• Should the musical builtins be available when --guardedness is not active?

• Should it be possible to define coinductive records that do not use sized types without turning on --guardedness? (In that case: Is there a correct way to "use sized types"?)

• Should both --sized-types and --guardedness be off by default?

  Given that we plan to fix the problems with sized types I suggest that we let sized types be on by default unless --safe is used, in which case neither option is activated. Later we can perhaps make --sized-types the default also when --safe is in use.

[gallais]

@MatthewDaggitt and @gallais, how would you like to address this?

We could move the conversion functions to the Codata.Musical.* modules. They exist
solely because the (unsafe) IO currently uses old-style coinduction and we want to be
able to write programs using the new-style one.

[nad]

I've pushed a fix now. Some notes:

• I moved the conversion functions to the Musical modules. I also changed Data.Container.ν so that it uses the sized variant of M. I pushed these changes to the experimental branch.

• I did not address the further questions above.

• I discussed the matter of missing problematic calls with @andreasabel, and I got the impression that he did not think that this is a sign of a (new) hole in the termination checker.

[nad]

Blocked by #3451.

Instead of waiting for a fix I pushed a test case to test/Succeed instead of test/Fail.

[nad]

@andreasabel, consider the following code:

Type : Set

postulate
  type : Type
  Term : Type → Set

Type = Term type

When I run Agda with -vterm.found.call:20 I get the following output:

found call from Type to type
found call from Type to Term
found call from type to type
found call from type to Term
found call from Term to Type

This looks strange to me. Why are there calls from type to type/Term, but no call from type to Type?

[nad]

I'm moving the discussion of the potential problem discussed in the previous comment to #1556.

[andreasabel]

Your fix as described in #1209 (comment) LGTM, @nad.