<div dir="ltr">Unification is based on reduction, so since primForce x f doesn&#39;t immediately reduce to f x (which is the whole point) they also don&#39;t unify. To reason about programs using primForce you have to use primForceLemma, something I think is pretty clear from the documentation. In your example you can define <span style="font-size:12.8px">wrap→dup as follows:</span><div><span style="font-size:12.8px"><br></span></div><div><div><span style="font-size:12.8px">subst : {A : Set} (P : A → Set) {x y : A} → x ≡ y → P y → P x</span></div><div><span style="font-size:12.8px">subst P refl px = px</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">wrap→dup : ∀ {n : Nat} → (w : Wrap n) → Dup (unwrap w)</span></div><div><span style="font-size:12.8px">wrap→dup (wrap 0) = zero</span></div><div><span style="font-size:12.8px">wrap→dup (wrap (suc n)) = subst Dup (primForceLemma (unwrap (wrap n)) suc) suc</span></div><div style="font-size:12.8px"><br></div></div><div style="font-size:12.8px">/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Sep 7, 2016 at 3:43 AM, Martin Stone Davis <span dir="ltr">&lt;<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">The typechecker seems unwilling to unify &#39;primForce x f&#39; with &#39;f x&#39;, as the code below shows. Is this a bug in Agda? I.e. shouldn&#39;t it unify? I&#39;m unclear. The documentation on strictness (at <a href="https://agda.readthedocs.io/en/latest/language/built-ins.html#strictness" rel="noreferrer" target="_blank">https://agda.readthedocs.io/en<wbr>/latest/language/built-ins.htm<wbr>l#strictness</a>) mentions how it impacts on the compiler, but there seems to be no mention of how it works with the typechecker.<br>
<br>
I&#39;m hoping that it *should* unify because I&#39;ve run into a catch-22: I started using applications of strictness (Agda.Builtin.Strict.primForce<wbr>) in order to try to reduce a space leak during typechecking. Unfortunately, doing so led to some typechecking errors. In the code below, &#39;unwrap&#39; 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 &#39;wrap→dup&#39; to get it to type-check?<br>
<br>
  open import Agda.Builtin.Strict using (primForce)<br>
  open import Agda.Builtin.Nat using (Nat; zero; suc)<br>
<br>
  infixr 0 _$!_<br>
  _$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x<br>
  f $! x = primForce x f<br>
<br>
  data Wrap : Nat → Set where<br>
    wrap : (n : Nat) → Wrap n<br>
<br>
  data Dup : Nat → Set where<br>
    zero  : Dup zero<br>
    suc : ∀ {n : Nat} → Dup (suc n)<br>
<br>
  unwrap : ∀ {n : Nat} → Wrap n → Nat<br>
  unwrap (wrap 0) = 0<br>
  unwrap (wrap (suc n)) = Nat.suc $! (unwrap (wrap n))<br>
<br>
  wrap→dup : ∀ {n : Nat} → (w : Wrap n) → Dup (unwrap w)<br>
  wrap→dup (wrap 0) = zero<br>
  wrap→dup (wrap (suc n)) = suc<br>
  {- ERROR:<br>
       suc (_n_34 n) != primForce (unwrap (wrap n)) suc of type Nat<br>
       when checking that the expression suc has type<br>
       Dup (unwrap (wrap (suc n)))<br>
<br>
     No error if the strictness application is removed from &#39;unwrap&#39;.<br>
  -}<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div>