Search code examples
ocamltype-inferencealgebraic-data-typessubtypingrefinement-type

Ocaml disambiguates inferred types by their proximity to the value?


type large1 = Int of int | Bool of bool
type small1 = Int of int    
let intersect1 = Int 0

The ocaml top-level (4.01.0) infers the type of intersect1 as small1. I thought I understood why: small1 looks like a subtype (or refinement type) of large1.

But now:

type small2 = Int of int
type large2 = Int of int | Bool of bool    
let intersect2 = Int 0

The top-level now infers a type of large2 for intersect2. This makes it look like proximity is used as a tiebreaker, but that's pretty surprising and unlike other languages I have used, so i suspect there is something subtle here I'm misunderstanding.

One complication: as noted in the question that inspired the answer that inspired this question, the "closer" type doesn't completely hide the further one.

type left = Int of int | Dem
type right = Int of int | Gop

let zell (x:left) =
  match x with
    Int v -> Int v
  | Dem -> Gop

zell is given the type left -> right.

What are the specific rules for inferring these types, and where in the manual (or any other published papers or documentation) can I read more?

This question was inspired by an older answer to a question about polymorphic variants.


Solution

  • OCaml has "type-directed" disambiguation of record fields and constructors these days.

    It was added to the language as of OCaml 4.01.0, released September 12, 2012. The release notes refer to this link for further information:

    Type-based selection of record labels and constructors.

    Here's a good writeup that describes the thought processes for making the change:

    Resolving Field Names

    And here is a followup with more details:

    Resolving Field Names 2

    I can't find this feature mentioned in the OCaml manual (as you say).