Application in type term not reduced in proof context, but reduced in goal

[radoye]

I can't work out why the function application S k == S j = True does not reduce to k == j = True during interactive proof in function scope. Especially, given the where clause that accepts the same term as a proof for both types. However, if put in the goal position, the type reduces.

module Reduction
%default total                                 
                                 
refl' : {x : Nat} -> {y : Nat} -> (x == y = True) -> (x = y)                                 
refl' {x = Z} {y = Z} prf = Refl
refl' {x = Z} {y = (S _)} Refl impossible
refl' {x = (S _)} {y = Z} Refl impossible
refl' {x = (S k)} {y = (S j)} prf = ?todo
  where
    fact : (S k == S j = True) -> (k == j = True)
    fact prf = prf

reduce_beq : (S k == S j) = True
reduce_beq = ?todo_beq

Here's the *idris-holes* buffer for the session.

Holes

This buffer displays the unsolved holes from the currently-loaded code. Press
the [P] buttons to solve the holes interactively in the prover.

- + Reduction.todo [P]
 `--               k : Nat
                   j : Nat
                 prf : S k == S j = True
     ------------------------------------
      Reduction.todo : S k = S j

- + Reduction.todo_beq [P]
 `--                   j : Nat
                       k : Nat
     -----------------------------------------------------------------------------------------------
      Reduction.todo_beq : Prelude.Nat.Nat implementation of Prelude.Interfaces.Eq, method == k j =
     True

Steps to Reproduce

$ idris --version
1.3.2

Expected Behavior

Non-neutral terms should be reduced regardless of the context.

Observed Behavior

A non-neutral term not is reduced properly when in goal position. However, it is not reduced in the proof context.