[Agda] Re: Do we really want special case casts?

[Nils Anders Danielsson]

On 2009-10-20 00:42, Samuel Gélineau wrote:
> fail : {A : Set}{B : A → Set}
>      → {x₁ : A}{y₁ : B x₁}
>      → {x₂ : A}{y₂ : B x₂}
>      → y₁ ≅ y₂
>      → x₁ ≅ x₂
>      → y₁ ≅ y₂
> fail prf-y prf-x =      -- goal is (_≅_ {B x₁} y₁ {B x₂} y₂)
>   case prf-y of         -- case argument has type (_≅_ {B x₁} y₁ {B x₂} y₂)
>     refl {Bx} {y} ->    -- case argument has type (_≅_ {Bx} y {Bx} y)
>                         -- goal is (_≅_ {Bx} y {Bx} y)

This pattern is not well-typed; B x₁ and B x₂ cannot be unified.

>       case prf-x of     -- case argument has type (_≅_ {A} x₁ {A} x₂)
>         refl {A} {x} -> -- case argument has type (_≅_ {A} x {A} x)
>           refl {Bx} {y} -- goal is (_≅_ {Bx} y {Bx} y)

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.