04:30 <discocaml> <Nezteb> Not super sure where to post this, but when I try to sign into https://reasonml.chat/ with GitHub, I approve the OAuth connection but get this error message every time. It happens in both Brave and Chrome. 🤔

04:30 <discocaml> <Nezteb> https://cdn.discordapp.com/attachments/436568060288172044/1087956551450492948/Screenshot_2023-03-21_at_9.30.09_PM.png

04:55 <discocaml> <hopefullyhat> link?

05:32 <discocaml> <anmonteiro> cc @Manas (prometheansacrifice)

05:51 <discocaml> <darrenldl> <https://discuss.ocaml.org/t/what-are-the-biggest-reasons-newcomers-give-up-on-ocaml/10958>

10:02 <discocaml> <octachron> @beheddard : since the first partial application could have a effect, it is wrong in general to reject it. You could reverse the first and second argument to impose the constraint that the spatial type is compatible with an existing instance of `t`. All other workaround would be similar I think (aka having a first proof-only argument that enforces that the spatial type is meaningful).

15:56 <discocaml> <geoff> Right, I wasn't thinking of an effect from the partial application 🤦🏻‍♂️(that aren't necessarily using the argument that can be an incorrect type). Yea, I realized begrudgingly that a reversal would clear things up, but unfortunately the shape really has to be last for chaining transformations together ergonomically.

15:56 <discocaml> <geoff>

15:56 <discocaml> <geoff> So with early rejection off the table, could the type error message at least use the information about the possible variants of `t`? I guess nothing can be done about the partial application inferred type since the first argument could be ignored anyway. Though I still wonder at the utility of such an uncompletable function.

16:05 <discocaml> <octachron> I see two potential issues

16:05 <discocaml> <octachron> - first, checking that a type is uninhabited is undecidable: the refutable clause construct in patterns is carefully designed to ask the user how much effort they want the typechecker to spend.

16:06 <discocaml> <octachron> - second, having an uninhabited type as a function argument is probably an error, but it is error somewhere in the past.

16:07 <discocaml> <octachron> In your case, it is clear that it is the first application that is problematic; but the empty type could be a result of n contradictory constraints without a clear pair of constraints responsible for the ultimate contradiction.

16:54 <discocaml> <geoff> Thanks for the answers/clarifications 🙏.

16:54 <discocaml> <geoff>

16:54 <discocaml> <geoff> By "n contradictory constraints" do you mean the other type variables that the first application has nothing to do with? E.g. the 'space parameter, which doesn't inform the others as far as the type signature is concerned. I guess there are cases more complicated than mine that would make what I'm asking about for the error message problematic (more parameters and more variants).

16:54 <discocaml> <geoff>

16:54 <discocaml> <geoff> It just *feels* like something matching against the incorrect type parameter slot in the existing variants of `t` to give a single option (or a list, if there are multiple variants sharing a type parameter) to the user on failure should be possible (to my uneducated self).

17:02 <discocaml> <octachron> Imagine that you have encoded a sudoku in the type system, with function that update one case at a time. You can end up with an unsolvable grid, but it is the set of update that is responsible for the absence of solution, not really a single update.

17:05 <discocaml> <octachron> Exploring the set of possibility is more a meta-language concern, and there are tools to do so: `#show t` for instance, or the documentation.

17:15 <discocaml> <geoff> Ok I think I understand that example better. I know they can look at my doc's, and it should be clear on thinking about it a little, but I still feel a pang of guilt about choosing this path that comes with funny tooltip and error messages 😅.

17:18 <discocaml> <geoff> I still like the tradeoff that avoids 2d/3d versions of all the functions, but I wondered at how unavoidable the downside is (which as you say, shouldn't be the end of the world since the user should be able to figure out what they've done based on looking at the docs and/or using their brain)