Copatterns: values that do not produce anything coinductive should not have to be guarded

[UlfNorell]

From guillaum...@gmail.com on September 18, 2013 16:48:41

{-# OPTIONS --copatterns #-}

module Test where

{- Globular types as a coinductive record -} record Glob : Set1 where coinductive field Ob : Set Hom : (a b : Ob) → Glob open Glob public

record Unit : Set where

data == {A : Set} (a : A) : A → Set where refl : a == a

{- The terminal globular type -} Unit-glob : Glob Ob Unit-glob = Unit Hom Unit-glob = Unit-glob

{- The tower of identity types -} Id-glob : (A : Set) → Glob Ob (Id-glob A) = A Hom (Id-glob A) a b = Id-glob (a == b)

---

(now I’m using the new copatterns implementation) The definition of Unit-glob is accepted but the definition of Id-glob is rejected (it should be accepted as well).

Original issue: http://code.google.com/p/agda/issues/detail?id=906

[UlfNorell]

From nils.anders.danielsson on September 19, 2013 06:36:22

Owner: andreas....@gmail.com
Labels: Milestone-2.3.4

[UlfNorell]

From nils.anders.danielsson on September 19, 2013 06:36:38

Labels: Copatterns

[UlfNorell]

From andreas....@gmail.com on September 20, 2013 10:15:06

If you make the hidden argument of the identity type visible

Id-glob : (A : Set) → Glob Ob (Id-glob A) = A Hom (Id-glob A) a b = Id-glob (== {A = Ob (Id-glob A)} a b)

then you see the problem. Agda does not like the call

Hom (Id-glob A) --> Ob (Id-glob A)

thinking this is unguarded.

No sure what to do about it.

• Ignore parameters in the termination checker? (Losing SN possibly)
• Infer an order on the projections?

Status: InfoNeeded

[UlfNorell]

From andreas....@gmail.com on October 27, 2013 07:01:16

Mmh, maybe we could consider projections defined earlier in the record type as being smaller. This would reflect the dependency order.

Labels: Termination Type-Enhancement

[UlfNorell]

From andreas....@gmail.com on November 07, 2013 08:47:33

Issue 942 has been merged into this issue.

[UlfNorell]

From andreas....@gmail.com on November 07, 2013 12:24:40

Earlier projections (like Ob) are now considered smaller than later ones (like Hom) when comparing copattern spines, so this termination checks now.

Status: Fixed

[UlfNorell]

From guillaum...@gmail.com on November 14, 2013 08:56:47

Doesn’t seem to be completely fixed, see http://code.google.com/p/agda/issues/detail?id=907#c5 for a term which is wrongly reported as non-terminating when there are still unsolved goals.

[UlfNorell]

From ulf.nor...@gmail.com on November 14, 2013 08:59:55

Status: Accepted

[UlfNorell]

From andreas....@gmail.com on November 21, 2013 14:39:02

data == {A : Set} (a : A) : A → Set where idp : a == a

-- Coinductive equivalences record CoEq (A B : Set) : Set where coinductive constructor coEq field to : A → B from : B → A eq : (a : A) (b : B) → CoEq (a == from b) (to a == b) open CoEq public

module Works where id-CoEq : (A : Set) → CoEq A A to (id-CoEq A) a = a from (id-CoEq A) b = b eq (id-CoEq A) a b = id-CoEq (a == b)

module Issue where id-CoEq : (A : Set) → CoEq A A to (id-CoEq A) a = a from (id-CoEq A) b = b eq (id-CoEq A) a b = id-CoEq {!(a == b)!}

Interesting. In module Works everything is fine, but in module Issue, the metavariable is solved as

?0 := (a == from (id-CoEq A) b)

This can be given via C-c C-s. However, termination checking fails since the call to

id-CoEq A .from b

is not guarded. This is an imprecision of the termination checker. Since it does not produce anything in a coinductive type, it does not have to be guarded.

It seems pointless to patch up the termination checker further. Why don't you try to use sized types? Works like a charm for this example: {-# OPTIONS --copatterns --sized-types --show-implicit #-}

open import Size

data == {A : Set} (a : A) : A → Set where idp : a == a

-- Coinductive equivalences record CoEq {i : Size} (A B : Set) : Set where coinductive constructor coEq field to : A → B from : B → A eq : {j : Size< i}(a : A) (b : B) → CoEq {i = j} (a == from b) (to a == b) open CoEq public

module Works where id-CoEq : {i : Size}(A : Set) → CoEq {i = i} A A to (id-CoEq A) a = a from (id-CoEq A) b = b eq (id-CoEq A) a b = id-CoEq (a == b)

module Issue where id-CoEq : {i : Size}(A : Set) → CoEq {i = i} A A to (id-CoEq A) a = a from (id-CoEq A) b = b eq (id-CoEq {i = i} A) a b = id-CoEq {! (a == b) !}

[UlfNorell]

From andreas....@gmail.com on December 04, 2013 13:12:02

Does your stuff work with sized types?

I am taking away the milestone tag here, unless you protest....

Summary: Copatterns: values that do not produce anything coinductive should not have to be guarded (was: Productivity/termination checker complains where it shouldn't)
Labels: -Milestone-2.3.4 Priority-High