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: 6223 Reporter:@lpw25 Assigned to:@lpw25 Status: closed (set by @xavierleroy on 2015-12-11T18:24:19Z) Resolution: not a bug Priority: normal Severity: minor Version: 4.01.0 Category: typing
Bug description
It seems that GADT patterns do not give unification errors for the parameters of types which may be non-injective. For example, in the following code, t is known to be injective and we get an error on the definition of f, but N.s is not known to be injective and we are allowed to use the Bar pattern with the wrong type.
type 'a t = T;;
type 'a t = T
type 'a foo = Foo : int t foo;;
type 'a foo = Foo : int t foo
let f (Foo: string t foo) = ();;
Characters 7-10:
let f (Foo: string t foo) = ();;
^^^
Error: This pattern matches values of type int t foo
but a pattern was expected which matches values of type string t foo
Type int is not compatible with type string
module N : sig type 'a s end = struct type 'a s = S end;;
module N : sig type 'a s end
type 'a bar = Bar : int N.s bar;;
type 'a bar = Bar : int N.s bar
let g (Bar: string N.s bar) = ();;
val g : string N.s bar -> unit =
The text was updated successfully, but these errors were encountered:
I'm actually not sure if this is a bug or not. It seems wrong to allow you to use a pattern with a different type than it was declared. On the other hand if I was to try to pattern match on a string N.s bar I need to include a case for Bar in case string N.s equals int N.s.
Either way I thought it was better to have a Mantis issue than to not have one.
This might be viewed as a design question rather than a bug. If N.s turns out to be non-injective then it's possible to construct a value of type string N.s bar that matches the pattern in g. For example, N may also export a coercion function
module M (S : sig type 'a t end) : sig
val coerce : 'a s S.t -> 'b s S.t
end
Original bug ID: 6223
Reporter: @lpw25
Assigned to: @lpw25
Status: closed (set by @xavierleroy on 2015-12-11T18:24:19Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.01.0
Category: typing
Bug description
It seems that GADT patterns do not give unification errors for the parameters of types which may be non-injective. For example, in the following code,
t
is known to be injective and we get an error on the definition off
, butN.s
is not known to be injective and we are allowed to use theBar
pattern with the wrong type.type 'a t = T;;
type 'a t = T
type 'a foo = Foo : int t foo;;
type 'a foo = Foo : int t foo
let f (Foo: string t foo) = ();;
Characters 7-10:
let f (Foo: string t foo) = ();;
^^^
Error: This pattern matches values of type int t foo
but a pattern was expected which matches values of type string t foo
Type int is not compatible with type string
module N : sig type 'a s end = struct type 'a s = S end;;
module N : sig type 'a s end
type 'a bar = Bar : int N.s bar;;
type 'a bar = Bar : int N.s bar
let g (Bar: string N.s bar) = ();;
val g : string N.s bar -> unit =
The text was updated successfully, but these errors were encountered: