Known pattern match in agda

Question

Roughly, I have

check : UExpr -> Maybe Expr

And I have a test term

testTerm : UExpr

Which I hope will check successfully, after which I want to extract the resulting Expr and manipulate it further. Basically

realTerm : Expr
just realTerm = check testTerm

Such that this definition would fail to typecheck if check testTerm turned out to be nothing. Is this possible?

Answer 1

The usual deal is to write something like

Just : {X : Set} -> Maybe X -> Set
Just (just x) = One -- or whatever you call the fieldless record type
Just nothing = Zero

justify : {X : Set}(m : Maybe X){p : Just m} -> X
justify (just x) = x
justify nothing {()}

If m computes to a success, the type of p is One and the value is inferred.

Answer 2

Well I found one way to do it, which is sortof bizarre and magical.

testTerm-checks : Σ Expr (\e -> check testTerm ≡ just e)
testTerm-checks = _ , refl

realTerm : Expr
realTerm = proj₁ testTerm-checks

This gives me the heebie jeebies, but not necessarily in a bad way. Still interested in other ways to do it.