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
GADTs, abstract types and the error "a type variable cannot be deduced..." #7605
Comments
Comment author: @yallop Rejecting the program is the correct behaviour here. The problem is as follows: when 't' is an abstract type it's not possible to reason backwards from the fact 'a t = 'b t to the fact 'a = 'b because t could be defined as follows type 'a t = unit There's (a lot) more discussion in #5985 |
Comment author: rlepigre I see. However, in my actual code, I have explicit variance annotations (i.e., "type (-'a,+'b) t"). Shouldn't this be accepted at least? |
Comment author: rlepigre Oh, actually, I thought that variance annotations did not allow invariance... |
Comment author: @yallop Unfortunately, variance annotations don't help. Since '+' means "is not used contravariantly" rather than "is used covariantly", the following is allowed: type +'a t = unit Injectivity annotations would solve the issue, but it's not clear how to add them without a lot of syntactic clutter. Depending on your use case, you might be able to use the new unboxed types (new in 4.04.0), which give you a distinct type with the same representation: type 'a t = T of 'a s [@@unboxed] (but you'll still need to explicitly convert between t and s) Or you may be able to use private types, like this: type ('a, 'b) t = private ('a -> 'b) With this second approach the definition of t is visible to the type checker, so the type checker can see that it's injective. However, 'private' only provides abstraction in one direction, so isn't appropriate in every case. |
Comment author: rlepigre OK, I think I'll use private types then, since I have control over the library I'm using. Thanks! |
Original bug ID: 7605
Reporter: rlepigre
Assigned to: @yallop
Status: resolved (set by @yallop on 2017-08-16T10:58:52Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.03.0
Category: language features
Monitored by: @gasche
Bug description
The definition of a GADT using an abstract type from some module is rejected with the error "In this definition, a type variable cannot be deduced from the type parameters.". Here is a minimal example.
##########
module B : sig type ('a,'b) t end =
struct
type ('a,'b) t = 'a -> 'b
end
type _ s = U : unit s
type _ q = Last : 'c s * ('c, 'b) B.t -> ('c, 'b) B.t q
##########
If the signature of the module B is removed, it is accepted.
Additional information
This example still fails using OCaml 4.05.0.
The text was updated successfully, but these errors were encountered: