Abstract block leaking information for constructor-headedness checker

[GoogleCodeExporter]

Agda version 2.3.2

The following code compiles:

    module test where

    data U : Set where 
      a b : U

    data A : Set where
    data B : Set where

    abstract
      A' B' : Set

      A' = A
      B' = B

    [_] : U → Set
    [_] a = A'
    [_] b = B'

    f : ∀ u → [ u ] → U
    f u _ = u

    postulate x : A'

    zzz = f _ x


But if we change the definition of B' to:

      B' = A

It complains about unresolved metas. The reason for that is that `[_]` stops 
being constructor-headed. My understanding is that abstract blocks are not 
supposed to leak information, but in this case some information is leaked.

Original issue reported on code.google.com by rot...@gmail.com on 18 Feb 2013 at 2:47

[GoogleCodeExporter]

Bug n+1 concerning `abstract'.  It seems this leaking is intended, although I 
do not know why.  Looking into the relevant code in 
TypeChecking/Injectivity.hs, I see:

-- | Reduce simple (single clause) definitions.
reduceHead :: Term -> TCM (Blocked Term)
reduceHead v = ignoreAbstractMode $ do

headSymbol :: Term -> TCM (Maybe TermHead)
headSymbol v = ignoreAbstractMode $ do
  v <- ignoreBlocking <$> reduceHead v

Why?

Original comment by andreas....@gmail.com on 18 Feb 2013 at 4:05

• Changed state: Accepted
• Added labels: Abstract, Priority-Medium, Type-Defect

[GoogleCodeExporter]

@rotsor:  There might be a misunderstanding.  Thinking in terms of 'abstract 
blocks' is misleading.  You have defined a module with some abstract 
definitions, meaning that the definitions should not be known outside of the 
module.  However, the [_] function is defined inside the module.

However, you bug report is still valid because one can change your example to 
involve a module with abstract definitions and a separate module that should 
not have access to the definitions in the first module:

module Issue796a where

data U : Set where
  a b : U

data A : Set where
data B : Set where

module Abs where
 abstract
  A' B' : Set

  A' = A
  B' = B

module Conc where

  open Abs

  [_] : U → Set
  [_] a = A'
  [_] b = B'

  f : ∀ u → [ u ] → U
  f u _ = u

  postulate x : A'

  zzz = f _ x

In module Conc it should not be known that A' and B' are different so [_] 
should not be classified as injective.

Original comment by andreas....@gmail.com on 18 Feb 2013 at 9:07

• Added labels: Injectivity

[GoogleCodeExporter]

However, one could also argue that if A' and B' are abstract definitions from 
another module, they are never considered equal by the type checker, so [_] 
should be injective after all. After all, it does not matter whether they are 
equal as *values* (run-time equality), but whether they are equal as *syntax* 
(definitional equality).

Original comment by andreas....@gmail.com on 18 Feb 2013 at 9:17

[GoogleCodeExporter]

Fix pushed.  Example #2 no longer checks.  Original example still checks (see 
explanation in #1).

Original comment by andreas....@gmail.com on 19 Feb 2013 at 11:19

• Changed state: Fixed

[GoogleCodeExporter]

> Thinking in terms of 'abstract blocks' is misleading.  You have
> defined a module with some abstract definitions, meaning that the
> definitions should not be known outside of the module.

This is wrong, the definitions should be opaque also in the definition
of [_].

Andreas, can you explain why #1 checks but not #2?

Original comment by nils.anders.danielsson on 20 Feb 2013 at 4:34

• Changed state: Accepted

[GoogleCodeExporter]

The initial mode of Agda's type checker is 'AbstractMode' (see Base.hs).  I was 
quite puzzled about this, since I expected it to be 'ConcreteMode'.  
AbstractMode allows to see into abstract definitions of the same module.  Thus, 
#1 checks, but not #2.

If you say my understanding of 'abstract' is wrong, then probably the initial 
mode should be indeed 'ConcreteMode'.

Original comment by andreas....@gmail.com on 20 Feb 2013 at 11:09

[GoogleCodeExporter]

Changed initial mode to 'ConcreteMode', which now makes the original example 
fail as well.

Original comment by andreas....@gmail.com on 20 Feb 2013 at 11:45

• Changed state: Fixed