Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
vicuna opened this issue Mar 24, 2012 · 1 comment
Assignees

Comments

@vicuna
Copy link

vicuna commented Mar 24, 2012

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.

@vicuna
Copy link
Author

vicuna commented Mar 25, 2012

Comment author: @garrigue

Fixed both in 4.00 and trunk, by restricting optional parameter elimination through coercions to variables and applications. (typecore.ml, revisions 12269 and 12270)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants