[Agda] Bug in record definition

[Nicolas Pouillard]

On Sun, 27 Mar 2011 22:10:47 +0200, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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.

I would be in favor of this change to. At least by a flag to begin with.
Does anybody want to keep this feature and why?

Cheers,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr