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

Trivial GADT functions are untypable #7877

Closed
vicuna opened this issue Nov 26, 2018 · 6 comments

Comments

Projects
None yet
1 participant
@vicuna
Copy link

commented Nov 26, 2018

Original bug ID: 7877
Reporter: mdl
Assigned to: @yallop
Status: resolved (set by @yallop on 2018-11-26T06:33:49Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.07.1
Category: typing

Bug description

I have attached a file: one where the function "Tl.tl" types, and one where the function "To_string.to_string" types; each file needs a slightly different definition of "t" in order for the corresponding function to typecheck. But no amount of annotation seems to allow for a "t" that can type both some version of "tl" and "to_string".

Just as a sanity check, I tried writing an equivalent of to_string.ml in GHC Haskell using its GADTs extension, and I can get "tl" to type there, so I don't think I'm doing something wrong, but if I am, then sorry for the support ticket masquerading as a bug. :)

File attachments

@vicuna

This comment has been minimized.

Copy link
Author

commented Nov 26, 2018

Comment author: mdl

I meant "module To_string" rather than "to_string.ml" in the second paragraph--sorry for the extra noise.

@vicuna

This comment has been minimized.

Copy link
Author

commented Nov 26, 2018

Comment author: @yallop

I don't see anything that suggests a compiler bug here, but there are a few problems in your code, so your question belongs elsewhere (e.g. the mailing list or the online forum).

Here's some advice before you do ask elsewhere: (1) think carefully about what your type definitions actually mean. Once you have the types right, everything else willbecome easier. (2) for the moment, stop using '_' in type definitions, and use named type variables instead.

@vicuna vicuna closed this Nov 26, 2018

@vicuna

This comment has been minimized.

Copy link
Author

commented Nov 26, 2018

Comment author: mdl

I would appreciate a little civility; I already said that if I'm making a mistake, then I'm sorry. Would you like to tell me what it is, or is it more entertaining for you to simply lord it over me? Is this how you normally treat people who submit bugs in good faith?

I did in fact try using named type variables. I also tried multiple OCaml versions to see if this was a regression, as I saw similar code online that suggested what I was doing did work at some point.

@vicuna

This comment has been minimized.

Copy link
Author

commented Nov 26, 2018

Comment author: mdl

The "problem" (?) turned out to be that not defining constructors on "zero" and "succ" made the otherwise correct definition for "t" (in "module To_string") fail with the following error:

In this definition, a type variable cannot be deduced
from the type parameters.

So the problem partly involved needing named type variables, but I don't see why "zero" or "succ" require the addition of constructors that are not even being used anywhere in the code. I'll attach the working OCaml version as well as the Haskell code, which may help others who come across this issue, or you, if you decide there's actually an issue here (feel free to consider it a documentation bug, if you prefer.)

@vicuna

This comment has been minimized.

Copy link
Author

commented Nov 26, 2018

Comment author: @lpw25

I don't think @yallop was being uncivil or lording it over to you. His answer reads like what a teacher would say when trying to lead a student towards an answer rather without giving it outright, presumably because they think that the student will learn more that way. I can see why you might just want a more direct answer, but that doesn't mean that @yallop was being rude by taking a more pedagogical approach.

I'm happy to give a more direct answer, but I'm not entirely sure what you are trying to do with the Tl.t type so you'd need to give some explanation of what you are trying to do there. Your To_string.t type is clearer, and for that you seem to have a couple of issues:

  1. The definition of Cons needs to use a type variable where you have two _s. Otherwise there is nothing connecting the length of the list with the length of its tail.

  2. You need to give some constructors to the [zero] and [succ] types. Currently they are abstract and could stand for any type definition. By adding constructors you rule out definitions like:

    type zero
    type 'a succ = int

    which would make the [_] in your definition of [Cons] unconnected to the parameters of [t] -- this is what the error message you got is saying.

It also rules out definitions like:

    type zero
    type 'a succ = zero

which would make definitions like your [hd] and [tl] functions unsound.
@vicuna

This comment has been minimized.

Copy link
Author

commented Nov 26, 2018

Comment author: mdl

Thank you. This is much more helpful, and again, my intent was not to place this in the wrong venue. I should have explained myself better regarding [Tl.t]: obviously it was incorrect, but I supplied it for sake of showing that it gave a "working" [Tl.tl], albeit with a suspicious signature.

I was further confused by the behavior of the types I'd written for [zero] and [succ]--it didn't occur to me that they weren't behaving as I had intended; I was not considering the module system, and that even without a sharing constraint, "empty" type declarations are in fact abstract in a structure--this makes sense now.

I apologize for the earlier frustrated reply, but this interaction here is admittedly subtle, between the cryptic error message and the subtle interaction with module system concerns. (I have respected both your work from a distance, so I was a little taken aback--I'm aware of the restrictions that various module system constructs impose, e.g. why higher-kinded types require the indirections outlined in the paper you authored with @yallop a few years ago, the things your work on modular implicits are intended to solve, related work in 1ML, etc.--but I'm willing to admit this was a brain-fart on my part!)

Cheers.

@vicuna vicuna added typing bug labels Mar 14, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.