Agda-2.3.2.2: test/succeed/Issue558c.agda

-- {-# OPTIONS --verbose tc.proj.like:100 #-}

-- Apparently, there can be projection like functions working on arguments of type Axiom.
module Issue558c where

data ⊤ : Set where
  tt : ⊤

data V : Set where
  aV : ⊤ → V

postulate D : ⊤ → Set
          zero : D tt
          suc : ∀ {t} → D t → V

test : {{v : V}} → ⊤
test {{v}} = tt

module test {t : ⊤} {d : D t} where
  inst : V
  inst = aV tt

  someT : ⊤
  someT = test