Issue435.agda

module Issue435 where

data Bool : Set where
  true false : Bool

record Unit : Set where

postulate
  Dh : ({ x : Bool } → Bool) → Set
  Di : ({{x : Bool}} → Bool) → Set

noth : Set
noth = Dh (\ { {true}  → false ; {false} → true})

noti : Set
noti = Di (\ { {{true}}  → false ; {{false}} → true})

-- Testing absurd patterns

data ⊥ : Set where

data T : Set where
  expl : (⊥ → ⊥) → T
  impl : ({_ : ⊥} → ⊥) → T
  inst : ({{_ : ⊥}} → ⊥) → T

explicit : T
explicit = expl (λ ())

implicit : T
implicit = impl (λ {})

instance : T
instance = inst (λ {{ }})

explicit-match : T
explicit-match = expl (λ { () })

implicit-match : T
implicit-match = impl (λ { {} })

implicit-match′ : T
implicit-match′ = impl (λ { { () } })

instance-match : T
instance-match = inst (λ { {{}} })

instance-match′ : T
instance-match′ = inst (λ { {{ () }} })