[ new ] Allow forward declarations of records

[dunhamsteve]

This change allows users to forward declare record, like they can for data, by omitting the where clause. The implementation follows the pattern of same functionality for data. After the change you can do:

record B
record A where
  b : B
record B where
  a : A

instead of

mutual
  record A where
    b : B
  record B where
    a : A

[buzden]

Mutual records also have projections cross-available, when your approach, as far as I understand, forward-declares only data. Is it possible to forward-declare projections too?

[dunhamsteve]

Do you have an example of the behavior you want? I believe happens with this patch should be exactly the same behavior as mutual blocks. (The code for desugaring the forward declaration was lifted from Mutual.idr.) My initial goal here was to enable not needing mutual (mentioned in the Yaffle docs), but perhaps there is room for improvement in both cases.

[buzden]

Do you have an example of the behavior you want? I believe happens with this patch should be exactly the same behavior as mutual blocks. (The code for desugaring the forward declaration was lifted from Mutual.idr.) My initial goal here was to enable not needing mutual (mentioned in the Yaffle docs), but perhaps there is room for improvement in both cases.

OMG, sorry, I had example like this

mutual                                                     
            
  record X where      
    n : Nat                                                                                                                                  
    y : Maybe (x : X ** Y x)                                                             
                                                                                                      
  record Y (x : X) where                                                                                                          
    m : Vect x.n Nat

but I didn't realise that I can't swap definitions inside this mutual block. So, indeed, your correction works exactly as a mutual block, but mutual blocks operates strangely when records are inside. So, this is not a problem of your code, this is a problem of records desugaring themselves.