Abstract block leaking information for constructor-headedness checker

[UlfNorell]

From rot...@gmail.com on February 18, 2013 15:47:13

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: http://code.google.com/p/agda/issues/detail?id=796

[UlfNorell]

From andreas....@gmail.com on February 18, 2013 08:05:59

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?

Status: Accepted
Labels: Type-Defect Priority-Medium Abstract

[UlfNorell]

From andreas....@gmail.com on February 18, 2013 13:07:33

@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.

Owner: andreas....@gmail.com
Labels: Injectivity

[UlfNorell]

From andreas....@gmail.com on February 18, 2013 13:17:41

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).

[UlfNorell]

From andreas....@gmail.com on February 19, 2013 15:19:28

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

Status: Fixed

[UlfNorell]

From nils.anders.danielsson on February 20, 2013 08:34:12

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?

Status: Accepted

[UlfNorell]

From andreas....@gmail.com on February 20, 2013 15:09:30

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'.

[UlfNorell]

From andreas....@gmail.com on February 20, 2013 15:45:58

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

Status: Fixed