gistfile1.txt

module bugreport where

open import Data.Nat 
open import Data.Bool hiding (_≟_)
open import Relation.Nullary

⸤_⸥ : {A : Set} → Dec A → Bool
⸤ yes _ ⸥ = true 
⸤ no  _ ⸥ = false 

record State : Set where
  field var₁ : Bool
  field var₂ : ℕ

open State ⦃ ... ⦄

postulate Program : Set → Set 
postulate guard : ∀{S : Set} → (S → Bool) → Program S

test₃ : Program State
test₃ = guard (λ σ → var₁) -- works

test₂ : Program State
test₂ = guard {State} (λ σ → ⸤ var₂ ≟ 0 ⸥) -- works

test₁ : Program State
test₁ = guard (λ σ → ⸤ var₂ ≟ 0 ⸥) -- doesn't work, used to work in agda 2.4