-- {-# 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
  instance
    inst : V
    inst = aV tt

  someT : ⊤
  someT = test
