[Agda] Record types are not allowed in mutual blocks

[Andreas Abel]

On 24.03.11 11:23 PM, Nils Anders Danielsson wrote:
> On 2011-03-18 18:15, Thorsten Altenkirch wrote:
>> Is there any way to switch off this check which stops me from doing
>> this?
>
> I'm sure there is, but we want to avoid infinite η-expansion. Perhaps we
> can avoid this by requiring that any cycle from a record type to itself
> is "guarded" by a data type (or ∞).

Sounds reasonable.  In MiniAgda, eta-expansion for recursive records is 
lazy, because of the infinite eta-expansion problem.  In Agda with 
\infty, recursive records need to be explicitely guarded, otherwise they 
would not make sense.

@Thorsten:  Here is how to remove that check: Go to

   src/full/Agda/Syntax/Concrete/Definitions.hs

and then put the -- at exactly this spot:  (for me, it is line 393)

             checkMutual nd@(NiceDef _ _ _ ds)
--              | any isRecord ds = throwError $ NotAllowedInMutual nd
               | otherwise       = return ()
             checkMutual d = throwError $ NotAllowedInMutual d

Now Agda does not complain any more.

But do not complain to me if your Agda loops now...

Cheers,
Andreas

-- 
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/
-------------- next part --------------
module MutualRecords where

mutual

  data List (A : Set) : Set where
    nil  : List A
    cons : Cons A -> List A

  record Cons (A : Set) : Set where
    constructor _,_
    field
      head : A
      tail : List A