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

GADTs, abstract types and the error "a type variable cannot be deduced..." #7605

Closed
vicuna opened this issue Aug 16, 2017 · 5 comments
Closed

Comments

@vicuna
Copy link

vicuna commented Aug 16, 2017

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.

@vicuna
Copy link
Author

vicuna commented Aug 16, 2017

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

@vicuna
Copy link
Author

vicuna commented Aug 16, 2017

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?

@vicuna
Copy link
Author

vicuna commented Aug 16, 2017

Comment author: rlepigre

Oh, actually, I thought that variance annotations did not allow invariance...

@vicuna
Copy link
Author

vicuna commented Aug 16, 2017

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.

@vicuna
Copy link
Author

vicuna commented Aug 16, 2017

Comment author: rlepigre

OK, I think I'll use private types then, since I have control over the library I'm using. Thanks!

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

1 participant