The positivity checker can still see through abstract

[GoogleCodeExporter]

The following program type checks, both in batch and in interactive mode:

module Bug where

abstract

  T : Set -> Set
  T a = a

data Foo (a : Set) : Set where
  foo : T (Foo a) -> Foo a

Original issue reported on code.google.com by nils.anders.danielsson on 19 Oct 2007 at 6:38

[GoogleCodeExporter]

Original comment by ulf.nor...@gmail.com on 22 Oct 2007 at 11:16

• Changed state: Accepted

[GoogleCodeExporter]

Original comment by ulf.nor...@gmail.com on 22 Oct 2007 at 11:16

• Added labels: Priority-Low
• Removed labels: Priority-Medium

[GoogleCodeExporter]

Original comment by ulf.nor...@gmail.com on 24 Oct 2007 at 10:35

[GoogleCodeExporter]

Original comment by ulf.nor...@gmail.com on 24 Oct 2007 at 3:34

• Changed state: Fixed

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 14 Nov 2012 at 10:09

• Added labels: Abstract

[GoogleCodeExporter]

This bug is back in Agda 2.3.2. There was apparently no failing test case for it.

Original comment by andreas....@gmail.com on 15 Nov 2012 at 11:21

• Changed state: Accepted
• Added labels: Priority-High
• Removed labels: Priority-Low

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 15 Nov 2012 at 11:22

• Added labels: Positivity

[GoogleCodeExporter]

Fixed (again), along with #796.

Original comment by andreas....@gmail.com on 21 Feb 2013 at 9:46

• Changed state: Fixed