Improve inference of polymorphic types #392

New Issue

2022-06-17T20:52:26+09:00

ghallak commented

2022-06-17 20:52:26 +09:00

(Migrated from gitlab.com)

In the below example the assignment of x is failing even though the user would expect this to pass, regardless of the type of DT_CO_TWICE(f_c_to_u_to_a) (it should pass whether the type is dt_co_twice(Animal) or dt_co_twice(Cat) because dt_co_twice in covariant in 'a).

The error originates from the rvalue in the assignment of x. When matching between (Cat => unit) => Animal) (the type of f_c_to_u_to_a) and ('a => unit) => 'a (the type in the type constructor DT_CO_TWICE), the type variable 'a is first bound to Cat, and when it tries to bind to Animal it fails.

contract interface Animal =
    entrypoint f : () => unit

contract Cat : Animal =
    entrypoint f() = ()

main contract C =
    datatype dt_co_twice('a) = DT_CO_TWICE(('a => unit) => 'a)

    stateful function f_c_to_u_to_a(_ : (Cat => unit)) : Animal = Chain.create() : Cat

    stateful entrypoint init() =
        let x : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_a)  // this is failing

        ()

In the below example the assignment of `x` is failing even though the user would expect this to pass, regardless of the type of `DT_CO_TWICE(f_c_to_u_to_a)` (it should pass whether the type is `dt_co_twice(Animal)` or `dt_co_twice(Cat)` because `dt_co_twice` in covariant in `'a`). The error originates from the rvalue in the assignment of `x`. When matching between `(Cat => unit) => Animal)` (the type of `f_c_to_u_to_a`) and `('a => unit) => 'a` (the type in the type constructor `DT_CO_TWICE`), the type variable `'a` is first bound to `Cat`, and when it tries to bind to `Animal` it fails. ``` contract interface Animal = entrypoint f : () => unit contract Cat : Animal = entrypoint f() = () main contract C = datatype dt_co_twice('a) = DT_CO_TWICE(('a => unit) => 'a) stateful function f_c_to_u_to_a(_ : (Cat => unit)) : Animal = Chain.create() : Cat stateful entrypoint init() = let x : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_a) // this is failing () ```

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: QPQ-AG/sophia#392