open Core
let rec sort (lst : 'a list) =
match lst with
| [] -> []
| head :: tail -> insert head (sort tail)
and insert elt lst =
let open Poly in
match lst with
| [] -> [ elt ]
| head :: tail -> if elt <= head then elt :: lst else head :: insert elt tail
in
let _ = sort [ "is"; "a"; "table"; "told"; "etc." ] in
let _ = sort [ 3.14; 2.718 ] in
let _ = sort [ 6; 2; 5; 3 ] in
()

The problem here, I believe is that sort starts with type 'a list -> 'a list
but the first call binds 'a to string, which causes the 2nd call to have an
error of:

37 | let _ = sort [ 3.14; 2.718 ] in
^^^^
Error: This expression has type float but an expression was expected of type
string

Question: without redefining sort, is there a way to make this code compile ?

let () =
(* Here is the line that is changed! *)
let rec sort : 'a. 'a list -> 'a list =
fun lst ->
match lst with [] -> [] | head :: tail -> insert head (sort tail)
and insert elt lst =
let open Poly in
match lst with
| [] ->
[elt]
| head :: tail ->
if elt <= head then elt :: lst else head :: insert elt tail
in
let _ = sort ["is"; "a"; "table"; "told"; "etc."] in
let _ = sort [3.14; 2.718] in
let _ = sort [6; 2; 5; 3] in
()

is that the type annotation (lst: 'a list) makes the function works only on list of a certain type 'a
and with the first call to sort

let _ = sort ["is"; "a"; "table"; "told"; "etc."] in

the typechecker will infer that 'a = int. Removing the annotation all together will fix the issue because then the type of sort will be generalized outside of its definition.
In other words,

let id x = x in
id 1, id "two"

is fine but not

let monomorphic_id (x:'a) = x in
monomorphic_id 1, monomorphic_id "error"

In other words, if you want to add annotation for debugging purpose, it is necessary to use an explicitly polymorphic annotation:

let id: 'a. 'a -> 'a = fun x -> x in
id 1, id "two"

If your functions were not polymorphicrecursive, using just a locally abstract type,

let sort (type a) (lst: a list) : a list = ...

would also have worked.

To avoid this caveat, I advise in general to use the `explicit polymorphic annotation with locally abstract types" short form:

let id: type a. a -> a = fun x -> x in
id 1, id "two"

which works in (almost) all case and more often than not lead to better and earlier error.

let fixpoint : 'a. ('a -> 'a) -> 'a -> 'a = fun f x ->
let open Poly in
let exception Done in
let x = ref x in
try while true do
let y = f !x in
if !x = y then raise Done else x := y
done; assert false
with Done -> !x;;

I am a little confused by this type signature of:

let fixpoint : 'a. ('a -> 'a) -> 'a -> 'a = fun f x ->

I would have expected something like:

let fixpoint : 'a : Equal. ('a -> 'a) -> 'a -> 'a = fun f x ->

Because of the two lines:

let open Poly in
...
if !x = y then raise Done else x := y
...

Intuitively, the forall 'a is strange reading because it does not
seem to be for all 'a, only those where Poly.(=) is defined.

My confusion here is how to think of type signatures of the form:

There is no ad-hoc polymorphism in OCaml, only parametric polymorphism. Thus the function (=): 'a -> 'a -> bool is defined for all types'a (even if it does fail dynamically on some memory representation). Type constraints of the form 'a . ... reads for all types 'a. ... . A more natural example would be:

let rec len: 'a. 'a list -> int = function
| [ ] -> 0
| _ :: q -> 1 + len q