Less enough Functional dependencies

[acple]

For type inference, I think this should/can have fundeps as:

class NestedFunctor fa fb a b | fb a b -> fa, fa fb b -> a, fa a b -> fb, fa fb a -> b where

But it doesn't work.

I don't know why. Please HELP!
Is this a compiler issue or not?

[ursi]

I was about to put in a PR but then I noticed this issue.

Let's look at the type signature for nmap. We see it's

nmap :: NestedFunctor fa fb a b => (a -> b) -> fa -> fb

So how do we want this to behave? Well, if we give it an a -> b and we give it an fa, there should only be one possibility for fb. Therefore, I think the only FD we need is

a b fa -> fb

I noticed when trying to do something like

show $ add 1 <$$> [ Just 0 ]

it wouldn't work unless I added the type signature Array (Maybe Int) to the value. If we check the type of add 1 <$$> [ Just 0 ] in the REPL, we get

> :t nmap (add 1) [Just 0]
forall t2. NestedFunctor (Array (Maybe Int)) t2 Int Int => t2

because t2 is a type variable, it has no Show instance, so show throws a type error. This is not the behaviour we want. We know this expression only has one possible type - Array (Maybe Int).

If we change the FDs to just a b fa -> fb and try again we get

> :t nmap (add 1) [Just 0]
Array (Maybe Int)

this is exactly what we'd expect, and now show works without having to provide a type signature!

---

Regarding your question as to why those FDs don't compile together, I'm actually not sure, but the one that is causing problems is the only one I think we need - fa a b -> fb. If you remove just that one or if you remove all but that one it works fine. Do you have an example of why any of the other FDs are needed?

p.s. really cool trick, I didn't know this was possible!

[acple]

| fa a b -> fb, fa fb a -> b and | fb a b -> fa, fa fb b -> a are both correct but each have another process of type resolution.
If we choose former one, some Test functions won't be compiled. (see test6 function)
And also identity <$$> [Just 0] with latter one needs more type signatures as you know.

So I believe this should be | fb a b -> fa, fa fb b -> a, fa a b -> fb, fa fb a -> b, but it doesn't work.

The similar example is here.

class TestClass a b c | a b -> c, a c -> b where
  func :: a -> b -> c

instance instanceA :: TestClass a (f a) a where
  func = unsafeCoerce
else
instance instanceB :: TestClass a b b where
  func = unsafeCoerce

test :: Int -> Int
test = func unit
--     ^^^^^^^^^
--   Could not match type
--
--     t3 Unit
--
--   with type
--
--     Int
--
--
-- while solving type class constraint
--
--   Test.TestClass Unit
--                  Int
--                  Int
--
-- while applying a function func
--   of type TestClass t0 t1 t2 => t0 -> t1 -> t2
--   to argument unit
-- while checking that expression func unit
--   has type Int -> Int
-- in value declaration test
--
-- where t0 is an unknown type
--       t1 is an unknown type
--       t2 is an unknown type
--       t3 is an unknown type

I expected this chooses instanceB with Unit -> Int -> Int but was instanceA.
Is this bug/edge case of compilers?

[ursi]

Oh wow, I neglected to notice you had a test suite. I will give that a look.

[ursi]

I may have figured out your TestClass problem. I think it matches the first type variable in instanceA and once it does that it commits and can't backtrack. If we switch them around, it works.

class TestClass a b c | a b -> c, a c -> b where
  func :: b -> a -> c

instance instanceA :: TestClass (f a) a  a where
  func = unsafeCoerce
else
instance instanceB :: TestClass b a b where
  func = unsafeCoerce

test :: Int -> Int
test = func unit

[acple]

Oh, you forget swapping FD's typevars.
That's same result if I correct your FD. | a b -> c, b c -> a

[ursi]

it actually doesn't make sense anyway since b unifies (I think I'm using that right) with Unit and c unifies with Int, but instanceB requires b and c to be the same. I need to go to bed lol. This is interesting stuff.

[ursi]

looks like it's a bug
https://functionalprogramming.slack.com/archives/C04NA444H/p1602933949458200?thread_ts=1602918736.449900&cid=C04NA444H

hdgarrood

I think this might be a bug. In test, the use of func ought to be inferred as needing the type Unit -> Int -> Int, which would mean we are looking for an instance TestClass Unit Int Int, which the first instance clearly doesn’t match. There are already a couple of bugs around MPTCs and instance chains, I wonder if this is related

[acple]

If it is fixed, this will work! 😄

However,
I know some scenarios are still affected by this issue, we need that will be fixed too for a good type inference experience.