[Haskell-cafe] Data Types a la Carte - automatic injections (help!)

28 Jul 2008

      I have a question about Data Types a la Carte
(http://www.cs.nott.ac.uk/~wss/Publications/DataTypesALaCarte.pdf) and
more generally hacking smart coproduct injections into Haskell (all
extensions are fair game).
...
{-# LANGUAGE MultiParamTypeClasses,TypeOperators,UndecidableInstances,IncoherentInstances,FlexibleInstances,FlexibleContexts #-}
Here are the definitions from Wouter's paper, which cleverly manage
the instances of (:<:)
...
data (f :+: g) a = Inl (f a) | Inr (g a)
infixr 6 :+:
...
instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap f (Inl x) = Inl (fmap f x)
  fmap f (Inr x) = Inr (fmap f x)
...
class (Functor sub, Functor sup) => sub :<: sup where
  inj :: sub a -> sup a
...
instance Functor f => (:<:) f f where
  inj = id
...
instance (Functor f, Functor g) => (:<:) f (f :+: g) where
  inj = Inl
...
instance (Functor f, Functor g, Functor h, (f :<: g)) => (:<:) f (h :+: g) where
  inj = Inr . inj
Now in my case, I want to be able to inject an arbitrary coproduct
into a larger one, assuming the components are in the same order, so
it is a subsequence of the larger sum, for example:
...
coprodInject1 :: (Functor f, Functor g, Functor h, Functor i) => (f :+: g :+: h) a -> (f :+: g :+: h :+: i) a
coprodInject1 = inj
...
coprodInject2 :: (Functor f, Functor g, Functor h, Functor i) => (f :+: g :+: i) a -> (f :+: g :+: h :+: i) a
coprodInject2 = inj
...
instance (Functor f, Functor g, Functor h, (g :<: h)) => (:<:) (f :+: g) (f :+: h) where
  inj (Inl x) = Inl x
  inj (Inr x) = Inr (inj x)
The above works fine, and maybe I could manipulate my code to only
have injections
of those forms, but I want this next one to work too:
...
coprodInject3 :: (Functor f, Functor g, Functor h, Functor i) => (f :+: g :+: i :+: j) a -> (f :+: g :+: h :+: i :+: j) a
coprodInject3 = inj
It fails because after "passing up" the h in the search, it can either
use the reflexivity rule or decompose the sum on (i :+: j).  The full
error is:

    Overlapping instances for (i :+: j) :<: (i :+: j)
      arising from a use of `inj'
      ...
    Matching instances:
      instance [incoherent] (Functor f) => f :<: f
        -- Defined at ...
      instance [incoherent] (Functor f, Functor g, Functor h, g :<: h) =>
                            (f :+: g) :<: (f :+: h)
        -- Defined at ...
    In the expression: inj
    In the definition of `coprodInject3': coprodInject3 = inj

What confuses me is that IncoherentInstances is on, but it is still
rejected by GHC 6.8.3 seemingly for being incoherent.  I haven't tried
it with any other version.  Am I missing something?  Any suggestions
or pointers?

[Haskell-cafe] Data Types a la Carte - automatic injections (help!)

Kenn Knowles