Type errors with Existential types in Haskell

Question

I am struggling with existential types in my program. I think I'm trying to do something very reasonable however I cannot get past the typechecker :(

I have a datatype that sort of mimics a Monad

data M o = R o | forall o1. B (o1 -> M o) (M o1)

Now I create a Context for it, similar to that described in Haskell Wiki article on Zipper, however I use a function instead of a data structure for simplicity -

type C o1 o2 = M o1 -> M o2

Now when I try to write a function that splits a data value into its context and subvalue, the typechecker complains -

ctx :: M o -> (M o1 -> M o, M o1)
ctx (B f m) = (B f, m) -- Doesn't typecheck

Error is -

Couldn't match type `o2' with `o1'
  `o2' is a rigid type variable bound by
       a pattern with constructor
         B :: forall o o1. (o1 -> M o) -> M o1 -> M o,
       in an equation for `ctx'
       at delme1.hs:6:6
  `o1' is a rigid type variable bound by
       the type signature for ctx :: M o -> (M o1 -> M o, M o1)
       at delme1.hs:6:1
Expected type: M o2
  Actual type: M o1
In the expression: m
In the expression: (B f, m)

However, I can work around it like so -

ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK

Why does this second definition typecheck but not the first one?

Also, if I try to convert ctx to a complete function by checking for R, I again get a typecheck error -

ctx (R o) = (id, R o) -- Doesn't typecheck

Error -

Couldn't match type `o' with `o1'
  `o' is a rigid type variable bound by
      the type signature for ctx :: M o -> (M o1 -> M o, M o1)
      at delme1.hs:7:1
  `o1' is a rigid type variable bound by
       the type signature for ctx :: M o -> (M o1 -> M o, M o1)
       at delme1.hs:7:1
In the first argument of `R', namely `o'
In the expression: R o
In the expression: (id, R o)

How can I work around this error?

Any help is appreciated!

Answer 1

Let's look at the failing cases first. Both of these fail for the same reason, which is clearer once you add in the implicit forall in the type signature:

ctx :: forall o o1. M o -> (M o1 -> M o, M o1)

i.e. your function must not only work for a some o1, but for any o1.

1. In your first case,

   ctx (B f m) = (B f, m)
   

   we know that f :: (o2 -> M o) and m :: M o2, for some type o2, but we have to be able to offer any type o1, so we can't assume that o1 ~ o2.

2. In the second case,

   ctx (R o) = (id, R o)
   

   Here, we know that o :: o, but again, the function has to be defined for any o1, so we can't assume that o ~ o1.

Your workaround only seems to work because it's calling itself, similar to an inductive proof. But without a base case, it's just circular reasoning, and you cannot write the base case for this function, because there is no way to construct an M o1 from an M o for any combination of o and o1 without using a bottom value.

What you'll probably need to do, is to define another existential type for the context, instead of using just a tuple. Not sure if it'll work for your needs, but this compiles¹, at least:

data Ctx o = forall o1. Ctx (M o1 -> M o) (M o1)

ctx :: M o -> Ctx o
ctx (B f m) = case ctx m of Ctx c m' -> Ctx (B f . c) m'
ctx (R o)   = Ctx id (R o) 

_{¹ Try using a let instead of case for a funny GHC error :)}