0005554: Type annotation do not always propagate when defining a function that contains local definitions (seen with GADT) in 3.13.0+dev1

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005554

OCaml

OCaml typing

public

2012-03-24 08:17

2012-03-25 09:03

Reporter

rdicosmo

Assigned To

garrigue

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

4.00.0+dev

Summary

0005554: Type annotation do not always propagate when defining a function that contains local definitions (seen with GADT) in 3.13.0+dev1

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.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0007151) garrigue (manager) 2012-03-25 09:03	Fixed both in 4.00 and trunk, by restricting optional parameter elimination through coercions to variables and applications. (typecore.ml, revisions 12269 and 12270)

Issue History
Date Modified	Username	Field	Change
2012-03-24 08:17	rdicosmo	New Issue
2012-03-25 07:09	garrigue	Assigned To	=> garrigue
2012-03-25 07:09	garrigue	Status	new => assigned
2012-03-25 09:03	garrigue	Note Added: 0007151
2012-03-25 09:03	garrigue	Status	assigned => closed
2012-03-25 09:03	garrigue	Resolution	open => fixed
2012-03-25 09:03	garrigue	Fixed in Version	=> 4.00.0+dev