Agda's type checker explodes

Question

The following code is meant to describe C/C++-like enumerations which can take 4 bytes although all they are supposed to contain is just a few different alternatives.

open import Prelude.Bool
open import Prelude.Nat
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Numeric.Nat.Pow renaming (_^′_ to _^_)

data Enum : Set where
  makeEnum : (size : Nat) → (variants : Nat) → 
             .{{ _ : (variants < size) ≡ true }} → Enum

five : Enum
five = makeEnum (2 ^ 32) 5

data Expr : (t : Enum) → Set where
  constant : (x : Nat) → Expr five

So far so good. Everything type checks nicely. However adding the following lines

func : ∀ {t} → Expr t → Bool
func (constant x) = false

that don't appear to be doing much of anything, leads to a nontermination of the type checker and depletion of all system resources.

I don't see anything besides the instance argument that could lead to this, but that does not seem to agree with the fact that Agda is able to both solve and type check the following

5<2³² : (5 < 2 ^ 32) ≡ true
5<2³² = refl

in no time. So what is going on?

Answer 1

The question was answered by Jesper Cockx. As it turns out it was a compiler bug that will be fixed in the next version of Agda.

Update: the bug has already been fixed in the master branch.