Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Constraints are not handled symmetrically by jkind inference in type declarations #2993

Open
jbachurski opened this issue Aug 29, 2024 · 0 comments
Labels

Comments

@jbachurski
Copy link
Contributor

jbachurski commented Aug 29, 2024

As we found out in discussion with @lpw25, constraints are handled in a somewhat surprising way by Typedecl.transl_declaration:

let cstrs = List.map
(fun (sty, sty', loc) ->
transl_simple_type ~new_var_jkind:Any env ~closed:false Mode.Alloc.Const.legacy sty,
transl_simple_type ~new_var_jkind:Sort env ~closed:false Mode.Alloc.Const.legacy sty', loc)
sdecl.ptype_cstrs
in

Left hand sides of the constraint (sty) are kinded using the Any policy (unseen type variables get initialised to the top of the jkind lattice/currently any), while the right hand sides (sty') get Sort (initialised to the highest point below the representable space - currently sort variables).

This leads to the following surprising behaviour (note 'a : any, but 'b is left unbound):

type float64 : float64
[%%expect{|
type float64 : float64
|}]

type ('a : any) foo = 'a constraint 'a = 'b (* 'b gets a sort var, defaults to value *)
type foobar = float64 foo
[%%expect{|
type 'b foo = 'b
Line 2, characters 14-21:
2 | type foobar = float64 foo
                  ^^^^^^^
Error: This type float64 should be an instance of type ('a : value)
       The layout of float64 is float64
         because of the definition of float64 at line 1, characters 0-22.
       But the layout of float64 must be a sublayout of value
         because of the definition of foo at line 1, characters 0-43.
|}]

type ('a : any) foo = 'a constraint 'b = 'a (* 'b gets any as expected *)
type foobar = float64 foo
[%%expect{|
type ('a : any) foo = 'a
type foobar = float64 foo
|}]

After some thinking it seems the correct solution is to use Any in both cases.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants