Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005554OCamlOCaml typingpublic2012-03-24 08:172012-03-25 09:03
Reporterrdicosmo 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.00.0+dev 
Summary0005554: Type annotation do not always propagate when defining a function that contains local definitions (seen with GADT) in 3.13.0+dev1
DescriptionType 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 ReproduceConsider 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 InformationDidier 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.
TagsNo 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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker