Polyvariadic functions with polymorphic result value

Question

I'm trying to implement a Pascal-style write procedure in Haskell as a polyvariadic function. Here is a simplified version with monomorphic result type (IO in that case) that works fine:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main where

import Control.Monad.IO.Class
import Control.Monad.Trans.Reader
import System.IO


class WriteParams a where
    writeParams :: IO () -> a

instance (a ~ ()) => WriteParams (IO a) where
    writeParams = id

instance (Show a, WriteParams r) => WriteParams (a -> r) where
    writeParams m a = writeParams (m >> putStr (show a ++ " "))

write :: WriteParams params => params
write = writeParams (return ())

test :: IO ()
test = do
    write 123
    write ('a', 'z') True

When changing the result type to a polymorphic type, however, to use that function in different monads that have a MonadIO instance, I'm running into overlapping or undecidable instances. Specifically, that a ~ () trick from the previous version doesn't work anymore. The best approach is the following which requires a lot of type annotations, though:

class WriteParams' m a where
    writeParams' :: m () -> a

instance (MonadIO m, m ~ m') => WriteParams' m (m' ()) where
    writeParams' m = m

instance (MonadIO m, Show a, WriteParams' m r) => WriteParams' m (a -> r) where
    writeParams' m a = writeParams' (m >> liftIO (putStr $ show a ++ " "))

write' :: forall m params . (MonadIO m, WriteParams' m params) => params
write' = writeParams' (return () :: m ())

test' :: IO ()
test' = do
    write' 123 () :: IO ()
    flip runReaderT () $ do
        write' 45 ('a', 'z') :: ReaderT () IO ()
        write' True

Is there anyway to make this example work without having to add type annotations here and there and still keep the result type polymorphic?

Answer 1

The two instances overlap, because their indices unify: m' () ~ (a -> r) with m' ~ (->) a and () ~ r.

To pick the first instance whenever m' is not a function type, you can add an OVERLAPPING pragma. (Read more about it in the GHC user guide)

-- We must put the equality (a ~ ()) to the left to make this
-- strictly less specific than (a -> r)
instance (MonadIO m, a ~ ()) => WriteParams (m a) where
    writeParams = liftIO 

instance {-# OVERLAPPING #-} (Show a, WriteParams r) => WriteParams (a -> r) where
    writeParams m a = writeParams (m >> putStr (show a ++ " "))

---

However, the overlapping instance makes it inconvenient to use write in a context where the monad is a parameter m (try generalizing the signature of test).

There is a way to avoid overlapping instances by using closed type families, to define a type-level boolean that's true if and only if a given type is a function type, so that instances can match on it. See below.

It arguably just looks like more code and more complexity, but, on top of the added expressiveness (we can have a generalized test with a MonadIO constraint), I think this style makes the logic of the instances clearer in the end by isolating the pattern-matching on types.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

import Control.Monad.IO.Class
import Control.Monad.Trans.Reader
import System.IO


class WriteParams a where
    writeParams :: IO () -> a

instance WriteParamsIf a (IsFun a) => WriteParams a where
    writeParams = writeParamsIf

type family IsFun a :: Bool where
  IsFun (m c) = IsFun1 m
  IsFun a = 'False

type family IsFun1 (f :: * -> *) :: Bool where
  IsFun1 ((->) b) = 'True
  IsFun1 f = 'False

class (isFun ~ IsFun a) => WriteParamsIf a isFun where
  writeParamsIf :: IO () -> a

instance (Show a, WriteParams r) => WriteParamsIf (a -> r) 'True where
  writeParamsIf m a = writeParams (m >> putStr (show a ++ " "))

instance ('False ~ IsFun (m a), MonadIO m, a ~ ()) => WriteParamsIf (m a) 'False where
  writeParamsIf = liftIO

write :: WriteParams params => params
write = writeParams (return ())

test :: (MonadIO m, IsFun1 m ~ 'False) => m ()
test = do
    write 123
    write ('a', 'z') True

main = test  -- for ghc to compile it

---

Some words on UndecidableInstances

Undecidable instances are an orthogonal feature to overlapping instances, and in fact I think they're much less controversial. Whereas badly using OVERLAPPING may cause incoherence (constraints being solved differently in different contexts), badly using UndecidableInstances may at worst send the compiler in a loop (in practice GHC terminates with an error message once some threshold is reached), which is still bad but when it does manage to resolve instances it is still guaranteed that the solution is unique.

UndecidableInstances lifts limitations that made sense a long time ago, but are now too restrictive to work with the modern extensions to type classes.

In practice, most common type classes and instances defined with UndecidableInstances, including the one above, still guarantee that their resolution will terminate. In fact, there is an active proposal for a new instance termination checker. (I don't know yet whether it handles this case here.)