Positivity regression

[UlfNorell]

From darinmor...@gmail.com on April 04, 2012 00:03:21

In the following code, 'e' does not pass the termination check with the darcs version of Agda. With version Agda 2.3.0.1, it works fine.

--BEGIN {-# OPTIONS --guardedness-preserving-type-constructors #-} module Fail where

infixl 6 ⊔

postulate Level : Set zero : Level suc : Level → Level ⊔ : Level → Level → Level

{-# BUILTIN LEVEL Level #-} {-# BUILTIN LEVELZERO zero #-} {-# BUILTIN LEVELSUC suc #-} {-# BUILTIN LEVELMAX ⊔ #-}

infix 1000 ♯_

postulate ∞ : ∀ {a} (A : Set a) → Set a ♯_ : ∀ {a} {A : Set a} → A → ∞ A ♭ : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞ #-} {-# BUILTIN SHARP ♯_ #-} {-# BUILTIN FLAT ♭ #-}

data CoNat : Set0 where z : CoNat s : ∞ CoNat → CoNat

record A : Set2 where field f : Set1

record B (a : ∞ A) : Set1 where field f : A.f (♭ a)

postulate a : A

e : CoNat → A e z = a e (s n) = record { f = B (♯ e (♭ n)) } --END

Original issue: http://code.google.com/p/agda/issues/detail?id=602

[UlfNorell]

From darinmor...@gmail.com on April 03, 2012 15:11:08

It might be better for testing purposes to change the definition of the record B to the following, although both versions exhibit the behaviour:

record B (a : ∞ A) : Set1 where field f1 : Set f2 : f1 → A.f (♭ a)

[UlfNorell]

From ulf.nor...@gmail.com on April 04, 2012 04:49:42

The reason it doesn't pass the termination checker is that the argument to B is marked as negative by the positivity checker. Type constructors only preserve guardedness in their positive arguments, I'm not sure why but I can imagine that it's for pesky soundness reasons.

The real question is why the argument to B is suddenly considered negative. Here's a simpler example that shows the problem (and doesn't rely on --guardedness-preserving-type-constructors):

record A : Set₁ where constructor mkA field f : Set

unA : A → Set unA (mkA x) = x

data B (a : A) : Set where mkB : unA a → B a

data D : Set where d : B (mkA D) → D

-- D is not strictly positive, because bla bla bla

Nisse you did some work on the positivity checker recently, could you take a look? Interestingly: if A is changed to a datatype it works.

Summary: Positivity regression
Status: Accepted
Owner: nils.anders.danielsson
Cc: ulf.nor...@gmail.com
Labels: Priority-High Type-Defect

[UlfNorell]

From ulf.nor...@gmail.com on April 04, 2012 05:07:29

It turns out that record projections are not considered positive in the record argument. They should be and changing that makes the example type check. What's weird is that Agda-2.3.0.1 doesn't treat record projection arguments as positive either, so I have no idea why the example checks in 2.3.0.1. It's fixed now anyway.

Status: Fixed

[UlfNorell]

From andreas....@gmail.com on April 04, 2012 08:32:34

Owner: ulf.nor...@gmail.com
Labels: Positivity