aeternity / aesophia

Stand alone compiler for the Sophia smart contract language
https://docs.aeternity.com/aesophia
ISC License
52 stars 19 forks source link

Type checker failing too early on complex remote calls #358

Closed hanssv closed 2 years ago

hanssv commented 2 years ago

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 2 years ago

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?

UlfNorell commented 2 years ago

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.