Should we also allow arbitrary dependency order in structs and datas?

[re-xyr]

trafficstars

This means allowing fields/ctors defined later refer to those defined earlier in their types, as what we did to Stmts, as long as the dependency graph forms a DAG.

For structs,

struct A : \Type
  | v : T
  | T : \Type

For datas,

data B (n : N) : \Type \with
  | zero => { | conA (P conC) | conB }
  | suc m => { | conC | conD (P conA) }

The case for datas looks more complicated because constructors are intertwined with match clauses.

[re-xyr]

I prefer having this functionality but the case of datas looks really very tricky to implement

[ice1000]

:worried: In case of data we would also need induction-recursion..

[ice1000]

@ice1000 Test by @ice1000

[ice1000]

Oh geez

[re-xyr]

@ice1000 Test by @ice1000

What is this?

[ice1000]

@ice1000 Test by @ice1000

What is this?

Checkout the telegram group.

[ice1000]

open data Z : Set
 | zeroZ
 | succZ Z { | predZ n => n }
 | predZ Z { | succZ n => n }

[ice1000]

The plan is:

• For data ctors, the order is random, but has to be linearizable.
• For class fields, the order is as written.
• Records are going to be deleted after classes are implemented