Re: [Caml-list] Polymorphic recursion and GADTs

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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

You must not use a type annotation here ('t47), because its (implicit)
scope is above. Removing the annotation or using _ in lieu of the free type
variable solves your problem. See this recent bugreport where the same
question was raised:
  http://caml.inria.fr/mantis/view.php?id=6264


On Tue, Dec 10, 2013 at 3:24 PM, Lukasz Stafiniak <lukstafi@gmail.com>wrote:

> I have another challenge for you. Without the redundant annotations (i.e.
> with only an annotation on let-rec) it type-checks nicely. I am providing
> more annotations as an option.
> >>>
> 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
>   | Pair : (*∀'a, 'b.*)'a term * 'b term -> (('a * 'b)) term
>   | Fst : (*∀'a, 'b.*)(('a * 'b)) term -> 'a term
>   | Snd : (*∀'a, 'b.*)(('a * 'b)) term -> 'b 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 : type 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)
>     | Pair (x, y) -> (eval x, eval y)
>     | Fst p -> let ((x, y): (a * 't47)) = eval p in x
>     | Snd p -> let ((x, y): ('t59 * a)) = eval p in y): a term -> a)
> <<<
> We get at "eval p" to the right of "let ((x, y): (a * 't47))":
> Error: This expression has type a * b#0
>        but an expression was expected of type a * b#0
>        The type constructor b#0 would escape its scope
>
>

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