Следующий код предназначен для описания C / C ++ -подобных перечислений, которые могут занимать 4 байта, хотя все, что они должны содержать, это всего лишь несколько различных альтернатив.
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
Пока все хорошо.Все тип проверяет красиво.Однако добавление следующих строк
func : ∀ {t} → Expr t → Bool
func (constant x) = false
, которые, кажется, ничего не делают, приводит к невозможности проверки типа и истощению всех системных ресурсов.
Я неЯ не вижу ничего, кроме аргумента экземпляра, который может привести к этому, но это, кажется, не согласуется с тем фактом, что Agda способна как решить, так и проверить тип следующего
5<2³² : (5 < 2 ^ 32) ≡ true
5<2³² = refl
в кратчайшие сроки.Так что же происходит?