Type Check fail

[LKlinke]

from probably.pgcl.compiler import compile_pgcl

compile_pgcl("""
nat s;
nat c;
nat tmp;
tmp :=((1-(1-(c*c))^(1/2))/c)
""")

Results in

CheckFail(location=BinopExpr(operator=Binop.POWER,
lhs=BinopExpr(operator=Binop.MINUS,
        lhs=NatLitExpr(1),
        rhs=BinopExpr(operator=Binop.TIMES, lhs=VarExpr('c'), rhs=VarExpr('c'))
    ),
rhs=RealLitExpr("1/2")),
message='Expected value of type NatType(bounds=None), got RealType().')

[Philipp15b]

What's the minimal program/expression that triggers this?

[Legotier]

This is triggered by the expression ((1-(1-(c*c))^(1/2))/c). It happens because the function is_compatible() in check.py doesn't behave as documented; NatTypes are not compatible with RealTypes, i.e., n^(1/2) is wrongly typed if n is a natural number.

A simple fix would be to change line 309 in check.py from if isinstance(lhs, NatType) and isinstance(rhs, NatType): to if isinstance(lhs, NatType) and isinstance(rhs, (NatType, RealType)):, though this seems to break one of the testcases.

(it might be possible that I'm misunderstanding the concept of compatibility here)