Inconsistency by Forcing too much before universe checking

[GoogleCodeExporter]

Since type constructors are considered injective by the forcing analysis we are 
able to define the type for the "russel" paradox:

open import Data.Product

Type = Set₁

data Box : Type -> Set where

data Tree' : Set -> Type where
  sup' : ∀ (A : Type) -> (A → ∃ Tree') → Tree' (Box A)

Tree = ∃ Tree'

sup : (a : Type) -> (f : a -> Tree) -> Tree
sup a f = _ , sup' a f

a : Tree -> Type
a (._ , sup' a _) = a

f : (t : Tree) -> a t -> Tree
f (._ , sup' a f) = f

-- The rest is the standard paradox

open import Relation.Binary.PropositionalEquality
open import Data.Empty

normal : Tree -> Type
normal t = Σ (a t) (λ (y : a t) → (f t y ≡ sup (a t) (f t))) -> ⊥

nt : Type
nt = Σ Tree \ (t : Tree) -> normal t

p : nt -> Tree
p (x , _) = x

q : (y : nt) -> normal (p y)
q (x , y) = y

r : Tree
r = sup nt p

lemma : normal r
lemma ((y1 , y2) , z) = y2 (subst (\ y3 -> Σ _ \ (y : a y3) ->  f y3 y ≡ sup 
(a y3) (f y3)) (sym z) ((y1 , y2) , z))

russel : ⊥
russel = lemma ((r , lemma) , refl)

Original issue reported on code.google.com by sanzhi...@gmail.com on 21 Feb 2015 at 5:23

[GoogleCodeExporter]

More details on what is going on:

The argument A of sup' is being forced, that's because Box is considered 
injective.

The injectivity of "Box : Type -> Set" however is a problem because Set is 
smaller than Type, which is what allows the (A -> ∃ Tree') field.

Original comment by sanzhi...@gmail.com on 21 Feb 2015 at 6:45

[GoogleCodeExporter]

Constructor arguments that occur as indices in the target in something other 
than a pattern should not be forced, as they cannot be discarded during 
compilation.  Consequently, Epic crashes on this example:

$ agda --epic -i. -i.. Issue1441.agda
Checking Issue1441 (/home/abel/agda/test/bugs/Issue1441.agda).
...
Finished Issue1441.
Compiling: Issue1441
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/Compiler/Epic/Forcing.hs:270

Original comment by andreas....@gmail.com on 24 Feb 2015 at 3:51

• Added labels: Epic, Forcing, Type-Defect

[GoogleCodeExporter]

-- A short test case to expose the flaw in the forcing analysis

data Wrap (A : Set) : Set where
  wrap : A → Wrap A

data D : Set → Set1 where
  c : (A : Set) → D (Wrap A)

test : (A : Set) → D A → Set
test .(Wrap A) (c A) = A

-- this should crash Epic as long as A is considered forced in constructor c

Original comment by andreas....@gmail.com on 24 Feb 2015 at 3:57

[GoogleCodeExporter]

-- It is even worse if test computes a value (as opposed to a type)

data N : Set where
  zero : N
  suc  : N → N

data Sing : (n : N) → Set where
  sing : ∀ n → Sing n

data D : Set → Set where
  c : ∀ n → D (Sing n)

test : (A : Set) → D A → N
test .(Sing n) (c n) = n

-- this should crash Epic as long as n is considered forced in constructor c
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/Compiler/Epic/Forcing.hs:270

Original comment by andreas....@gmail.com on 24 Feb 2015 at 4:02

[GoogleCodeExporter]

Function types also cannot contain forced variables.

data D : Set → Set1 where
  c : (A B : Set) → D (A → B)

test : (X : Set) → D X → Set
test .(A → B) (c A B) = A

Compiling: Issue1441-5
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/Compiler/Epic/Forcing.hs:270

Original comment by andreas....@gmail.com on 24 Feb 2015 at 4:07

[GoogleCodeExporter]

See issue 1406.
The inconsistency has been introduced in 
https://github.com/agda/agda/commit/9a4ebdd372dc0510e2d77e726fb0f4e6f56781e8

Fixed by 
https://github.com/agda/agda/commit/40d28353e7a746f60cdd7ec66dec9dac5d70ee60

Original comment by andreas....@gmail.com on 24 Feb 2015 at 6:44

• Changed state: Fixed