[Haskell-cafe] Escaping phantom type

[Miguel Mitrofanov]

Hi cafe!

Assume I have some function

foo :: A x -> B x

Now, the type B is somewhat complicated. It consists of several parts. So, if we call foo twice, like

let b1 = foo a
    b2 = foo a

then it's possible that we'd use some parts of b1 and b2 together, mistakenly assuming they are from the same B, not from different ones.

I want to exclude this possibility. So I introduce a phantom type, and the signature becomes this:

foo :: A x -> exists y. B x y

(of course that's not a legitimate Haskell, in reality I'll use some GADT)

Now b1 and b2 would have different types, and we can't mix them up by mistake. So far so good.

But let's assume that we want to use "foo" recursively. Without the safety precautions it would be easy:

generateA :: B x -> OtherArgs -> A x
...
b = foo (generateA b otherArgs)

Unfortunately, we can't do the same thing with this safety net in place. If we do

generateA :: B x y -> OtherArgs -> A x

where x doesn't depend on y, then generateA would loose the phantom type, so

let b = foo (generateA b otherArgs) in b

and

let b1 = foo (generateA b1 otherArgs)
    b = foo (generateA b1 otherArgs) -- sic!
in b

would be indistinguishable. And that is definitely not what we want. In reality, we want x to depend on y. Unfortunately, there are lots of possibilities regarding the way x would depend on y. I know for sure that there would be many different "generateA" functions, and I don't want to encode them all in types.

I've come up with one solution:

foo :: (forall y. exists x. ((B x y -> A x), (B x y -> z))) -> z

This would work, as in the end I would be interested not in B, but in something that would have nothing to do with this phantom types. But that requires explicit CPS transformation, which makes the code difficult to read.

Is there some way to simplify things? To make them easier to use?