Unexpected type inference behaviour with record creation syntax

[lukaszcz]

Typechecking

module inferCreate;

type Tree A :=
  | empty
  | node@{
      element : A;
      left : Tree A;
      right : Tree A
    };

map {A B} (f : A -> B) (tree : Tree A) : Tree B :=
  let
    go : Tree A -> Tree B
      | empty := empty
      | node@{element; left; right} := node@{
        element := f element;
        left := go left;
        right := go right
      };
  in go tree;

gives

/Users/heliax/Documents/progs/juvix/inferCreate.juvix:16:9-21: error:
The expression f element has type:
  B
but is expected to have type:
  A

One would expect the type of the node being created to be correctly inferred as Tree B. It seems that type inference for some reason decides it should be Tree A.

Note that the following type-checks:

map {A B} (f : A -> B) (tree : Tree A) : Tree B :=
  let
    go : Tree A -> Tree B
      | empty := empty
      | node@{element; left; right} := node (f element) (go left) (go right);
  in go tree;

So the problem is with type inference for the record creation syntax.

[janmasrovira]

I think the problem is that in the assignment element := f element, the element on the rhs refers to the element on the lhs and not to the element bound in the node@{element; left; right} pattern. I remember we agreed to only bind the name of the field as a recursive function if it had at least one argument. But now I can't find the issue for that

[lukaszcz]

Yes, right, I didn't think of that. The issue is here: https://github.com/anoma/juvix/issues/2968. I think we should prioritize it, because it is really confusing. Even though I "know" that this is recursive, I didn't notice and the error message was not very helpful.