Hello,

Recursive definitions need to be explicitly annotated to be polymorphic.
The (type a) annotation
introduces an abstract type a in the body of the function but does not make
it polymorphic.
The annotation type a. on the other hand, does both.

See http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227 for the
details.

Cheers,
Nicolas


On Fri, Mar 24, 2017 at 10:20 AM, Grumpy <grumpy@drno.eu> wrote:

> Hello,
>
> I think there is an incoherency or a bug somewhere in the type inference
> engine with the following code with version 4.02.3 (I have not tested in
> previous versions). Both functions eval and eval2 are identical but the
> inferred types are different, and the type inferred for eval2 is
> actually wrong.
>
> The function eval is typed correcly ('a exp -> 'a) while the type
> inferred for funcion function eval2 is (int exp -> int), which is wrong
> because of the Inc case returning ('a exp -> 'a).
>
> It seems the syntax (type a) leads to this incorrect behaviour...
>
>
> type _ exp =
>   | Stop : int exp
>   | Inc : (int exp -> int) exp
>
> let rec eval : type a. a exp -> a = function
>   | Stop -> 0
>   | Inc -> (fun (p : int exp) -> 1 + eval p)
>
> let rec eval2 (type a) (p : a exp) : a =
>   match p with
>   | Stop -> 0
>   | Inc -> (fun (p : int exp) -> 1 + eval2 p)
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>