[Agda] Using coinductive record constructor fails termination checking (2.5.1.1)

[Andreas Abel]

Dear Sebastian,

this is to be expected.  Agda uses a unrestricted rewriting semantics, 
so if you write

   bar = 0 > bar

there is an infinite reduction sequence

   bar = 0 > bar = 0 > 0 > bar = 0 > 0 > 0 > bar ...

Thus, the termination checker complains.

Cheers,
Andreas

P.S.: The old ("musical") coinduction of Agda had a special magic for 
the sole coinductive constructor #, thus,

   bar = 0 > (# bar)

would be accepted there.

On 30.08.2016 15:09, Sebastian Seufert wrote:
> Dear all,
>
> I have a record declared that is parametrized with Stream Set:
>
> record ⟦_⟧ (R : Stream Set)  {i : Size} : Set where
>   coinductive
>   constructor _►_
>   field
>     now   : hd R
>     later :  ∀ {j : Size< i} → ⟦ tl R ⟧ {j}
> open ⟦_⟧ public
>
> Using the record with copatterns is fine by the termination checker :
>
> foo : ⟦ repeat ℕ  ⟧
> now foo = 0
> later foo = foo
>
> whereas using the constructor awakens the termination-check-dogs:
>
> bar : ⟦ repeat ℕ ⟧
> bar = 0 ► bar
>
> --
>
> Stream is defined using sized types
>
> record Stream {i : Size} {a} (A : Set a) : Set a where
>   coinductive
>   constructor _∷_
>   field
>     hd : A
>     tl : ∀ {j : Size< i} → Stream {j} A
> open Stream public
>
> and repeat like this
>
> repeat : ∀ {a} {A : Set a} → A → Stream A
> hd (repeat x) = x
> tl (repeat x) = repeat x
>
> I expected the behaviour of foo to be the same as bar, wondering if there's something I am missing.
>
> Regards,
> -Sebastian
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/