Dependent Records

[SkySkimmer]

What exactly should happen when evaluating

{ x := e, eq : x == e := refl x}

?
If we do it wrong, we can get something like

{ x : T := e, eq : e == e := refl e } : {x:T, eq : e==e}

which doesn't have the expected type.
Essentially x isn't bound the same way in the type

x==e

and in the value

refl x

This double binding gets very annoying, see for instance the fold at line 270 of eval.ml where we carry around 2 environments and it's not clear if we should have 2 contexts as well or something.

We also unfold eagerly in values, so for instance

{ x := big, y := f x x, z := g y y }

will produce

{ x := big, y := f big big, z := g (f big big) (f big big) }

which is kind of horrible.

[andrejbauer]

We allow fields to refer to other fields and there is no need to unfold eagerly. In

{ foo := e1 ; bar := e2 ; baz := e3 }

in e3 the field foo has de Bruijn index 1 and the field bar has de Bruijn index 0. In particular this means that we do not substitute eagerly.

Next,

 { x := e, eq : x == e := refl x}

should not be valid syntax. Instead it should be

{ x := e, eq := (refl x ::  x == e)}

which evaluates to

{ x := e, eq := refl x }   ::    { x : T ; eq := (x == e) }

or with explicit de Bruijn indices:

{ x := e, eq := refl 0 }    :: { x : T ; eq := (0 == e) }

[andrejbauer]

I think it's better to create a separate branch for this than to fold it into the contexts branch. In any case, we shuld move over to master as soon as possible.

[andrejbauer]

Closing because I merged it into the records branch.

[andrejbauer]

I see now what you're talking about. I think we need to use beta hints to get around the problem.