SuperComposition instance resolution is brittle

[treeowl]

In GHCi:

ghci> :t ("b"++)
("b"++) :: [Char] -> [Char]
ghci> :t ('b':)
('b':) :: [Char] -> [Char]

ghci> :t (++"a") ... ("b"++)
(++"a") ... ("b"++) :: [Char] -> [Char]
ghci> :t (++"a") ... ('b': )

<interactive>:1:9: error:
    • Couldn't match type: [Char]
                     with: [Char] -> [Char]
        arising from a use of ‘...’
    • In the expression: (++ "a") ... ('b' :)

Ouch! I'd be tempted to go with something simpler:

infixl 8 ...

class SuperComposition x y b r | x y b -> r where
  (...) :: (x -> y) -> b -> r

instance {-# OVERLAPPABLE #-} (x ~ b, y ~ r) => SuperComposition x y b r where
  f ... g = f g
  {-# INLINE (...) #-}

instance {-# OVERLAPPING #-} (SuperComposition x y d r1, r ~ (c -> r1)) => SuperComposition x y (c -> d) r where
  (f ... g) c = f ... g c
  {-# INLINE (...) #-}

I used four parameters instead of three to be able to infer directly that the first argument of (...) is a function. We could do that with three parameters too, but it gets a little hacky and I don't see a real advantage.

[treeowl]

I'm struggling to find a solution that doesn't break too much code. As I understand it, we want

(...) :: (x -> y) -> x -> y
(...) :: (x -> y) -> (m -> x) -> (m -> y)
(...) :: (x -> y) -> (m -> n -> x) -> (m -> n -> y)
-- etc.

I see two basic approaches to this, starting from

class SuperComposition x y b r | x y b -> r where
  (...) :: (x -> y) -> b -> r

Analyze the second argument type

This requires the type checker to be able to determine exactly how many arrows are in the second argument. This is, roughly speaking, what we currently do, but with more principled overlap to avoid brittleness.

instance {-# OVERLAPPABLE #-} (x ~ b, y ~ r) => SuperComposition x y b r where
  f ... g = f g

instance {-# OVERLAPPING #-} (SuperComposition x y d r1, r ~ (c -> r1)) => SuperComposition x y (c -> d) r where
  (f ... g) c = f ... g c

Compare the result types

This requires the type checker to know the result type (or at least a whole lot about it), but it works great in that case.

instance {-# OVERLAPPABLE #-} (b ~ (b1 -> b'), r ~ (b1 -> r'), SuperComposition x y b' r') => SuperComposition x y b r where
  (f ... g) c = f ... g c

instance {-# OVERLAPPING #-} x ~ b => SuperComposition x r b r where
  f ... g = f g

There are different trade-offs, and neither of them seems to "just work" in an intuitive way. When they don't work out, the error messages can be rather bad, because of the way GHC picks an instance to complain about in the face of overlap. I suspect we might be able to combine the approaches: use an auxiliary class that takes as an argument the result of a type family comparing the results, and play some {-# INCOHERENT #-} tricks. It will require some care to get this right, and I am not terribly optimistic about the user experience even if we succeed, but the current situation is just awful.

[treeowl]

OK, I think I've come up with a fairly reasonable solution in #267. It's not beautiful, and it's not friendly, but I believe it offers exactly as much type inference as possible without losing polymorphism.