Confusion between constructor and variable name

[UlfNorell]

From jesper.c...@gmail.com on November 26, 2013 15:34:52

Using the latest darcs version of Agda, I get an internal error at src/full/Agda/TypeChecking/Substitute.hs:82 for the following program:

=== BEGIN CODE ===

module InternalError (A : Set) where

data D : Set where d : D

data P : D → Set where

Confuse : (d : D) (p : P d) → Set Confuse x ()

confusing : (d : D) (p : P d) → Confuse d p confusing x ()

test : (x : P d) → Set test x with confusing d x test x | e = ?

=== END CODE ===

Some remarks:

• Leaving out the parameter A : Set removes the error, even though it is never used.
• Leaving out the index D of P also removes the error.
• Rewriting test so it no longer uses with removes the error as well. So this is the smallest example that I could come up with.

Original issue: http://code.google.com/p/agda/issues/detail?id=981

[UlfNorell]

From ulf.nor...@gmail.com on November 26, 2013 23:20:38

Status: Accepted
Owner: ulf.nor...@gmail.com
Labels: Type-Defect Priority-High Milestone-2.3.4

[UlfNorell]

From ulf.nor...@gmail.com on November 27, 2013 04:42:17

Status: Fixed