Minimal example:
open import Haskell.Prelude
test : ⊤
test = local
where postulate local : ⊤
{-# COMPILE AGDA2HS test #-}
Error message:
src/Agda2Hs/Compile/Function.hs:163:5-25: Non-exhaustive patterns in Function {..}
Should: compile the local definition as a postulate (i.e. a run-time error).