Why does the Agda typechecker crash on this program

Question

Consider the following (invalid) Agda code

data Example : Example ex → Set where
  ex : Example ex

This type can be writtien validly in Agda in the following way, making use of Agda's feature of allowing values to be given a type earlier and a definition later

exampleex : Set
ex' : exampleex

data Example : exampleex → Set where
  ex : Example ex'

exampleex = Example ex'
ex' = ex

This all compiles, and Agda correctly knows that ex : Example ex

However, trying to define a function out of Example with pattern matching causes the compiler to crash

test : (e : Example ex) → Example e → ℕ
test ex x = 0

When I add this function to the file, and run "agda main.agda", agda says "Checking main" but never finishes running. Isn't type checking in Agda supposed to be deciable?

Also, is there any way to fix this and make the test function possible to define?

Amends

I’m genuinely surprised you were able to successfully define Example this way, although I’m not an Agda expert. I would not at all be surprised if the bug here was that Agda let you define this strangely-recursive type in the first place – Angelia

Answer 1

This is a known problem in Agda. You can find the corresponding issue on the Agda github at https://github.com/agda/agda/issues/1556.

Flossi