ocamlreason

OCaml error: "The present constructor Function__webkit_gradient has a conjunctive type"


What this error means and how can i solve it? I am trying to generate types based on the CSS spec at styled-ppx and got stuck at this error that i dont know how to it fix neither what that means exactly.

I tried to get OCaml inference from the target file with dune using (ocamlc_flags -i :standard) because my suspect is that infered types and generated types are crashing since both are polymorphic variants, but had problems generating targets.

You can check the pull request with the problem being reproducible here


Solution

  • In your ppx code,

      let mk_typ = (name, types) => {
        let core_type = ptyp_variant(types, Closed, None);
    

    it is unlikely that the meaning of types matches your expectation.

    In this context, the list of type types represents an intersection (aka a conjunction) of types. For instance, in

    type 'a t = [< `A of int & float ] as 'a
    

    the types list would contain the ast nodes for the type int and float. (You can have a look at the latest version of OCaml manual https://ocaml.org/api/compilerlibref/Parsetree.html#TYPErow_field_desc to have more detailed description of those AST nodes.)

    You probably meant to box the list of types in a product type

    type t = [ `A of (int * float) ]
    

    Indeed, polymorphic variant constructors always have arity one. Otherwise, `A _ * _ would not be unifiable with `A of _.

    Concerning your exact error message, the conjunctive type error that you are half-describing is likely related to the fact that conjunctive (like int & float) are only allowed as argument of polymorphic variant constructors in the upper bound of a polymorphic variant type. In other words,

    type 'a t = [< `A of int & float ] as 'a
    

    is fine because we are on the right-hand side of <. But both

    type 'a t = [> `A of int & float ] as 'a
    

    and

    type t = [ `A of int & float ]
    

    yields an error

    Error: The present constructor A has a conjunctive type
    

    because the conjunction of types appears in the lower bound of the type which lists the constructors that were explicitly present.

    EDIT: Why are conjunctive types sometimes allowed?

    Having conjunctive types makes it possible to use functions that have incoherent interpretation of some constructors. For instance, I could have a function that works on either `A of int or `B of float

    let f = function
    | `A n -> float_of_int n
    | `B f -> f
    

    and another function that expects both `A and `B to have a float argument

    let g (`A f | `B f ) = f
    

    If I try to apply f and g on the same argument

    let h x = f x +. g x
    

    I end up in a situation where h can be applied to `B 0. without trouble

    let z = h (`B 0.)
    

    but trying to use h on `A _ for any _ cannot work

    let error = h (`A 0)
    
    Error: This expression has type [> `A of int ]
           but an expression was expected of type
             [< `A of float & int | `B of float ]
           Types for tag `A are incompatible
    

    This is the kind of situation where conjunctive types arise: h has type [< `B of float | `A of int & float ] -> float. Moreover, we can wait to get a concrete argument of the form `A of x to check if the constructor argument x fit in the conjunction of types int & float. In this specific case, we know that there are no types that are both int and float, but more complex cases can happen, and delaying the check is a simple way to handle all cases.

    Contrarily, when we have a concrete value of type [> `A of 'x ], there is no reason to delay this check. Thus it is not possible to construct a positive value that has a conjunctive type in OCaml. Consequently, it forbids the possibility to write types with conjunctive types in a positive position.