Gabriel Scherer
Gabriel Scherer
My general impression is that there are many small places where the code could be factored/improved, and it would be nice, maybe a couple issues to fix, and maybe a...
@Octachron I believe that we need your help on the interaction between adding Tfunctor parameters to the environment and the printing of error traces. (@samsa1 mentioned this to you already.)...
I'm confused by this PR, the testsuite proposed, and the code. You have for example: ```ocaml module M = struct type t = true | false let \#true = 13...
I can think of two broad approaches that make sense to me: 1. `true` and `false` are (reserved) keywords, and in particular trying to rebind them as constructors should be...
Ah, of course: in practice we have implemented the core of (2) for a while, so there are chances that some people rebind `true` and `false` in their programs for...
I want a clear specification for what we should be doing before we handle five more issues about corner cases of `true` or `false`.
(cc @yallop who may be interested in this feature)
Side-note: I find it surprising that `(type a)` does not force generalizability, and I would prefer the `a option ref` example to be rejected with an error.
I don't think that handling this as an optional argument works well. Consider the case where you abstract over several type arguments in sequence, there is no way at application...
I think that this is a question that is weighting on @diremy's mind. Note: Coq/Rocq allows the application syntax `f (a := foo)` to explicit apply the implicit argument `a`...