You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
typeemptytypenonemptytype('a, 'b) l =
Nil : (empty, 'b) l
| Cons : 'b* ('a, 'b) l -> (nonempty, 'b) l;;
If we define the function
letrec 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
letrec length : type a b. (a,b) l -> int =letid : 'a -> 'a =funx -> x infunction|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
letrec length : type a b. (a,b) l -> int =letid : 'a -> 'a =funx -> 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 -> intty;;
we have that
letf : type a. a ty -> a =funx -> match x withInty -> y;;
is accepted, but
letg : type a. a ty -> a =let()=()infunx -> match x withInty -> y;;
is rejected, and adding annotations on x does not make the problem go away.
The text was updated successfully, but these errors were encountered:
Fixed both in 4.00 and trunk, by restricting optional parameter elimination through coercions to variables and applications. (typecore.ml, revisions 12269 and 12270)
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
If we define the function
we get the expected type
val length : ('a, 'b) l -> int = <fun>
But if we add a local definition in the middle
We get a typing error: the type checker no longer knows the two branches
are instances of a polymorphic function
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
Additional information
Didier Remy greatly simplified the example allowing to reproduce the issue:
with the type declaration
we have that
is accepted, but
is rejected, and adding annotations on x does not make the problem go away.
The text was updated successfully, but these errors were encountered: