Comment author: mdl

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

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.

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.

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.)

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.

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.