Printing records in eta-contracted form let them look ill-typed sometimes

[GoogleCodeExporter]

postulate
  A : Set

record R (a : A) : Set where
  constructor c
  field 
    p : A

postulate
  a b : A
  r : R a

Now,

  R.p {b} (c {b} (R.p {a} r)

reduces to the ill-typed

  R.p {b} r

instead of R.p {a} r

Original issue reported on code.google.com by andreas....@gmail.com on 12 Nov 2010 at 12:58

[GoogleCodeExporter]

Looks almost as if this reduction is the result of an eta-contraction

  c {b} (R.p {a} r) -> r

Original comment by andreas....@gmail.com on 12 Nov 2010 at 2:23

[GoogleCodeExporter]

To precise the report, the problem appears only in the form with a definition

relabel : R a -> R b
relabel r = c {b} (R.p {a} r)

R.p {b} (relabel r) reduces to R.p {b} r

The manually expanded term

  R.p {b} (c {b} (R.p {a} r)

reduces correctly to R.p {a} r.

Must be that the body of relabel is eta-contracted or something like that.

Original comment by andreas....@gmail.com on 12 Nov 2010 at 2:47

[GoogleCodeExporter]

The buggy behavior disappears if I skip eta-contraction of function bodies.
This is done by removing the line

  cs <- instantiateFull =<< mapM rebindClause cs

in Def.hs/checkFunDef. rebindClause is the identity, instantiateFull eta-contracts. Without this line the body of relabel is kept as is and not eta-contracted to r.

As a side effect, test/fail/Issue259.agda now type-checks.

How can I document this issue in the test suite? How can I write a test-case that ensures that a certain eta-contraction is not carried out? (When the type-checker works modulo eta...)

Original comment by andreas....@gmail.com on 12 Nov 2010 at 5:48

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 12 Nov 2010 at 5:52

• Changed title: Record eta-contraction (of function bodies) breaks well-typedness

[GoogleCodeExporter]

Undid my fix because it breaks Data.Star.Decoration of the std-lib.
Also, Simon Forster reports that fix was not complete.

Original comment by andreas....@gmail.com on 16 Nov 2010 at 10:37

[GoogleCodeExporter]

Now this triggers an error message, which it should not. Eta-contraction for records is a solid bug:

data _==_ {A : Set}(a : A) : A -> Set where
  refl : a == a

postulate
  A : Set
  a b : A
  F : A -> Set

record R (a : A) : Set where
  constructor c
  field 
    p : A

beta : (x : A) -> R.p {b} (c {b} x) == x
beta x = refl

lemma : (r : R a) -> R.p {b} (c {b} (R.p {a} r)) == R.p {a} r
lemma r = beta (R.p {a} r)

{-
    a != b of type A
    when checking that the expression beta (R.p {a} r) has type
    _==_ {A} (R.p {b} r) (R.p {a} r)
-}

Original comment by andreas....@gmail.com on 16 Nov 2010 at 11:45

Attachments:

• Issue361.agda

[GoogleCodeExporter]

Original comment by nils.anders.danielsson on 19 Jan 2011 at 5:12

• Added labels: Eta

[GoogleCodeExporter]

The example in Comment 6 no longer triggers an error message.

Original comment by nils.anders.danielsson on 2 Sep 2011 at 7:00

[GoogleCodeExporter]

Closing this.

Original comment by ulf.nor...@gmail.com on 2 Sep 2011 at 8:03

• Changed state: Fixed

[GoogleCodeExporter]

One or more problems in Issue361.agda remain.

Original comment by nils.anders.danielsson on 2 Sep 2011 at 8:27

• Changed state: Accepted

[GoogleCodeExporter]

One or more problems?  Anything that isn't just printing?

Original comment by ulf.nor...@gmail.com on 2 Sep 2011 at 8:48

[GoogleCodeExporter]

postulate
  A   : Set
  a b : A

record R (_ : A) : Set where
  constructor c
  field
    p : A

postulate
  r : R a

relabel : R a → R b
relabel r = c {b} (R.p {a} r)

-- Type of r: R a.
-- Type of relabel r: R b.
--
-- If we normalise relabel r we get r, which does not have type R b,
-- so it seems as if subject reduction is broken.

-- r-does-not-have-type-R-b : R b
-- r-does-not-have-type-R-b = r

Original comment by nils.anders.danielsson on 3 Sep 2011 at 4:40

[GoogleCodeExporter]

That is just printing. relabel r doesn't normalise to r, we just print it as r. 
Eta contracting the output helps a lot when working with big records. I don't 
think it's worth losing that over this.

Original comment by ulf.nor...@gmail.com on 4 Sep 2011 at 7:09

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

[GoogleCodeExporter]

No plans to fix this in the near future, since problem is minor and fix 
substantial.

Original comment by andreas....@gmail.com on 11 Sep 2011 at 7:08

• Changed title: Printing records in eta-contracted form let them look ill-typed sometimes

[andreasabel]

Here is an example using lambda.

postulate
  A : Set
  B : A → Set

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

test : (x : A) → D x
test = λ x → c (λ (y : B x) → y) x

-- Agda eta-contracts this to the following, which is not well-typed.

-- foo : (x : A) → D x
-- foo = c λ y → y

-- Cannot instantiate the metavariable _11 to solution x since it
-- contains the variable x which is not in scope of the metavariable
-- or irrelevant in the metavariable but relevant in the solution
-- when checking that the expression c λ y → y has type (x : A) → D x