[Agda] change in handling of irrelevant parameters (bug?)

Nils Anders Danielsson nad at chalmers.se
Tue Mar 15 13:35:18 CET 2011


On 2011-03-15 12:02, Darin Morrison wrote:
> I noticed a change in the handling of irrelevant parameters between
> 2.2.9 and 2.2.10 which I think is beyond having irrelevant projections
> enabled by default. [...]

I don't know too much about irrelevance, but this doesn't look good.
Consider the following code:

   data D : Set where
     c : .Bool → D

   irr : c true ≡ c false
   irr = refl

   proj : D → Bool
   proj (c x) = x

   bad : proj (c true) ≡ proj (c false)
   bad = cong proj irr

As it happens the last definition does not type check, so perhaps we
cannot use this bug to produce an inconsistency, but it is at least
clear that the type system is broken in some way.

-- 
/NAD



More information about the Agda mailing list