Ordering wrong in instance chain?

[bbarker]

There was some discussion around this, and a couple of people (paluh and paf31 :-)) found that the instance chain order seemed wrong: https://try.purescript.org/?gist=ffb4ebbf07b2feb00563e109f0ccf440&session=1f5015b2-f2f7-ea7d-9702-28da84846303

[acple]

Oh, I'd like to see the discussion, where did you do?
Ya I suppose current one may still be wrong.

The first instance is intended to match (h a -> h b) -> f (g (h a)) -> f (g (h b)), e.g. example2.
If I omit it, this only match the lowest type.
But I still don't understand why I can't write fundep as fa a b -> fa, fa fb b -> a, fa a b -> fb, fa fb a -> b.

[bbarker]

Sure! Here's the chat. https://functionalprogramming.slack.com/archives/C04NA444H/p1601480864221000?thread_ts=1601480864.221000&cid=C04NA444H

…

On Thu, Oct 1, 2020 at 2:12 AM acple ***@***.***> wrote: Oh, I'd like to see the discussion, where did you do? Ya I suppose current one may still be wrong. The first instance is intended to match (h a -> h b) -> f (g (h a)) -> f (g (h b)), e.g. example2. If I omit it, this only match the lowest type. But I still don't understand why I can't write fundep as fa a b -> fa, fa fb b -> a, fa a b -> fb, fa fb a -> b. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAG7XDSK3WCD46T32AZTZLLSIQMUFANCNFSM4R7UPFYQ> .

-- Brandon Barker brandon.barker@gmail.com

[acple]

Thank you, I got it.
Simply their discussion doesn't consider about intermediate functor mapping.
And the root issue is: less enough fundeps, as I mentioned beforeabove.
Therefore, type inference doesn't work in some important scenario.

[bbarker]

Sorry, was there a prior discussion somewhere - you said you mentioned before? I'd be interested in reading about it. I'd like to try implementing this in Idris 2, which doesn't have fundeps exactly, but does have dependent types. So any additional reading would be appreciated. Feel free to close the issue. Thanks!

…

On Thu, Oct 1, 2020 at 8:37 PM acple ***@***.***> wrote: Thank you, I got it. Simply their discussion doesn't consider about intermediate functor mapping. And the root issue is: less enough fundeps, as I mentioned before. Therefore, type inference doesn't work in some important scenario. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAG7XDWNB3WCDBGAJ2FYNK3SIUOFDANCNFSM4R7UPFYQ> .

-- Brandon Barker brandon.barker@gmail.com

[acple]

I opened #2, please check it!
Thank you too!