[Agda] Bug in record definition

[Andreas Abel]

Yes, it seems that this is a bug.

However, I would like to add that you are using speculative features of 
Agda which I personally would like to disappear.

If you just feed Agda the record definition,

On 27.03.11 8:26 PM, Sivaram Gowkanapalli wrote:
> module bug-in-record where
>
> open import Data.Maybe using (Maybe; just; nothing)
> open import Data.List using (List; []; [_]; _++_)
> open import Data.Nat using (ℕ)
>
> record MyMonadPlus m : Set₁ where
>   field mzero : {a : Set} → m a → List a
>         mplus : {a : Set} → m a → m a → List a

then you will will notice that m is colored yellow, so the type of m 
could not be determined; unsolved metavariables remain.

The feature which I think should be removed is that Agda allows the 
subsequent code to solve these metavariables.  Which means that the 
*definition* of a thing is influenced behind the curtain by its *use*. 
Conceptually very questionable.

In your case that leads to an error.

But you should have gone back earlier and have removed the yellow stuff 
right away, by telling Agda what you mean.

> record MyMonadPlus (m : Set → Set) : Set₁ where
>  field mzero : {a : Set} → m a → List a
>        mplus : {a : Set} → m a → m a → List a

Then, as you say, everything works.

Cheers,
Andreas

P.S.: I file a bug in the tracker.

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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