DestroyPrefix does not work well with abstract stacks
Clarification and motivation
GHC can't deduce DestroyPrefix (Natural ': s) s
if s
is not concrete (it's just an example, the main point is that this constraints holds for each s
). So we can't easily use functions that have DestroyPrefix
constraint to full extent. And if write a general-purpose function that we want to be reusable we can't specify concrete s
. A workaround is to add DestroyPrefix (Natural ': s)
and other required tautological constraints and propagate them as far as needed. That's what I do in !167 (merged), but that's pretty much inconvenient.
Acceptance criteria
It should be possible to pass things like Var Natural -> IndigoM (Natural ': s) (Natural ': s) ()
to ifJust
(body in Just
case) without explicitly requiring DestroyPrefix (Natural ': s) s
constraint. ifJust
requires DestroyPrefix (Natural ': s) s
and currently it is not deduced without our help.
I don't know whether it is possible to modify DestroyPrefix
to make it work this way, in the worst case we may have to do something different from DestroyPrefix
.