[Agda] strictness application not unifying in the typechecker

[Ulf Norell]

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 wrap→dup as follows:

subst : {A : Set} (P : A → Set) {x y : A} → x ≡ y → P y → P x
subst P refl px = px

wrap→dup : ∀ {n : Nat} → (w : Wrap n) → Dup (unwrap w)
wrap→dup (wrap 0) = zero
wrap→dup (wrap (suc n)) = subst Dup (primForceLemma (unwrap (wrap n)) suc)
suc

/ Ulf

On Wed, Sep 7, 2016 at 3:43 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> 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'.
>   -}
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160907/e8fd265c/attachment.html