"Refuse to construct infinite term" in an innocent-looking code

[GoogleCodeExporter]

The code:

    module test where

    data Q (A : Set) : Set where

    F : (N : Set → Set) → Set₁
    F N = (A : Set) → N (Q A) → N A

    postulate N : Set → Set
    postulate f : F N
    postulate R : (N : Set → Set) → Set
    postulate funny-term : ∀ N → (f : F N) → R N

    qqq : R N
    qqq = funny-term ? (λ A → f ?)

The error message:

    Refuse to construct infinite term by instantiating _9 to Q (?1 A)
    when checking that the expression f ? has type
    N (?1 (Q A)) → N (?1 A)

The error can be fixed in one of the following ways:

* Change Q to be a postulate instead of a data type
* Fill the first hole with N.
* Fill the second hole with A.

I can't explain why any of those changes fix the error or what the error is,
but it sure looks like a bug to me!

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

[GoogleCodeExporter]

Sorry, the formatting is wrong. The actuall error message ends with "N (?1 (Q 
A)) → N (?1 A)", the further text is mine.

Original comment by rot...@gmail.com on 18 Feb 2013 at 3:36

[GoogleCodeExporter]

Here is an analysis of the situation:

Agda first creates a (closed) meta variable

  ?N : Set -> Set

Then it checks

  λ A → f ?   against type F ?N = (A : Set) -> ?N (Q A) -> ?N A

(After what it does now, it still needs to check that

  R ?N  is a subtype of R N

It would be smart if that was done first.)

In context A : Set, continues to check

  f ?  against type  ?N (Q A) -> ?N A

Since the type of f is F N = (A : Set) -> N (Q A) -> N A, the created meta,
dependent on A : Set is

  ?A : Set -> Set

and we are left with checking that the inferred type of f (?A A),

  N (Q (?A A)) -> N (?A A)

is a subtype of

  ?N (Q A) -> ?N A

This yields two equations

  ?N (Q A) = N (Q (?A A))

  ?N A     = N (?A A)

The second one is solved as

  ?N = λ z → N (?A z)

simpliying the remaining equation to

  N (?A (Q A)) = N (Q (?A A))

and further to

  ?A (Q A) = Q (?A A)

The expected solution is, of course, the identity, but it cannot be
found mechanically from this equation.

At this point, another solution is ?A = Q.
In general, any power of Q is a solution.

If Agda postponed here, it would come to the problem

  R ?N  =  R N

simplified to ?N = N and instantiated to

  λ z → N (?A z)  =  N

This would solve ?A to be the identity.

Original comment by andreas....@gmail.com on 18 Feb 2013 at 2:48

• Changed state: Accepted
• Added labels: Meta, Priority-High, Type-Defect

[GoogleCodeExporter]

Oh! And why does changing Q to be a postulate help then?

Original comment by rot...@gmail.com on 18 Feb 2013 at 3:00

[GoogleCodeExporter]

Good question! ;-)

If you turn on {-# OPTIONS -v tc.meta:50 #-} and then search in the *Agda 
debug* buffer for "term " you see which equations Agda tries to solve.

Original comment by andreas....@gmail.com on 18 Feb 2013 at 3:43

[GoogleCodeExporter]

Fixed this issue by turning off the error "Refuse to construct infinite term" 
in favor of leaving metas unsolved.

Original comment by andreas....@gmail.com on 18 Feb 2013 at 3:44

• Changed state: Fixed
• Added labels: OccursCheck