Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Record field ordering issue in shared term type checking #102

Closed
atomb opened this issue Feb 16, 2016 · 0 comments
Closed

Record field ordering issue in shared term type checking #102

atomb opened this issue Feb 16, 2016 · 0 comments

Comments

@atomb
Copy link
Contributor

atomb commented Feb 16, 2016

When running the ECDSA proof with extra type checking enabled (the -t flag), I'm noticing some failures due to differences in field ordering in records. For example, the following is one of the messages (edited slightly for readability):

Function argument type
  let { x0 = #{};
      x1 = Prelude.Vec 384 Prelude.Bool;
      x2 = #(x1,x1);
      x3 = (x :: x1) -> x1;
    }
 in #(#{"add" = (__p1 :: x2) -> x1 |
      #{"div" = (__p21 :: x2) -> x1 |
      #{"field_unit" = x1 |
      #{"field_zero" = x1 |
      #{"half" = x3 |
      #{"is_equal" = (__p22 :: x2) -> Prelude.Bool |
      #{"is_val" = (x :: x1) -> Prelude.Bool |
      #{"mul" = (__p3 :: x2) -> x1 |
      #{"neg" = x3 |
      #{"norm" = x3 |
      #{"sq" = x3 |
      #{"sub" = (__p2 :: x2) -> x1 |
      x0}}}}}}}}}}}}
     ,#{"x" = x1 |
      #{"y" = x1 |
      #{"z" = x1 |
      x0}}})
doesn't match expected type
  let { x0 = #{};
      x1 = Prelude.Vec 384 Prelude.Bool;
      x2 = #(x1,x1);
      x3 = x1 -> x1;
      x4 = x2 -> x1;
    }
 in #(#{"is_val" = x1 -> Prelude.Bool |
      #{"norm" = x3 |
      #{"add" = x4 |
      #{"sub" = x4 |
      #{"neg" = x3 |
      #{"mul" = x4 |
      #{"sq" = x3 |
      #{"half" = x3 |
      #{"div" = x4 |
      #{"field_zero" = x1 |
      #{"field_unit" = x1 |
      #{"is_equal" = x2 -> Prelude.Bool |
      x0}}}}}}}}}}}}
     ,#{"x" = x1 |
      #{"y" = x1 |
      #{"z" = x1 |
      x0}}})

Modulo naming of type parameters and reordering of fields, these seem the same to me.

brianhuffman pushed a commit that referenced this issue Apr 26, 2021
Add name to error message about uninterpreted higher-order functions.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant