rodrigogribeiro / solcore

1 stars 2 forks source link

Problem typechecking instances #15

Open mbenke opened 1 month ago

mbenke commented 1 month ago

Consider the following simple class/instance:

class a: Enum {
  function fromEnum(a) -> Word;
}

data Food = Curry | Beans | Other

instance Food : Enum {
  function fromEnum(x : Food) {
     match x {
       | Curry => return 1;
       | Beans => return 2;
       | Other => return 3;
     };
  }
}

contract Food {
  function main() {
    return fromEnum(Beans);
  }
}

This fails to typecheck with:

Types do not match: Food and b
 - in:Food : Enum

OTOH typechecks fine if fromEnum is ordinary function rather than a class method.

mbenke commented 1 month ago

Another, possibly related problem with instances: in the contract test/examples/NegPair.solc the typechecker outputs

instance (a : Neg, b : Neg =>) Pair[a, b] : Neg {
   function neg (p : Pair[a19, a20]) {
      return Pair[neg(fst(p)), neg(snd(p))]
   }
}

where I think should be function neg (p : Pair[a, b])

IOW it seems neg gets too general (and incorrect) type - forall a19 a20. Pair[a19, a20] -> Pair[a19, a20] rather than forall a: Neg, b: Neg. Pair[a,b] -> Pair[a,b].