Jacques Garrigue
Jacques Garrigue
I'll try to answer your questions, but I'm not the original author of the code... > * What is the role of `check_well_founded`, what does it mean to be "well-founded"?...
> What is an example of an "internal cycle" that needs [check_well_founded] to continue checking under guarding type constructors? It might be that the second call inside `transl_declaration` removed the...
Following your remark about not needing to recurse on non-root paths, I have simplified the code. `check_well_founded` now only recurses until it finds a guarded node, or a node that...
I tried to include all your suggestions, except for the documentation. The behavior has been much simplified, so maybe we can come up with something. Concerning ```ocaml (* new behavior...
Actually, this is not a single graph, but rather n different graphs depending on which type you start from. This is because type abbreviations can be used polymorphically in other...
Is it really what we want? This would only report abbreviations as cyclic if if they expand to themselves without going through the expansion of another abbreviation. For instance ```ocaml...
While the impact is not clear, this is an important concern.
Still dreaming it could come back...
There is a good reason why both definitions are rejected: in both cases `p` cannot be defined without first knowing the definition of `q`. In the past, there has been...
Here is a workaround in your case: ```ocaml type ('a, 'b) either = Left of 'a | Right of 'b type ('a, 'b, 'c, 'd) either4 = In1 of 'a...