[Agda] Another potential typeclass bug in release-candidate/master

[David Darais]

Hi,

I have another use of typeclasses that fails to typecheck with both the release
candidate 2.5.0.20160213 and master, and which typechecks successfully with
2.4.2.5.

The problem is that typeclass resolution can't resolve metas in a rather simple
setting. In the definition of `stuck` in the code below, the unifier can't
determine some very basic information, like `A : Set` and `x : A`, and as a
result the typeclass instance `REFL : Reflexive A` can't be found. Agda had no
problem determining `A = ⟪ A ⟫` in 2.4.2.5 and I think it should continue to be
able to handle unification problems like this in the presence of type classes.

I tried to reduce the problem to be minimal. The first part of the setup is a
typeclass `Reflexive` for types `A : Set` which have a reflexive relation `_<_`
and proof of reflexivity `reflexivity : ∀ {x : A} → x < x`. The second part of
the setup is a type `Pack` which packages a type `A : Set` together with its
typeclass instance `Reflexive A`, and a type `⟪ A ⟫` which holds elements of
types packaged inside `A : Pack`. I then give a `Reflexive` instance for `⟪_⟫`
which the `stuck` definition is unable to find, although I think it should (and
so does Agda 2.4.2.5).

Thanks!
David

-- Code --
-- works in 2.4.2.5; unsolved metas in 2.5.0.20160213 and master --

-- A relation which is reflexive
record Reflexive (A : Set) : Set₁ where
  field
    _<_ : A → A → Set
    reflexivity : ∀ {x} → x < x
open Reflexive {{...}}

-- Packing a type with its reflexive relation
data Pack : Set₁ where
  ⇧ : ∀ (A : Set) {{_ : Reflexive A}} → Pack

-- Projecting the raw type from a packed type
dom : Pack → Set
dom (⇧ A) = A

-- Elements of a packed type
data ⟪_⟫ (A : Pack) : Set where
  ⟨_⟩ : dom A → ⟪ A ⟫

-- The ordering between projected types is the original reflexive relation
[_]_<ᵈ_ : ∀ (A : Pack) → dom A → dom A → Set
[ ⇧ A ] x <ᵈ y = x < y

-- Reflexivity between projected types
reflexivityᵈ : ∀ (A : Pack) (x : dom A) → [ A ] x <ᵈ x
reflexivityᵈ (⇧ A {{R}}) x = reflexivity {{R}}

-- The relation on packed elements, through projection
data _<⇧_ {A : Pack} : ⟪ A ⟫ → ⟪ A ⟫ → Set where
  ⟨_⟩ : ∀ {x y} → [ A ] x <ᵈ y → ⟨ x ⟩ <⇧ ⟨ y ⟩

-- The Reflexive instance for Pack
instance
  Reflexive[Pack] : ∀ {A : Pack} → Reflexive ⟪ A ⟫
  Reflexive[Pack] {A} = record
    { _<_ = _<⇧_
    ; reflexivity = λ{ {⟨ x ⟩} → ⟨ reflexivityᵈ A x ⟩ }
    }

-- Works
goal₁ : ∀ {A : Pack} → ⟪ A ⟫ → ⟪ A ⟫ → Set
goal₁ = _<_

-- Resolving (A : Set) explicitly works
goal₃ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x
goal₃ {A} x = reflexivity {⟪ A ⟫} {_}

-- Resolving (r : Reflexive A) explicitly works
goal₅ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x
goal₅ {A} x = reflexivity {_} {{Reflexive[Pack]}} {_}

-- Resolving (x : A) explicitly works
goal₄ : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x
goal₄ {A} x = reflexivity {_} {x}

-- Weird unsolved metas: (A : Set), (r : Reflexive A), (x : A), and
-- two others (? : x <⇧ x)
--
-- Why can't type class resolution solve this?
stuck : ∀ {A : Pack} (x : ⟪ A ⟫) → x < x
stuck x = reflexivity