[Agda] reflective access to definitional equality

[Dan Licata]

Here's a somewhat crazy idea:

Given

  contains : Bool -> List Bool -> Bool

I was getting sick of proving equations like

pf : (x y z : Bool) -> Id (contains y (x :: (y :: (z :: [])))) True

(or of writing out a reflection goal and instantiating it with the
current context).  

So, I thought, what if I could write contains in such a way that the
above reduced to True *definitionally*?  

pf x y z = Refl

You can do this if you can call definitional equality as a function in
the language; i.e. something like

areTheyEq : forall {A} (x y : A) -> Maybe (Id a b) 
(areTheyEq e1 e2) |-> Some Refl  if e1 is definitionally equal to e2
(areTheyEq e1 e2) |-> None       otherwise

Now, this is clearly problematic, as it breaks substitutivity of
equality in a bad way:
 x : Nat |- areTheyEq x 0 = None 
but 
 areTheyEq 0 0 = Some Refl)

However, if you (a) CPS the result and then (b) restrict the function so
that the 'yes' branch and the 'no' branch agree whenever the two terms
are actually equal, then I think equality is still substitutive *up to
propositional equality*:

  testDefEq : forall {A : Set} (C : A -> A -> Set)
              (eq     : (x y : _) -> Id x y -> C x y)
              (notnow : (x y : _) -> C x y)
              (safe : (x y : _) (p : Id x y) -> Id (eq x y p) (notnow x y))
              -> (x y : A) 
	      -> C x y

And you can write 'contains' in such a way that the above equation holds
definitionally.  It was actually really easy to implement testDefEq as a
primitive, by a slight modification of the 'primTrustMe' that's already
there.

So, a few questions:

(1) Have people thought about giving programatic access to definitional
equality before?  E.g. if you had a reflective syntax for Agda terms, I
can imagine areTheyEqual being a useful function to have for free.

(2) Does anyone know how to make sense of a type theory where equality
is substitutive only up to propositional equality?  I can imagine there
being an open term for which subject reduction fails, given the above
primitive and the way Agda works right now---there may be spots where
you need to insert some casts.

-Dan