[#265] Make SuperComposition less brittle

CHANGES.md

@@ -1,6 +1,12 @@
 Unreleased
 =====
 
+* [#265](https://github.com/serokell/universum/issues/265):
+  Make `SuperComposition` inference less brittle, and give it four type
+  parameters. Applications may require more or different type annotations in
+  some cases and fewer in others. Details of the constraint resolution process
+  should no longer affect which applications successfully typecheck.
+
 * [#252](https://github.com/serokell/universum/pull/252):
   Remove `Option` re-export. Use `Maybe` instead.
 

README.md

@@ -272,9 +272,9 @@ Finally, we can move to part describing the new cool features we bring with `uni
 * Variadic composition operator `(...)`. So you can write:
 
   ```haskell
-  ghci> (show ... (+)) 1 2
+  ghci> (show ... (+)) (1 :: Int) 2
   "3"
-  ghci> show ... 5
+  ghci> show ... 5 :: String
   "5"
   ghci> (null ... zip5) [1] [2] [3] [] [5]
   True

benchmark/Main.hs

@@ -112,9 +112,9 @@ bgroupSuperComposition = bgroup "(...)"
  where
   super10 :: [()] -> Bool
   super10 = null
-        ... ((: []) ... Unsafe.head ... pure ... Unsafe.head
+        ... (: []) ... Unsafe.head ... (pure :: () -> [()]) ... Unsafe.head
         ... (: [(), (), (), ()]) ... Unsafe.head ... (: []) ... Unsafe.head
-        ... (: [()]) ... Unsafe.head ... (: [(), ()]) ... Unsafe.head :: [()] -> [()])
+        ... (: [()]) ... Unsafe.head ... (: [(), ()]) ... Unsafe.head
 
   norm10 = null
          . (: []) . Unsafe.head . pure . Unsafe.head

src/Universum/VarArg.hs

@@ -1,16 +1,24 @@
+{-# LANGUAGE AllowAmbiguousTypes    #-}
+{-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE FlexibleContexts       #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MultiParamTypeClasses  #-}
 {-# LANGUAGE Safe                   #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
 {-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeOperators          #-}
 {-# LANGUAGE UndecidableInstances   #-}
 
 -- | Provides operator of variable-arguments function composition.
 
 module Universum.VarArg
        ( SuperComposition(..)
        ) where
+import Data.Type.Bool (Not, type (||))
+import Data.Type.Equality (type (==))
+import Prelude (Bool (..))
 
 -- $setup
 -- >>> import Universum.Base ((+))
@@ -19,17 +27,25 @@ module Universum.VarArg
 -- >>> import Data.List (zip5)
 
 -- | This type class allows to implement variadic composition operator.
-class SuperComposition a b c | a b -> c where
-    -- | Allows to apply function to result of another function with multiple
+class SuperComposition x y b r | x y b -> r where
+    -- | Applies a function to the result of another function with multiple
     -- arguments.
     --
-    -- >>> (show ... (+)) 1 2
+    -- >>> (show ... (+)) (1 :: Int) 2
     -- "3"
-    -- >>> show ... 5
+    -- >>> (show ... (+)) 1 2 :: String
+    -- "3"
+    -- >>> show ... (5 :: Int)
+    -- "5"
+    -- >>> show ... 5 :: String
     -- "5"
     -- >>> (null ... zip5) [1] [2] [3] [] [5]
     -- True
     --
+    -- Note that the type checker needs to have enough information on hand to deduce
+    -- the appropriate arity for the second argument, which explains the need for explicit
+    -- types in some examples above.
+    --
     -- Inspired by <http://stackoverflow.com/questions/9656797/variadic-compose-function>.
     --
     -- ==== Performance
@@ -45,16 +61,42 @@ class SuperComposition a b c | a b -> c where
     -- disappear due to very general inferred type. However, functions without type
     -- specification but with applied @INLINE@ pragma are fast again.
     --
-    (...) :: a -> b -> c
+    (...) :: (x -> y) -> b -> r
 
 infixl 8 ...
 
-instance {-# INCOHERENT #-} (a ~ c, r ~ b) =>
-         SuperComposition (a -> b) c r where
-    f ... g = f g
-    {-# INLINE (...) #-}
+-- The implementation is a bit tricky to get right. See #265 for how things can go wrong.
+-- The basic idea is that we can commit to using the base case if we know we've reached
+-- a result of the right type *or* we know that we don't have any arrows left. Similarly,
+-- we can commit to using the recursive case if we know we don't yet have a result of the
+-- right type *or* we know that we have more arrows we can use.
+
+type family IsArrow b where
+  IsArrow (_ -> _) = 'True
+  IsArrow _ = 'False
+
+-- | Can we use the base case?
+type PlainApplication y b r = y == r || Not (IsArrow b)
+
+-- | Can we use the recursive case?
+type Composing y b r = Not (y == r) || IsArrow b
+
+class SuperComposition' (plainApplication :: Bool) (composing :: Bool) x y b r | x y b -> r where
+    comp :: (x -> y) -> b -> r
+
+instance (x ~ b, y ~ r) =>
+         SuperComposition' 'True composing x y b r where
+    comp f = f
+    {-# INLINE comp #-}
+
+instance {-# INCOHERENT #-} (b ~ (b1 -> b'), r ~ (b1 -> r'), SuperComposition x y b' r') =>
+         SuperComposition' plainApplication 'True x y b r where
+    (f `comp` g) c = f ... g c
+    {-# INLINE comp #-}
 
-instance {-# INCOHERENT #-} (SuperComposition (a -> b) d r1, r ~ (c -> r1)) =>
-         SuperComposition (a -> b) (c -> d) r where
-    (f ... g) c = f ... g c
+instance ( pa ~ PlainApplication y b r
+         , co ~ Composing y b r
+         , SuperComposition' pa co x y b r) =>
+         SuperComposition x y b r where
+    (...) = comp @pa @co
     {-# INLINE (...) #-}