Reduce with already type-checked clauses for type-checking remaining clauses (useful for copatterns)

[UlfNorell]

From guillaum...@gmail.com on September 18, 2013 16:53:39

{-# 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

Glob-corec : {A : Set1} (Ob* : A → Set) (Hom* : (x : A) (a b : Ob* x) → A) → (A → Glob) Ob (Glob-corec Ob* Hom* x) = Ob* x Hom (Glob-corec Ob* Hom* x) a b = Glob-corec Ob* Hom* (Hom* x ? ?)

---

The two question marks should be filled by [a] and [b]. C-c C-SPC accept them but not C-c C-l. The error is:

(Ob (Glob-corec Ob* Hom* x)) !=< (Ob* x) of type Set when checking that the expression a has type Ob* x

(note that [Ob (Glob-corec Ob* Hom* x)] should be equal to [Ob* x] because of the first clause)

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

[UlfNorell]

From nils.anders.danielsson on September 19, 2013 06:39:18

Summary: Some term is accepted by C-c C-SPC but not by C-c C-l (involving reduction of a previous copattern) (was: [copatterns] Some term is accepted by C-c C-SPC but not by C-c C-l (involving reduction of a previous copattern))
Owner: andreas....@gmail.com
Labels: Copatterns

[UlfNorell]

From andreas....@gmail.com on September 20, 2013 10:21:37

The problem here is that the first equation is only unfolded after the whole definition has been type-checked. This spoils the fun for dependent record types and copatterns.

To make this work we need to change Agda to add the clauses one after another. However, termination checking currently needs all the clauses (not so the Abel-Pientka-ICFP'13 approach, though).

That bug is probably not fixed soon...

Status: Accepted
Labels: Priority-Medium

[UlfNorell]

From andreas....@gmail.com on October 14, 2013 07:55:47

Summary: Reduce with already type-checked clauses for type-checking remaining clauses (useful for copatterns) (was: Some term is accepted by C-c C-SPC but not by C-c C-l (involving reduction of a previous copattern))
Labels: Type-Enhancement

[UlfNorell]

From andreas....@gmail.com on October 27, 2013 06:55:10

Fixed. We now add function clauses to the reduction machinery as soon as they are type-checked.

Guillaume, if this was a show-stopper, you can try to move on now.

Status: Fixed
Labels: Conversion

[UlfNorell]

From guillaum...@gmail.com on November 14, 2013 08:51:21

Thanks, the original example works now, but here is another example where it's not working. In this case it’s the opposite, C-c C-l works but C-c C-Space doesn’t. Also, id-CoEq is wrongly reported as non-terminating, but only when there is a goal left.

{-# OPTIONS --copatterns #-}

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

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)!}

[UlfNorell]

From guillaum...@gmail.com on November 14, 2013 08:53:04

The error message (when doing C-c C-Space in the goal at the last line) is

b != (from (id-CoEq A) b) of type A when checking that the expression ? has type Set