Juvix Tree `not unifiable` crash

[janmasrovira]

Run:

juvix compile native error-cannot-unify.juvix

Gives:

/<tree>:1:1: error:
not unifiable: * → * → *, (Nat, Nat) → Nat

Example juvix file:

module error-cannot-unify;

type Foldable (container elem : Type) :=
  mkFoldable {
    syntax iterator for {init := 1; range := 1};
    for : (elem -> elem -> elem) -> elem -> container -> elem

  };

open Foldable public;

builtin bool
type Bool :=
  | true
  | false;

builtin bool-if
ite : {A : Type} → Bool → A → A → A
  | true a _ := a
  | false _ b := b;

< : Nat -> Nat -> Bool
  | _ _ := true;

+ : Nat -> Nat -> Nat
  | _ _ := zero;

type Nat :=
  | zero
  | suc Nat;

type Box N := mkBox {unbox : N};

ten : Nat := zero;

one : Nat := zero;

foldableBoxNatI : Foldable (Box Nat) Nat :=
  mkFoldable@{
    for (f : Nat -> Nat -> Nat) (ini : Nat) : Box Nat -> Nat
      | (mkBox x) :=
        let
          terminating
          go (x : Nat) : Nat := go (+ x one);
        in go x
  };

main : Nat := for foldableBoxNatI λ {_ y := y} one (mkBox zero);