Here's a piece of code that generates faulty Haskell code:
module Test where
open import Agda.Builtin.IO
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
record R : Set where
field x : Nat
variable r : R
data D : R → Nat → Set where
c : let open R r in D r x
f : R → Nat
f r = fst g
where
g : Σ Nat (D r)
g = (_ , c)
postulate print : Nat → IO ⊤
{-# COMPILE GHC print = print #-}
main = print (f (record { x = 3 }))
When compiled (with agda --compile, Agda version 2.6.4) and ran, it produces the following error message:
Test: Agda: unreachable code reached.
CallStack (from HasCallStack):
error, called at ./MAlonzo/RTE.hs:44:23 in main:MAlonzo.RTE
Making this fail is quite delicate. Binding r without the variable block, replacing the let open with anything else or replacing the _ in g make the code compile correctly. The print part at the bottom doesn't really matter, I just needed something to force the application of f & make compilation easy.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4