Lift a parser working on a subset of the tokens

[gallais]

It would be nice to have:

reLex : (check : q -> Maybe p) ->  ∀[ Parser P v ] ->  ∀[ Parser Q v ]

where P and Q are essentially the same parameters except that P has p as the token type while Q has q, which is larger.

My current use case: I want the user to provide a parser munching characters but I'd like to use it in a context where a lexer has been run and some special characters have been recognised as special. So I have:

data TOK = A | B | C Char

and I'd like reLex to run a modified view that takes check into account so that the client's anyTok only succeeds if the TOK has the shape C c.