Some experiments with --prop and instance arguments

Playground.agda

{-# OPTIONS --safe --prop --overlapping-instances #-} 

module Playground where

open import Data.Nat
open import Data.List
open import Data.Bool
open import Data.Empty
open import Data.Unit

it : {A : Set} ⦃ _ : A ⦄ → A
it ⦃ x ⦄ = x

it′ : {A : Prop} ⦃ _ : A ⦄ → A
it′ ⦃ x ⦄ = x

infix 4 _∈₁_
data _∈₁_ {A : Set} (x : A) : List A → Set where
  instance
    here  : ∀ {xs} → x ∈₁ x ∷ xs
    there : ∀ {y xs} ⦃ _ : x ∈₁ xs ⦄ → x ∈₁ y ∷ xs

data ∥_∥ (A : Set) : Prop where
  ∣_∣ : (x : A) → ∥ A ∥

instance
  pf : {A : Set} {x : A} → ∥ A ∥
  pf {A} {x} = ∣ x ∣

module Membership {A : Set} (_==_ : A → A → Bool) where
  _∈₂_ : A → List A → Prop
  a ∈₂ []     = ∥ ⊥ ∥
  a ∈₂ (x ∷ xs) with a == x
  ... | true  = ∥ ⊤ ∥
  ... | false = a ∈₂ xs
  infix 4 _∈₂_
open Membership _≡ᵇ_

_ : 1 ∈₂ (2 ∷ 1 ∷ [])
_ = it′

_ : ∥ 1 ∈₁ (2 ∷ 1 ∷ []) ∥
_ = ∣ it ∣ -- this requires --overlapping-instances 

_ : ∥ 1 ∈₁ 2 ∷ 1 ∷ [] ∥
_ = it′ ⦃ ∣ it ∣ ⦄

_ : ∥ 1 ∈₁ 2 ∷ 1 ∷ [] ∥
_ = it′ -- I hope this could work