Evaluation of an AST (as a GADT) with arrows as atomic values

Question

The following program type-checks and compiles:

import Control.Arrow

data Ns = Na | Nb | Nc | Nd deriving Show

data Net a where
    Uni :: a -> Net a
    Serial :: Net a -> Net a -> Net a
    Branch :: Show a => Net a -> Net (Net a, Net a)

deriving instance Show a => Show (Net a)

eval :: (Arrow a) => Net c -> a b (Net c)
eval (Uni m) = arr (const (Uni m))
eval (Serial m n) = eval m >>> eval n
--eval (Branch m) = eval m &&& eval m

example = Serial (Serial (Uni Na) (Uni Nb)) (Serial (Uni Nc) (Uni Nd))

main = do
    putStrLn $ show (app (eval example, Na))

However, when I try to add a case for eval (Branch m), type checking bombs out. Something of type

Arrow a => a b (Net d)

is expected, but of course the way I have it is

Arrow a => a b (c',c'')

Does anyone have a suggestion for how to write eval (Branch m)?

EDIT I

In response to @sabauma comment, I think the type signature for eval will have to change, but I'm not sure what it should be.

EDIT II

Here's an example of what should happen:

branch = Branch example
app (eval branch, Na)

should give,

Uni (Uni Na,Uni Na)

This is what @sabauma 's proposal does.

Answer 1

One possibility is

eval :: (Arrow a) => Net c -> a b (Net c)
eval (Uni m)      = arr (const (Uni m))
eval (Serial m n) = eval m >>> eval n
eval (Branch m)   = (eval m &&& eval m) >>> arr Uni

I don't know if this has the desired behaviour, but it typechecks and is not the trivial solution. This lets you get away without changing the type signature.

Answer 2

My guess would be to redifine Branch to take two arguments (since branching somehow implies that for me):

data Net a where
  Uni :: a -> Net a
  Serial :: Net a -> Net a -> Net a
  Branch :: Show a => Net a -> Net a -> Net (Net a, Net a)

leading to

eval :: (Arrow a) => Net c -> a b (Net c)
eval (Uni m) = arr (const $ Uni m)
eval (Serial m n) = eval m >>> eval n
eval (Branch l r) = (eval l) &&& (eval r) >>> arr (uncurry Branch)

But I can't say if this change makes sense for you. You probably should give some explanation how your type would be used.

Answer 3

Although I'm not entirely sure on the purpose of your code, and this might not be what you're after, the following typechecks:

eval :: Arrow a => Net c -> a b (Net c)
eval (Uni m)      = arr (const (Uni m)) 
eval (Serial m n) = eval m >>> eval n
eval (Branch m)   = arr (const (Branch m)) 

of course, arr . const trivially works for eval, but now I'm almost positive that's not what you wanted.