Handling ambiguous types in composable free DSLs

Question

I'm building a couple of DSLs which should be composable based on 'free monads' and 'datatypes a la carte', using the free and compdata packages (similar in spirit to Combining Free types).

Whilst this works for some simple DSLs, I'm stuck on one which has a type parameter, in the case of a constructor/command which doesn't depend on this type parameter, causing an ambiguous type parameter error from GHC.

To clarify, here's some code:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}

module DSL where

import Data.Comp
import Control.Monad.Free

type Index = Int

data DSL a next = Read Index (a -> next)
                | Write a (Index -> next)
                | GetLastIndex (Index -> next)
    deriving (Functor)

read :: (Functor f, DSL a :<: f, MonadFree f m) => Index -> m a
read idx = liftF (inj (Read idx id))

write :: (Functor f, DSL a :<: f, MonadFree f m) => a -> m Index
write a = liftF (inj (Write a id))

-- This works
getLastIndex' :: MonadFree (DSL a) m => m Index
getLastIndex' = liftF (GetLastIndex id)

-- This doesn't:
--
--     Could not deduce (Data.Comp.Ops.Subsume
--                         (compdata-0.10:Data.Comp.SubsumeCommon.ComprEmb
--                            (Data.Comp.Ops.Elem (DSL a0) f))
--                         (DSL a0)
--                         f)
--     from the context (Functor f, DSL a :<: f, MonadFree f m)
--       bound by the type signature for
--                  getLastIndex :: (Functor f, DSL a :<: f, MonadFree f m) => m Index
--       at simple.hs:30:17-66
--     The type variable ‘a0’ is ambiguous
--     In the ambiguity check for the type signature for ‘getLastIndex’:
--       getLastIndex :: forall (m :: * -> *) (f :: * -> *) a.
--                       (Functor f, DSL a :<: f, MonadFree f m) =>
--                       m Index
--     To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
--     In the type signature for ‘getLastIndex’:
--       getLastIndex :: (Functor f, DSL a :<: f, MonadFree f m) => m Index

getLastIndex :: (Functor f, DSL a :<: f, MonadFree f m) => m Index
-- getLastIndex = liftF (inj (GetLastIndex id))
getLastIndex = _

Trying to get this to work with enabling the AllowAmbiguousTypes extension as hinted by GHC didn't get me any further. I tried adding some forall a-style things in the type signature, to no avail.

Is there any way to get this pattern to work?

András Kovács András Kovács · Accepted Answer · 2015-05-05T21:12:44

This is a relatively well-known limitation of open sums "à la Carte".

In short, if we have an f functor that itself has one or more inner type indices, then type inference suffers significantly for open sums containing that functor.

Illustrating the reasons, suppose we have an open sum that contains a DSL () and a DSL Int. GHC must pick an instance for one of them, but it's impossible with getLastIndex, because the a parameter isn't mentioned in the arguments or the return type. GHC has essentially no information about a from the context.

This can be remedied in a somewhat clumsy way using Data.Proxy:

import Data.Proxy

getLastIndex ::
  forall a f m.
  (Functor f, DSL a :<: f, MonadFree f m)
  => Proxy a -> m Index
getLastIndex _ = liftF (inj (GetLastIndex id :: DSL a Index))

Alternatively, we can recover nice type inference and unambiguity if we require that there is only a single DSL in the open sum. However, this involves rewriting the type-level lookup code for :<: for functors like DSL (those that have an inner type index). We can't really do this with compdata as it is, because it doesn't export the relevant type-level machinery.

I wrote a minimal example for what the implementation of the above looks like for your case. I don't paste it here because it's a bit long and unedifying. Note that the choice of the inner index becomes completely determined by the functor's constructor and the open sum. This also repairs type inference for other cases; for example with the old code we have to type-annotate every use of Write x f if x is a number literal or any polymorphic value, while in the new code its gets inferred.

Also, note that the example implementation is only for functors with a single inner index! If we'd like to have a DSL a b next, then we would have to write new code for that case too, or use DSL '(a, b) next instead.

Handling ambiguous types in composable free DSLs

1 Answers