search

jaccokrijnen / plutus-cert

0 stars 2 forks source link

Why does binds_Gamma not add the real constructor types? #55

Closed jaccokrijnen closed 3 months ago

jaccokrijnen commented 3 months ago

image

Constructors' types are not directly their annotation, but have their result type replaced by the "expected" type (i.e. datatype name applied to all its parameters). Whether all constructors have this expected type is checked separately in constructor_well_formed.

Why not directly use the annotated type of the constructor? If it doesn't have the expected result type, the typing derivation will go wrong when checking that.

jaccokrijnen commented 3 months ago

The PIR typechecker compiles the datatype, and then only uses the generated types.

https://github.com/IntersectMBO/plutus/blob/16be7da33eacb1991ae0164b9fd65e12c7e4771e/plutus-core/plutus-ir/src/PlutusIR/TypeCheck/Internal.hs#L470

jaccokrijnen commented 3 months ago

I've changed it so that it just uses the annotation (with added type abstractions for the ADT's type parameter). This is consistent with the compiler implementation