Type checker failing too early on complex remote calls #358

New Issue

2021-11-25T16:59:47+09:00

zxq9 commented

2021-11-25 16:59:47 +09:00

(Migrated from gitlab.com)

Created by: hanssv

Example:

contract interface Coin =
  entrypoint mint : () => int

contract interface OtherCoin =
  entrypoint mint : () => int

main contract Main =
  function mkCoin() : Coin = ct_11111111111111111111111111111115rHyByZ
  entrypoint foo() : int =
    let r = mkCoin()
    r.mint()

// Cannot unify if(protected, option(int), int)
//          and int
// when checking the record projection at line 13, column 6
//   r.mint :
//     (gas : int, value : int, protected : bool) =>
//       if(protected, option(int), int)
// against the expected type
//   (gas : int, value : int, protected : bool) => int

*Created by: hanssv* Example: ``` contract interface Coin = entrypoint mint : () => int contract interface OtherCoin = entrypoint mint : () => int main contract Main = function mkCoin() : Coin = ct_11111111111111111111111111111115rHyByZ entrypoint foo() : int = let r = mkCoin() r.mint() // Cannot unify if(protected, option(int), int) // and int // when checking the record projection at line 13, column 6 // r.mint : // (gas : int, value : int, protected : bool) => // if(protected, option(int), int) // against the expected type // (gas : int, value : int, protected : bool) => int ```

ghallak commented

2021-12-04 01:34:02 +09:00

(Migrated from gitlab.com)

I have looked into this and the reason for why this bug is happening seems to be that the constraints are being solved out of order.

In the above code, there are 2 dependent type constraints (one for mkCoin() and the other for mint()), and 1 field constraint (for r.mint()).

To be able to solve the field constraint for r.mint(), the dependent type constraint for mkCoin() has to be solved first or otherwise the type of the record r will be unknown.

Currently, the code tries to solve all field constraints before moving to solve the dependent type constraints here.

What I think would fix this bug is trying to solve the constraints in the order in which they are added (1. dependent type constraint for mkCoin(), 2. field constraint for r.mint(), 3. dependent type constraint for r.mint()).

Do you know of the reason why constraints are being solved separately? and do you think that the above solution might fail for some reason?

I have looked into this and the reason for why this bug is happening seems to be that the constraints are being solved out of order. In the above code, there are 2 dependent type constraints (one for `mkCoin()` and the other for `mint()`), and 1 field constraint (for `r.mint()`). To be able to solve the field constraint for `r.mint()`, the dependent type constraint for `mkCoin()` has to be solved first or otherwise the type of the record `r` will be unknown. Currently, the code tries to solve all field constraints before moving to solve the dependent type constraints [here](https://github.com/aeternity/aesophia/blob/fe5f5545d35f5d92576b161c22ac750a02462c15/src/aeso_ast_infer_types.erl#L2081-L2082). What I think would fix this bug is trying to solve the constraints in the order in which they are added (1. dependent type constraint for `mkCoin()`, 2. field constraint for `r.mint()`, 3. dependent type constraint for `r.mint()`). Do you know of the reason why constraints are being solved separately? and do you think that the above solution might fail for some reason?

zxq9 commented

2021-12-06 17:34:53 +09:00

(Migrated from gitlab.com)

Created by: UlfNorell

The proper solution would be to solve all constraints together and be more careful about only failing hard if we know a constraint is unsolvable, and save it for later if more information might allow us to solve it. I don't think there are any reasons why the constraints need to be solved separately.

*Created by: UlfNorell* The proper solution would be to solve all constraints together and be more careful about only failing hard if we know a constraint is unsolvable, and save it for later if more information might allow us to solve it. I don't think there are any reasons why the constraints need to be solved separately.

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: QPQ-AG/sophia#358