[Agda] a bug in the type checker?

[Ulf Norell]

On Tue, Sep 21, 2010 at 2:15 PM, David Leduc <david.leduc6 at googlemail.com>wrote:

> Hi,
>
> In the definition of  t  below, the type checker does not see that
> [ t ]  is equal to  unit  and thus raise an error.
> I believe it is a bug, isnt it?
>
> module test where
>
> open import Coinduction
>
> data unit : Set where
>  tt : unit
>
> mutual
>  data T : Set1 where
>    makeT : (A : Set) -> (t : ∞ T) -> [ ♭ t ] -> T
>
>  [_] : (t : T) -> Set
>  [ makeT A _ _ ] = A
>
> t : T
> t = makeT unit (♯ t) tt
>

It's not a bug. In order to see that [ t ] is unit you need to know the
definition of t
and you can't look at the definition until you've type checked it. To make
it work
you can do the following:

mutual
  t : T
  t = makeT unit (♯ t) tt′

  tt′ : [ t ]
  tt′ = tt

In this case the definition of t can be type checked (just knowing the type,
but not
the definition of tt'). When checking the definition of tt', t has been
checked already,
so you're allowed to look at its definition.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100921/75e765c4/attachment.html