Coq unification is up to convertibility but does not compute normal forms

gistfile1.v

Require Import ssreflect.

Fixpoint ackn (m : nat) (ack : nat -> nat) {struct m} :=
  match m with
  | O => ack 1
  | S q => ack (ackn q ack)
  end.
Fixpoint ack (n m : nat) {struct n} : nat :=
  match n with
  | O => S m
  | S p => ackn m (ack p)
  end.
Lemma ack_S m n : ack (S m) n = ackn n (ack m).
Proof. reflexivity. Qed.

Fail Timeout 1 Eval compute in ack 4 4.
Fail Timeout 1 Eval vm_compute in ack 4 4.

Goal ack 4 4 = ack 4 4.
reflexivity.
Restart.
rewrite {1}ack_S.
Fail Timeout 1 reflexivity.
Abort.

Goal ack (3 + 1) 4 = ack 4 4.
reflexivity.
Goal ack 3 4 = ack 4 4.
Timeout 1 reflexivity.