contract interface Animal =
    entrypoint sound : () => string

contract Cat : Animal =
    entrypoint sound() = "meow"

main contract Main =
    datatype dt_contra('a) = DT_CONTRA('a => unit)
    datatype dt_co('a) = DT_CO(unit => 'a)
    datatype dt_inv('a) = DT_INV('a => 'a)
    datatype dt_biv('a) = DT_BIV(unit => unit)
    datatype dt_inv_sep('a) = DT_INV_SEP_A('a => unit) | DT_INV_SEP_B(unit => 'a)
    datatype dt_co_nest_a('a) = DT_CO_NEST_A(dt_contra('a) => unit)
    datatype dt_contra_nest_a('a) = DT_CONTRA_NEST_A(dt_co('a) => unit)
    datatype dt_contra_nest_b('a) = DT_CONTRA_NEST_B(unit => dt_contra('a))
    datatype dt_co_nest_b('a) = DT_CO_NEST_B(unit => dt_co('a))
    datatype dt_co_twice('a) = DT_CO_TWICE(('a => unit) => 'a)
    datatype dt_contra_twice('a) = DT_CONTRA_TWICE('a => 'a => unit)
    datatype dt_a_contra_b_contra('a, 'b) = DT_A_CONTRA_B_CONTRA('a => 'b => unit)

    function f_a_to_a_to_u(_ : Animal) : (Animal => unit) = f_a_to_u
    function f_a_to_c_to_u(_ : Animal) : (Cat => unit) = f_c_to_u
    function f_c_to_a_to_u(_ : Cat) : (Animal => unit) = f_a_to_u
    function f_c_to_c_to_u(_ : Cat) : (Cat => unit) = f_c_to_u

    function f_u_to_u(_ : unit) : unit = ()
    function f_a_to_u(_ : Animal) : unit = ()
    function f_c_to_u(_ : Cat) : unit = ()

    function f_dt_contra_a_to_u(_ : dt_contra(Animal)) : unit = ()
    function f_dt_contra_c_to_u(_ : dt_contra(Cat)) : unit = ()
    function f_dt_co_a_to_u(_ : dt_co(Animal)) : unit = ()
    function f_dt_co_c_to_u(_ : dt_co(Cat)) : unit = ()
    function f_u_to_dt_contra_a(_ : unit) : dt_contra(Animal) = DT_CONTRA(f_a_to_u)
    function f_u_to_dt_contra_c(_ : unit) : dt_contra(Cat) = DT_CONTRA(f_c_to_u)

    stateful function f_c() : Cat = Chain.create()
    stateful function f_a() : Animal = f_c()

    stateful function f_u_to_a(_ : unit) : Animal = f_a()
    stateful function f_u_to_c(_ : unit) : Cat = f_c()
    stateful function f_a_to_a(_ : Animal) : Animal = f_a()
    stateful function f_a_to_c(_ : Animal) : Cat = f_c()
    stateful function f_c_to_a(_ : Cat) : Animal = f_a()
    stateful function f_c_to_c(_ : Cat) : Cat = f_c()

    stateful function f_a_to_u_to_c(_ : (Animal => unit)) : Cat = f_c()
    stateful function f_c_to_u_to_a(_ : (Cat => unit)) : Animal = f_a()
    stateful function f_c_to_u_to_c(_ : (Cat => unit)) : Cat = f_c()

    stateful function f_u_to_dt_co_a(_ : unit) : dt_co(Animal) = DT_CO(f_u_to_a)
    stateful function f_u_to_dt_co_c(_ : unit) : dt_co(Cat) = DT_CO(f_u_to_c)

    stateful entrypoint init() =
        let va1 : dt_contra(Animal) = DT_CONTRA(f_a_to_u)  // success
        let va2 : dt_contra(Animal) = DT_CONTRA(f_c_to_u)  // fail
        let va3 : dt_contra(Cat)    = DT_CONTRA(f_a_to_u)  // success
        let va4 : dt_contra(Cat)    = DT_CONTRA(f_c_to_u)  // success

        let vb1 : dt_co(Animal) = DT_CO(f_u_to_a)  // success
        let vb2 : dt_co(Animal) = DT_CO(f_u_to_c)  // success
        let vb3 : dt_co(Cat)    = DT_CO(f_u_to_a)  // fail
        let vb4 : dt_co(Cat)    = DT_CO(f_u_to_c)  // success

        let vc1 : dt_inv(Animal) = DT_INV(f_a_to_a)  // success
        let vc2 : dt_inv(Animal) = DT_INV(f_a_to_c)  // success
        let vc3 : dt_inv(Animal) = DT_INV(f_c_to_a)  // fail
        let vc4 : dt_inv(Animal) = DT_INV(f_c_to_c)  // fail
        let vc5 : dt_inv(Cat)    = DT_INV(f_a_to_a)  // fail
        let vc6 : dt_inv(Cat)    = DT_INV(f_a_to_c)  // fail
        let vc7 : dt_inv(Cat)    = DT_INV(f_c_to_a)  // fail
        let vc8 : dt_inv(Cat)    = DT_INV(f_c_to_c)  // success

        let vd1 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Animal)  // success
        let vd2 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Cat)     // success
        let vd3 : dt_biv(Cat)    = DT_BIV(f_u_to_u) : dt_biv(Animal)  // success
        let vd4 : dt_biv(Cat)    = DT_BIV(f_u_to_u) : dt_biv(Cat)     // success

        let ve1 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_a_to_u)  // success
        let ve2 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_c_to_u)  // fail
        let ve3 : dt_inv_sep(Animal) = DT_INV_SEP_B(f_u_to_a)  // success
        let ve4 : dt_inv_sep(Animal) = DT_INV_SEP_B(f_u_to_c)  // fail
        let ve5 : dt_inv_sep(Cat)    = DT_INV_SEP_A(f_a_to_u)  // fail
        let ve6 : dt_inv_sep(Cat)    = DT_INV_SEP_A(f_c_to_u)  // success
        let ve7 : dt_inv_sep(Cat)    = DT_INV_SEP_B(f_u_to_a)  // fail
        let ve8 : dt_inv_sep(Cat)    = DT_INV_SEP_B(f_u_to_c)  // success

        let vf1 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_dt_contra_a_to_u)  // success
        let vf2 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_dt_contra_c_to_u)  // success
        let vf3 : dt_co_nest_a(Cat)    = DT_CO_NEST_A(f_dt_contra_a_to_u)  // fail
        let vf4 : dt_co_nest_a(Cat)    = DT_CO_NEST_A(f_dt_contra_c_to_u)  // success

        let vg1 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_dt_co_a_to_u)  // success
        let vg2 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_dt_co_c_to_u)  // fail
        let vg3 : dt_contra_nest_a(Cat)    = DT_CONTRA_NEST_A(f_dt_co_a_to_u)  // success
        let vg4 : dt_contra_nest_a(Cat)    = DT_CONTRA_NEST_A(f_dt_co_c_to_u)  // success

        let vh1 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_dt_contra_a)  // success
        let vh2 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_dt_contra_c)  // fail
        let vh3 : dt_contra_nest_b(Cat)    = DT_CONTRA_NEST_B(f_u_to_dt_contra_a)  // success
        let vh4 : dt_contra_nest_b(Cat)    = DT_CONTRA_NEST_B(f_u_to_dt_contra_c)  // success

        let vi1 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_dt_co_a)  // success
        let vi2 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_dt_co_c)  // success
        let vi3 : dt_co_nest_b(Cat)    = DT_CO_NEST_B(f_u_to_dt_co_a)  // fail
        let vi4 : dt_co_nest_b(Cat)    = DT_CO_NEST_B(f_u_to_dt_co_c)  // success

        let vj1 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_c : (Animal => unit) => Animal) : dt_co_twice(Animal)  // success
        let vj2 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_c : (Cat    => unit) => Cat   ) : dt_co_twice(Cat)     // success
        let vj3 : dt_co_twice(Cat)    = DT_CO_TWICE(f_c_to_u_to_a : (Animal => unit) => Animal) : dt_co_twice(Animal)  // fail
        let vj4 : dt_co_twice(Cat)    = DT_CO_TWICE(f_c_to_u_to_c : (Cat    => unit) => Cat   ) : dt_co_twice(Cat)     // success

        let vk01 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
        let vk02 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // fail
        let vk03 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // fail
        let vk04 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
        let vk05 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
        let vk06 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // success
        let vk07 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // fail
        let vk08 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
        let vk09 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
        let vk10 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // fail
        let vk11 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // success
        let vk12 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
        let vk13 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
        let vk14 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // success
        let vk15 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // success
        let vk16 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // success

        let vl1 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal)  // success
        let vl2 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_c_to_u : Cat    => Cat    => unit) : dt_contra_twice(Cat)     // fail
        let vl3 : dt_contra_twice(Cat)    = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal)  // success
        let vl4 : dt_contra_twice(Cat)    = DT_CONTRA_TWICE(f_c_to_a_to_u : Cat    => Cat    => unit) : dt_contra_twice(Cat)     // success

        ()
