Fully abstract records

[ohad]

Add support for implicit and auto implicit parameters to records, with rig annotations.

This allows us to declare records such as:

data NotZero : Nat -> Type where
  Is : {n : Nat} -> NotZero (S n)

record Positive (n : Nat) {auto 0 pos : NotZero n} where
  constructor Check

a : Positive 1
a = Check

b : Positive 2
b = Check

(taken from the added test/idris2/record003)

I'm not sure anyone would want the irrelevance annotation in the type, but we might as well allow it.

This is my first independent tweak to (small parts of) the elaborator, so I'd be grateful for a thorough review.

The refactoring of the parser's pibindList through pibindListName might slow it down a little bit. I haven't profiled to see if it's substantial. If it is, we can inline pibindListName and add a Just.

[ohad]

Ah, since @edwinb says we will support defaults, I'll add support for them too (should amount to just parsing + testing, but who knows up front)

[ohad]

OK, I've added default arguments to record types, so this is ready to be merged.

(There's still a missing feature in allowing fields to be auto / default implicits, but I'll leave that to the future.)

[ziman]

I'm wondering about the auto implicit parameters (not fields).

Just to illustrate what I mean: in the case of Positive, I think I'd go for the following instead:

record Positive (n : Nat) where
  constructor Check
  {auto 0 isPositive : NotZero n}

Otherwise you wouldn't be able to even talk about the positivity of numbers that have not already been proven to be positive.

I understand that Positive might be just a contrived minimal example to avoid a lot of explanation. Besides, even my suggestion does not parse currently, so it's certainly good to add that.

But I still wonder if it's ever useful to have an auto implicit as a parameter of a type constructor.

[ohad]

I understand that Positive might be just a contrived minimal example to avoid a lot of explanation.

Yes, it's a contrived example :).

I'm wondering about the auto implicit parameters (not fields).

Just to illustrate what I mean: in the case of Positive, I think I'd go for the following instead:

record Positive (n : Nat) where
  constructor Check
  {auto 0 isPositive : NotZero n}

Yes, that's a much better way to do it. As I said above, we should add auto to fields at some point, though it's a bit less pressing to me than adding implicit arguments to the record type parameters.

This is because, the auto implicit behaviour only affects the generated constructor, and so it is not a lot of hassle to add a 'smart constructor' instead.

[ohad]

PS: thanks for taking a close look at this. I'm still a newb in this area, and the more eyeballs covering my patches, the better.

[edwinb]

Thanks for the update and the useful discussion and reviewing! There may be more to tinker with, but this is a useful addition as it is now, I think.