[Caml-list] Polymorphic recursion and GADTs

[Lukasz Stafiniak <lukstafi@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2797 bytes --]

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 term
and integer

and boolean

external 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 term
       but a pattern was expected which matches values of type integer term
       Type boolean is not compatible with type integer
but 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 place
and a
and b

type (_, _) nearby =
  | Here : (*∀'b.*)'b place * 'b place -> ('b, 'b) nearby
  | Transitive : (*∀'a, 'b, 'c.*)('a, 'b) nearby * ('b, 'c) nearby ->
    ('a, 'c) nearby
type boolean

external is_nearby : (('a, 'b) nearby -> boolean) = "is_nearby"
type _ ex1 =
  | Ex1 : (*∀'a, 'b.*)('b place * ('a, 'b) nearby) -> 'a ex1
external wander : ('a place -> 'a ex1) = "wander"
type (_, _) meet =
  | Same : (*∀'b.*) ('b, 'b) meet
  | NotSame : (*∀'a, 'b.*) ('a, 'b) meet
external 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 get
Error: This expression has type b place
       but an expression was expected of type a place
       Type b is not compatible with type a
And when we switch to the ['a.] syntax, we get
Error: This definition has type 'a. 'a place -> 'a place -> ('a, 'a) nearby
       which is less general than
         'a 'b. 'a place -> 'b place -> ('a, 'b) nearby

Thanks in advance for any thoughts.
If you are curious, the source code is:
https://github.com/lukstafi/invargent/blob/master/examples/simple_eval.gadt
https://github.com/lukstafi/invargent/blob/master/examples/equational_reas.gadt

[-- Attachment #2: Type: text/html, Size: 4350 bytes --]