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

GADT patterns allow type mismatches in some type parameters #6223

Closed
vicuna opened this issue Nov 4, 2013 · 3 comments
Closed

GADT patterns allow type mismatches in some type parameters #6223

vicuna opened this issue Nov 4, 2013 · 3 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Nov 4, 2013

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 =

@vicuna
Copy link
Author

vicuna commented Nov 4, 2013

Comment author: @lpw25

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.

@vicuna
Copy link
Author

vicuna commented Nov 4, 2013

Comment author: @lpw25

I have now convinced myself that this is in fact the correct behavior, so I will mark the issue resolved.

@vicuna
Copy link
Author

vicuna commented Nov 4, 2013

Comment author: @yallop

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

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