Gabriel Scherer
Gabriel Scherer
Excellent feedback, thanks! > In my mind, the discussion of `sort_nondep` should be relegated to an explicitly-delimited remark, because it is of secondary interest; it discusses a work-around that used...
I modified the PR to take @fpottier's comments into account, and updated the [rendered PDF](https://www.irif.fr/~scherer/tmp/modular-explicits-manual.pdf).
Thanks! Rebased.
Hmm, don't hold your breath. Modifying the type-checker requires very technical work, the number of people with expertise enough to do this is small and they are busy, and it's...
> any explicit type pattern matched against a universal has to match before the GADT-induced equalities are available, while existential matches can happen afterwards. Because OCaml's syntax doesn't allow non-variables...
I tried to use this feature again today and hit the same limitation. The code was somewhat complex, but could be simplified into the following: ```ocaml type _ ty =...
My gut feeling is that if we hesitate between two values, we should use the lower one, because the runtime is known to sometimes degrade sharply in contended settings.
(cc @goldfirere)
@garrigue where do we stand on this PR? We need to know whether we want the change or not. If "yes", we should ask someone to rebase to move forward.
If I understand correctly, the principality issue comes from the fact that the proposed bidirectional type-checking relies on information that was inferred, not explicitly annotated, to propagate type information. The...