('a : value mod non_float) or_null is non_float
#4158
Conversation
| @@ -96,7 +96,7 @@ Line 1, characters 19-30: | |||
| ^^^^^^^^^^^ | |||
| Error: This type "int or_null" should be an instance of type | |||
| "('a : immediate_or_null)" | |||
| The kind of int or_null is immediate_or_null with int | |||
| The kind of int or_null is immediate_or_null mod non_float with int | |||
There was a problem hiding this comment.
Hmm. immediate should imply non_float. It's impossible to have a non-pointer float.
There was a problem hiding this comment.
Fixed. Before, immediate_or_null had to be maybe-separable because 'a or_null had kind immediate_or_null with 'a, but now the kind is value_or_null with magic.
typing/ctype.ml
Outdated
| called from [constrain_type_jkind]; the jkind returned without | ||
| substing is just weaker than the one we would get by substing. *) | ||
| jkind_subst env level type_decl.type_params args jkind | ||
| let substituted_jkind = |
There was a problem hiding this comment.
I don't think this is quite the right implementation strategy.
Instead, I think we should view or_null as closer to an [@@unboxed] type. Interestingly, estimate_type_jkind does not treat [@@unboxed] types specially. The special treatment for [@@unboxed] types comes in constrain_type_jkind, which knows how to look inside them. This is all ok, because estimate_type_jkind can just return an upper bound. This means that the separability of ty or_null can be maybe_separable for any ty -- as returned from estimate_type_jkind. But we must work harder in constrain_type_jkind to make up for this.
The way I think would work better is to teach unbox_once about or_null. unbox_once could return a new constructor Stepped_or_null (or something) in the or_null case. Critically, in constrain_type_jkind, before recurring on the type in the or_null, we have to adjust the jkind passed to loop, much like the existing use of Jkind.apply_modality_r call on line 2572.
I think this new implementation strategy is more "with the grain" of current things, and it also should empower more inference: if we have val f : 'a or_null accepts_non_float -> ..., we'll be able to infer that 'a is mod non_float too. (I don't think this works with the current implementation.)
There was a problem hiding this comment.
Yeah, you're right. We want to eventually unify Variant_with_null with Variant_unboxed anyway.
Done.
|
Now, |
Change
or_nullto benon_floatwhen its type argument is itselfnon_float. We can't express this behavior withmod-bounds, so hardcode it in
estimate_type_jkindforor_nullitself and types marked as re-exportingor_nullthrough the magic[@@or_null_reexport]attribute.This change has no risk on its own, since
'a or_nullcan't be put into arrays regardless. However, a subsequent PR will allow'a or_null array.