The following implementation comes closer to the original semantics of the ADT implementation. type _ value' = | GBool : bool -> bool value' | GInt :

The following implementation comes closer to the original semantics of the ADT implementation. type _ value' = | GBool : bool -> bool value' | GInt : int -> int value' type _ expr' = | GValue : 'a value' -> 'a expr' | GIf : bool expr' * 'a expr' * 'a expr' -> 'a expr' | GEq : 'a expr' * 'a expr' -> bool expr' | GLt : int expr' * int expr' -> bool expr' let rec eval' : type a. a expr' -> a = function | GValue (GBool b) -> b | GValue (GInt i) -> i | GIf (b, l, r) -> if eval' b then eval' l else eval' r | GEq (a, b) -> (eval' a) = (eval' b) | GLt (a,b) -> a < b ;; eval' (GIf ((GEq ((GValue (GInt 2)), (GValue (GInt 2)))), (GValue (GInt 42)), (GValue (GInt 12))));; eval' (GIf ((GEq ((GValue (GInt 2)), (GValue (GInt 2)))), (GValue (GBool true)), (GValue (GBool false))));; It does not support having separate return types for the branches on an if-statement but I consider that to be a good thing ;) I should probably update the ADT example to dis-allow that.