What Ωmega has joined, no one can take apart

Some days ago I became enthusiastic about creating data structures with some pretty strong invariants. What I did not expect were the difficulties actually providing the evidence that the preconditions hold, and that taking apart the the data into pieces without losing the constraints can become a challenge. In fact, when embarking on programming with SingleLabel, a bunch of proof obligations arise.

So the title is actually misleading (sounds cool nevertheless!) and should read "... no one can take apart losslessly". Of course a non-empty SingleLabel can be taken apart by pattern matching! This article is about propositional facts, and their propagation.

The More data constructor is only accessible if the constraint Equal rest {drop l rest} is given. Last time no evidence was needed, because rest was explicitly known, so the drop type function could be evaluated and the equality checked. But when we just want to join a new head with an unknown tail?
This should still be possible in case that a witness is provided, that testifies that the tail does not contain the label occurring in the new head. Simple enough,

join :: Label a -> v -> SingleLabel tail -> Equal {drop a tail} tail -> SingleLabel {a=v; tail}r
join a v t Eq = {a=v; t}s

should do it. Unfortunately I am running against the wall again. The Eq witness is not accepted by Ωmega, on the grounds that no refinement can be established. The debugging session tomorrow promises to become an adventure!

When this problem is fixed, I'll come back and tell you the story of the lossless decomposition (so that calling join with the results gives us the original back).