Can't verify equality when using icmp

[L-as]

I get this error:

file.neut:20:14:
error: couldn't verify the definitional equality of the following two terms:
- (switch (icmp-eq-i32 0 0) (bool.true bool.true) (bool.false bool.true))
- bool.true

file.neut:

(inductive Eq ((A tau) (a A) (b A))
  (refl () (Eq A a a)))

(enum bool (true 1) (false 0))

; this works
(let (_
  (Eq *
    (enum-elimination bool.true
      (bool.true bool.true)
      (bool.false bool.true))
    bool.true))
  (Eq.refl * *))

; this doesn't
(let (_
  (Eq *
    (enum-elimination (icmp-eq-i32 0 0)
      (bool.true bool.true)
      (bool.false bool.true))
    bool.true))
  (Eq.refl * *))

[vekatze]

Hi, from the future. This was (and is) intentional. I chose not to reduce LLVM-level primitive operations when type checking because the compiler was based on GHC, which doesn't use LLVM by default.

I'm feeling like making them reducible when writing a self-hosting compiler, though.