[Agda] Incompatibilities affecting ``Fresh Look''

[kahl at cas.mcmaster.ca]

On Tue, Dec 14, 2010 at 03:51:39PM +0100, Nils Anders Danielsson answered:
> 
> > Second Problem: In Data.Product.Extras, they have:
> >
> > \begin{code}
> > proj₁-injective : ∀ {a b} {A : Set a} {B : A → Set b} {x y : Σ A B}
> >                      (B-uniq : ∀ {z} (p₁ p₂ : B z) → p₁ ≡ p₂)
> >                    → proj₁ x ≡ proj₁ y → x ≡ y
> > proj₁-injective {x = (a , p₁)} {y = (.a , p₂)} B-uniq refl
> >    = cong (λ p → (a , p)) (B-uniq p₁ p₂)
> > \end{code}
> 
> [...]
> 
> > How can this be done?
> 
> proj₁-injective : ∀ {a b} {A : Set a} {B : A → Set b} {x y : Σ A B}
>                      (B-uniq : ∀ {z} (p₁ p₂ : B z) → p₁ ≡ p₂)
>                    → proj₁ x ≡ proj₁ y → x ≡ y
> proj₁-injective {B = B} {x = (a₁ , b₁)} {y = (a₂ , b₂)}
>                  B-uniq a₁≡a₂ = helper a₁≡a₂
>    where
>    helper : ∀ {a₁ a₂} {b₁ : B a₁} {b₂ : B a₂} →
>             a₁ ≡ a₂ → _,_ {B = B} a₁ b₁ ≡ (a₂ , b₂)
>    helper refl = cong ,_ (B-uniq _ _)
> 

Thank you very much!

> > and had to notice that the new Data.Maybe.decSetoid doesn't preserve
> > _≡_ anymore. Is the a ``right way'' to get this to work with the
> > current library
> 
> I don't think so.

I am therefore adding the old definition to their Data.Maybe.Extras;
this also involves the following lib-0.3 function:

  drop-just : ∀ {A : Set} {x y : A} → just x ≡ just y → x ≡ y
  drop-just refl = refl

I tried to adapt this to:

  drop-just′ : {a : Level} {A : Set a} {x y : A} → just x ≡ just y → x ≡ y
  drop-just′ {a} {A} {x} {y} refl = refl {x} {y}

/var/tmp/AGDA/pouillard-pottier-fresh-look-agda-2010/Data/Maybe/Extras.agda:32,28-32
Failed to solve the following constraints:
  _59 == _60 : _58
when checking that the pattern refl has type _59 ≡ _60
 
If I postulate drop-just′, it's usage in decPESetoid and the usage of that
in NotSoFresh.Derived go through.

Why did this work before and does not work now?
For proj₁-injective, I know that the treatment of records
has changed, but here, I don't know which of the changes in the past
year might affect this definition.
(I would not expect that universe-polymorphism is to blame.)


Wolfram