The `assert` function should not be used in erased positions

[jespercockx]

I was experimenting a bit with the assert function that I added in #388 for enforcing dynamic contracts. In particular, I wanted to implement the following function:

postcondition : (@0 P : b → Set) {{post : ∀ {y} → Dec (P y)}}
         → (f : a → b)
         → (x : a) → ∃ b P

Now the way I expected to have to implement it is as follows:

postcondition post f x = assert (post (f x)) (f x ⟨ it ⟩)

(where it : {{a}} → a is defined as usual by it {{x}} = x). This leads to the expected Haskell code:

postcondition :: (b -> Bool) -> (a -> b) -> a -> b
postcondition post f x = assert (post (f x)) (f x)

However I realized I could also put the assert in the erased portion of the result:

postcondition post f x = f x ⟨ assert (post (f x)) it ⟩

which leads to Haskell code without any run-time check:

postcondition post f x = f x

Now we could in principle "fix" this by only allowing the assert function to appear in non-erased parts of a program. However this is rather strange because usually things work the other way around.

More generally, the current type of assert is logically inconsistent because you can always simply assert ⊥ to get a proof of anything. This is "fine" in unerased positions since it will lead to a run-time error, but in erased positions this is problematic. Maybe instead of using postulate in the definition of assert it should work more like the definition of error which requires a tactic argument of type ⊥.

[anuyts]

Are you saying that #445 fixes this issue in the sense that it is deemed acceptable that MayThrow e implies ⊥?
I'm not sure if I would agree on that, if this implication can be used in erased positions without the error actually being thrown at runtime.

This seems to say that functions which can throw errors, are also allowed to silently misbehave.

[jespercockx]

MayThrow is a postulate, so there is no way to prove that it is either inhabited or empty. The intention is that it is an abstract type, which can only be produced by calls to catch and only consumed by calls to throw. Intuitively this seems enough to me to ensure that functions that may throw exceptions do not misbehave in other ways, but admittedly I have not done any theoretical work to ensure this is the case (but perhaps such work already exists - in which case I would love to hear about it).

[anuyts]

I'm thinking of something like the following:

postulate
  Output : Set
  Spec : Output -> Set
  Error : Set
  error : Error

record SpecifiedOutput : Set where
  constructor specifiedOutput
  field
    output : Output
    @erased spec : Spec output

liar : MayThrow Error -> Output -> SpecifiedOutput
liar m o = specifiedOutput o (throw m error)

No error will be thrown at runtime, the specification is silently violated.

[anuyts]

This is also not related to the fact that liar bundles up computation and specification. If the computation requires m : MayThrow Error, then in order to talk about it's output, you need m in the specification, allowing you to misbehave:

misbehave : MayThrow Error -> Output -> Output
misbehave m o = o

@erased misbehave-is-wellbehaved : (m : MayThrow Error) (o : Output) -> Spec (misbehave m o)
misbehave-is-wellbehaved m o = throw m error

[jespercockx]

Hmm you are absolutely correct, somehow I had managed to convince myself that having the MayThrow argument around would prevent the issue but of course you can still throw exceptions in erased code to prove anything, and then use catch to discharge the MayThrow requirement (where the catch will not catch anything at runtime since all calls to throw were erased). So what I implemented in #445 is pretty much useless for fixing this issue.

Perhaps an actual solution would be to require an (erased) proof that a is inhabited in the type of throw. Since basically all Haskell types are inhabited (unless EmptyDataDecls is enabled) the impact on usability would hopefully be small.

Anyway, for now let's unlink this issue from #445.

[anuyts]

I think, unless someone manages to extend your modal/quantitative system in order to support non-erasability, that the only/best reliable way to track error throwing on the Agda side is by having a dedicated error monad that compiles to the identity functor.

By introducing a MayThrow type, you're not making it just any monad but specifically a reader monad. But reader monads preserve Σ-types, whereas an error monad Error ⨄ _ does not. In Error ⨄ SpecifiedOutput, either both components succeed or both components fail. I think this is what I'm exploiting above: the runtime component succeeds, while the specification component fails.