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

Bad typing rule? Type checking errors in NoPCM and SWHS DDs #3131

Closed
balacij opened this issue Nov 25, 2022 · 3 comments
Closed

Bad typing rule? Type checking errors in NoPCM and SWHS DDs #3131

balacij opened this issue Nov 25, 2022 · 3 comments
Assignees

Comments

@balacij
Copy link
Collaborator

balacij commented Nov 25, 2022

Related to #3093

From NoPCM (shared with SWHS):

`tauW` exposes ill-typed expressions!
  - ERROR: Associative arithmetic operation expects all operands to be of the same expected type (Real).
    Received:
    - Rational
    - Rational

From SWHS:

`tauW` exposes ill-typed expressions!
  - ERROR: Associative arithmetic operation expects all operands to be of the same expected type (Real).
    Received:
    - Rational
    - Rational

`eta` exposes ill-typed expressions!
  - ERROR: Associative arithmetic operation expects all operands to be of the same expected type (Real).
    Received:
    - Rational
    - Rational

`tauSP` exposes ill-typed expressions!
  - ERROR: Associative arithmetic operation expects all operands to be of the same expected type (Real).
    Received:
    - Rational
    - Rational

`tauLP` exposes ill-typed expressions!
  - ERROR: Associative arithmetic operation expects all operands to be of the same expected type (Real).
    Received:
    - Rational
    - Rational
@balacij
Copy link
Collaborator Author

balacij commented Nov 25, 2022

Well, it's not really a bad typing rule. Each of these are "okay" (at least w.r.t. the errors shown), except that they use addRe or mulRe, when they need to be using, the non-existent, addRat or mulRat. I think we can merge addRe and addI into just add (and then hide it behind $+ again).

@JacquesCarette
Copy link
Owner

I agree about merging addRe and addI and hiding.

The errors are real (pun intended) basically because none of those things should be Rational, that seems like a plain hack that should be fixed.

@JacquesCarette
Copy link
Owner

All of these are fixed now.

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

2 participants