Add optional runtime checks for preconditions

[jespercockx]

Functions in Agda2Hs can use @0 arguments to express preconditions, but these arguments are erased in the translation to Haskell. For functions that are only used "internally" this is not a problem, but for functions that are meant to be used from Haskell code it would be nice to provide an option to generate run-time checks for these properties. Obviously this would need to be restricted to decidable properties (I'm thinking of IsTrue and equalities on types with decidable equality).

[jespercockx]

One way to support this with the current architecture would be to add the assert operator from Haskell to the agda2hs prelude with the following Agda definition:

assert : (b : Bool) → (@0 {{IsTrue b}} → a) → a
assert True  x = x
assert False x = oops
  where postulate oops : _

Even better would be if we could do this for an arbitrary decidable type rather than just booleans:

Reflects : (P : Set ℓ) → Bool → Set ℓ
Reflects P True  = P
Reflects P False = P → ⊥

Dec : Set ℓ → Set ℓ
Dec P = ∃ Bool (Reflects P)

assert : Dec b → (@0 {{b}} → a) → a
assert [ True  ] x = x
assert [ False ] x = oops
  where postulate oops : _

[omelkonian]

Even better, gather all decidable types in a typeclass so users can simply write the property and have instance inference do the work for you?

[jespercockx]

Well yes that would be nice, but I am not sure what type signature such a function should have: to compile to assert in Haskell it needs to have an explicit argument of type Bool (or a type that erases to it such as Dec b), but for instance search to kick in you need to have an instance argument on the Agda side. It doesn't make sense to have a typeclass of decidable types on the Haskell side since this will mostly be used for propositions that don't have a Haskell counterpart.

The best I can come up with is to have a typeclass of decidable types on the Agda side and then use the it function as an argument to the assert function I defined above. We can then have a tiny bit of special handling for the it function so agda2hs compiles it to the actual boolean check that's been found by Agda's instance search.

[jespercockx]

Ah we could make assert itself into a macro that takes a type and runs instance search to find a proof of decidability. Then we could write something like assert (x ≡ 42) ... in the Agda code and have it be compiled to the corresponding boolean assertion in Haskell.