<div dir="ltr">Unification is based on reduction, so since primForce x f doesn't immediately reduce to f x (which is the whole point) they also don'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"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></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 '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 <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'm hoping that it *should* unify because I'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, '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?<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 'unwrap'.<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>