Do we need to put symbol between each argument in Agda's notation?

December 10, 2022

As I described in the title, the supposed code should be like this:

data Mode : Set where
  ⇛ : Mode
  ⇚ : Mode

infix  4  _⊢_

data _⊢_ : Context → Term → Mode → Type → Set where
  ⊢-int : ∀ {Γ n}
    → Γ ⊢ (lit n) ⇛ Int

And it gave me the error

Mode → Type → Set should be a sort, but it isn't
when checking that the inferred type of an application
  Mode → Type → Set
matches the expected type
  _30

I sort of know what the type is. To deal with it, I may need to put some non-meaningful symbols between, e.g.

data _⊢_._._ where

which is not good-looking and I’m tired of writing those. Just want to know any solutions for this situation?

>Solution :

You can hardcode the mode right into the data type declaration and create two separate data types:

data _⊢_⇛_ : Context → Term → Type → Set where
  ⊢-int : ∀ {Γ n}
    → Γ ⊢ lit n ⇛ Int

data _⊢_⇚_ : Context → Term → Type → Set where

Note that Agda is able to recognize that ⇛ in _⊢_⇛_ is different to the one from Mode, so there’s no ambiguity (unless you also add _⊢_, at which point things become ambiguous).

Alternatively, you can make it

data Mode : Set where
  _⇛_ : Term → Type → Mode
  _⇚_ : Term → Type → Mode

infix 4  _⊢_
infix 5 _⇛_ _⇚_

data _⊢_ : Context → Mode → Set where
  ⊢-int : ∀ {Γ n}
    → Γ ⊢ lit n ⇛ Int