Original bug ID: 5554
Reporter: rdicosmo
Assigned to: @garrigue
Status: closed (set by @garrigue on 2012-03-25T07:03:53Z)
Resolution: fixed
Priority: normal
Severity: minor
Fixed in version: 4.00.0+dev
Category: typing
Monitored by: @hcarty

Bug description

Type annotations typically used in GADT do not to always propagate in the body of a function if the function has some local definitions before the code that needs the annotation.

Steps to reproduce

Consider this GADT declaration

type empty
type nonempty
type ('a, 'b) l =
    Nil : (empty, 'b) l
  | Cons : 'b * ('a, 'b) l -> (nonempty, 'b) l;;

If we define the function

let rec length : type a b. (a,b) l -> int = function
| Nil -> 0
| (Cons (_,r)) -> 1+ (length r);;

we get the expected type val length : ('a, 'b) l -> int = <fun>

But if we add a local definition in the middle

let rec length : type a b. (a,b) l -> int = 
let id : 'a -> 'a = fun x -> x in 
function 
  | Nil -> 0 | (Cons (_,r)) -> 1+ (id (length r));;

We get a typing error: the type checker no longer knows the two branches
are instances of a polymorphic function

      Characters 106-118:
    | Nil -> 0 | (Cons (_,r)) -> 1+ (id (length r));;
                 ^^^^^^^^^^^^
Error: This pattern matches values of type (nonempty, 'a) l
       but a pattern was expected which matches values of type (empty, 'b) l

If we add some extra annotation, we may manage to get the type through, as
in the following case that gives the type ('a, 'b) l -> int

let rec length : type a b. (a,b) l -> int = 
let id : 'a -> 'a = fun x -> x in 
fun x -> match (x : (a,b) l) with
  | Nil -> 0 | (Cons (_,r)) -> 1+ (id (length r));;

Additional information

Didier Remy greatly simplified the example allowing to reproduce the issue:
with the type declaration

type 'a ty = Int : int -> int ty;;

we have that

   let f : type a. a ty -> a =
     fun x -> match x with Int y -> y;;

is accepted, but

   let g : type a. a ty -> a =
     let () = () in
     fun x -> match x with Int y -> y;;

is rejected, and adding annotations on x does not make the problem go away.