[Agda] Incompatibilities affecting ``Fresh Look''

[kahl at cas.mcmaster.ca]

I am trying to get Nicolas Pouillard and François Pottier's ``Fresh Look''

  http://nicolaspouillard.fr/publis/pouillard-pottier-fresh-look-agda-2010/

to work with current Agda and standard library.


I encountered two problems:

First problem: In NotSoFresh.Derived, they have:

_≟MaybeName_ : ∀ {α} → Decidable {A = Maybe (Name α)} _≡_
_≟MaybeName_ = DecSetoid._≟_ (Data.Maybe.decSetoid (decSetoid _≟Name_))


In lib-0.3, Data.Maybe.decSetoid was:

  decSetoid : {A : Set} → Decidable (_≡_ {A = A}) → DecSetoid _ _

while now, it is:

  decSetoid : ∀ {ℓ₁ ℓ₂} → DecSetoid ℓ₁ ℓ₂ → DecSetoid _ _

So I tried (with |open import Relation.Binary.PropositionalEquality as PE|):

_≟MaybeName_ : ∀ {α} → Decidable {A = Maybe (Name α)} _≡_
_≟MaybeName_ = DecSetoid._≟_ (Data.Maybe.decSetoid (PE.decSetoid _≟Name_))

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, or should I just copy the old definition somewhere?



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}

This is now greeted with:

/var/tmp/AGDA/pouillard-pottier-fresh-look-agda-2010/Data/Product/Extras.agda:35,1-36,40
Not supported: Dot patterns inside record patterns, unless
accompanied by data type patterns
when checking that the clause
proj₁-injective {x = a , p₁} {y = .a , p₂} B-uniq refl
  = cong (λ p → a , p) (B-uniq p₁ p₂)
has type
{a b : .Level.Level} {A : Set a} {B : A → Set b} {x y : Σ A B}
(B-uniq : {z : A} (p₁ p₂ : B z) → p₁ ≡ p₂) →
proj₁ x ≡ proj₁ y → x ≡ y


I tried quite a few different combinations, but I just cannot get refl
to match. For example:

\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₂)
                  → let a₁ = proj₁ x
                        a₂ = proj₁ y
                    in a₁ ≡ a₂ → x ≡ y
proj₁-injective {a} {b} {A} {B} {x = (a₁ , p₁)} {y = (a₂ , p₂)} B-uniq  refl
          = cong (λ p → (a₁ , p)) (B-uniq  p₁ p₂)
\end{code}

/var/tmp/AGDA/pouillard-pottier-fresh-look-agda-2010/Data/Product/Extras.agda:25,73-77
a₁ != a₂ of type A
when checking that the pattern refl has type a₁ ≡ a₂


\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₂)
                  → let a₁ = proj₁ x
                        a₂ = proj₁ y
                    in a₁ ≡ a₂ → x ≡ y
proj₁-injective {a} {b} {A} {B} {x} {y} B-uniq  refl′ with proj₁ x
... | a₁  with proj₁ y
...  | a₂ with refl′
...   | refl 
          = cong (λ p → (a₁ , p)) (B-uniq (proj₂ x) (proj₂ y))
\end{code}

/var/tmp/AGDA/pouillard-pottier-fresh-look-agda-2010/Data/Product/Extras.agda:29,9-13
a₁ != a₂ of type A
when checking that the pattern refl has type a₁ ≡ a₂

\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₂)
                  → let a₁ = proj₁ x
                        a₂ = proj₁ y
                    in a₁ ≡ a₂ → x ≡ y
proj₁-injective {a} {b} {A} {B} {x} {y} B-uniq = let
    a₁ = proj₁ x
    a₂ = proj₁ y
  in let
    f : a₁ ≡ a₂ → x ≡ y
    f refl with a₂
    ... | .a₁ =
          cong (λ p → (a₁ , p)) (B-uniq (proj₂ x) (proj₂ y))
  in f
\end{code}

/var/tmp/AGDA/pouillard-pottier-fresh-look-agda-2010/Data/Product/Extras.agda:28,6-34,7
Not a valid let-declaration
when scope checking
let f : a₁ ≡ a₂ → x ≡ y
    f refl with a₂
    ... | .a₁ = cong (λ p → (a₁ , p)) (B-uniq (proj₂ x) (proj₂ y))
in f


For this, I find in the reference manual:

``the expression that we define in a let-expression can neither be
recursive nor defined by pattern matching.
[...]
we could also use where-expression to define recursive definitions by pattern matching.
''

So I try where, and it only gets worse again:

\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₂)
                  → let a₁ = proj₁ x
                        a₂ = proj₁ y
                    in a₁ ≡ a₂ → x ≡ y
proj₁-injective {a} {b} {A} {B} {x} {y} B-uniq =  f
  where
    a₁ = proj₁ x
    a₂ = proj₁ y
    f : a₁ ≡ a₂ → x ≡ y
    f refl with a₂
    ... | .a₁ =
          cong (λ p → (a₁ , p)) (B-uniq (proj₂ x) (proj₂ y))
\end{code}


How can this be done?



Wolfram