[Agda] strictness application not unifying in the typechecker

[Martin Stone Davis]

The typechecker seems unwilling to unify 'primForce x f' with 'f x', as 
the code below shows. Is this a bug in Agda? I.e. shouldn't it unify? 
I'm unclear. The documentation on strictness (at 
https://agda.readthedocs.io/en/latest/language/built-ins.html#strictness) 
mentions how it impacts on the compiler, but there seems to be no 
mention of how it works with the typechecker.

I'm hoping that it *should* unify because I've run into a catch-22: I 
started using applications of strictness (Agda.Builtin.Strict.primForce) 
in order to try to reduce a space leak during typechecking. 
Unfortunately, doing so led to some typechecking errors. In the code 
below, 'unwrap' represents one of those functions that--I 
/think/---without an application of strictness, would result in a space 
leak (but with such an application, leads to typechecking errors further 
down). If Agda is behaving appropriately here, is there a clear way out 
of my dilemma? I.e. is there something I could change about 'wrap→dup' 
to get it to type-check?

   open import Agda.Builtin.Strict using (primForce)
   open import Agda.Builtin.Nat using (Nat; zero; suc)

   infixr 0 _$!_
   _$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
   f $! x = primForce x f

   data Wrap : Nat → Set where
     wrap : (n : Nat) → Wrap n

   data Dup : Nat → Set where
     zero  : Dup zero
     suc : ∀ {n : Nat} → Dup (suc n)

   unwrap : ∀ {n : Nat} → Wrap n → Nat
   unwrap (wrap 0) = 0
   unwrap (wrap (suc n)) = Nat.suc $! (unwrap (wrap n))

   wrap→dup : ∀ {n : Nat} → (w : Wrap n) → Dup (unwrap w)
   wrap→dup (wrap 0) = zero
   wrap→dup (wrap (suc n)) = suc
   {- ERROR:
        suc (_n_34 n) != primForce (unwrap (wrap n)) suc of type Nat
        when checking that the expression suc has type
        Dup (unwrap (wrap (suc n)))

      No error if the strictness application is removed from 'unwrap'.
   -}