Hello,I am at a loss as to the difference between ['a.] syntax and [type a.] syntax of introducing polymorphic recursion. I will provide some examples. (Bear with me, they are automatically generated.)>>>type _ term =| Lit : integer -> integer term| Plus : integer term * integer term -> integer term| IsZero : integer term -> boolean term| If : (*∀'a.*)boolean term * 'a term * 'a term -> 'a termand integerand booleanexternal plus : (integer -> integer -> integer) = "plus"external is_zero : (integer -> boolean) = "is_zero"external if_then : (boolean -> 'a -> 'a -> 'a) = "if_then"let rec eval : 'a . ('a term -> 'a) =(function Lit i -> i | IsZero x -> is_zero (eval x)| Plus (x, y) -> plus (eval x) (eval y)| If (b, t, e) -> if_then (eval b) (eval t) (eval e))<<<The above produces:Error: This pattern matches values of type boolean termbut a pattern was expected which matches values of type integer termType boolean is not compatible with type integerbut if we replace the corresponding line with:>>>...let rec eval : type a . (a term -> a) =...<<<then it compiles fine.Now to a more complex example. According to my understanding (and InvarGenT), the following code should type-check:>>>type _ place =| LocA : a place| LocB : b placeand aand btype (_, _) nearby =| Here : (*∀'b.*)'b place * 'b place -> ('b, 'b) nearby| Transitive : (*∀'a, 'b, 'c.*)('a, 'b) nearby * ('b, 'c) nearby ->('a, 'c) nearbytype booleanexternal is_nearby : (('a, 'b) nearby -> boolean) = "is_nearby"type _ ex1 =| Ex1 : (*∀'a, 'b.*)('b place * ('a, 'b) nearby) -> 'a ex1external wander : ('a place -> 'a ex1) = "wander"type (_, _) meet =| Same : (*∀'b.*) ('b, 'b) meet| NotSame : (*∀'a, 'b.*) ('a, 'b) meetexternal compare : ('a place -> 'b place -> ('a, 'b) meet) = "compare"let rec walk : type a b . (a place -> b place -> (a, b) nearby) =(fun x goal ->((function Same -> Here (x, goal)| NotSame ->let Ex1 ((y, to_y)) = wander x in Transitive (to_y, walk y goal)))(compare x goal))<<<Here we getError: This expression has type b placebut an expression was expected of type a placeType b is not compatible with type aAnd when we switch to the ['a.] syntax, we getError: This definition has type 'a. 'a place -> 'a place -> ('a, 'a) nearbywhich is less general than'a 'b. 'a place -> 'b place -> ('a, 'b) nearbyThanks in advance for any thoughts.If you are curious, the source code is: