[Agda] Trust me regarding Dan Licata's trick

[Nils Anders Danielsson]

On 2013-06-06 22:57, Alan Jeffrey wrote:
> In the JS back end, _==_ is recognized as a singleton type, so any
> expressions of this type are eta-converted at compile time to refl,
> including uses of primTrustMe.

The Epic backend contains similar functionality. From the release notes
for 2.3.0:

   "An important example of an inferable type is the usual propositional
   equality type (_≡_). Any function returning a propositional equality
   can simply return the reflexivity constructor directly without
   computing anything."

-- 
/NAD