Wrong variable name in constraints for higher constructor

[jespercockx]

This may be related to #3659, but this time it is in the unsolved constraints you get when pattern matching on a higher inductive type. Minimal example:

{-# OPTIONS --cubical #-}

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

module _ where

data D (A : Set) : Set where
  c : A → D A
  path : (x : A) → c x ≡ c x

map : {A B : Set} → (A → B) → D A → D B
map f (c x) = c (f x)
map f (path x i) = path (f x) {!!}

Agda reports the following:

?0 : I

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  path (x x₁) (?0 (f = x) (x = x₁) (i = i0)) = c (x x₁) : D B
  path (x x₁) (?0 (f = x) (x = x₁) (i = i1)) = c (x x₁) : D B

The proper constraints should be like this instead:

  path (f x) (?0 (f = f) (x = x) (i = i0)) = c (f x) : D B
  path (f x) (?0 (f = f) (x = x) (i = i1)) = c (f x) : D B

[Saizan]

I believe this is just an unfortunate printout. notice how (f = x) and (x = x₁) in the arguments to the meta.

If you give names in the type signature you get better names in the constraints:

map : {A B : Set} → (g : A → B) → (d : D A) → D B
map f (c x) = c (f x)
map f (path x i) = path (f x) { }0

Failed to solve the following constraints:
  path (g x) (?0 (f = g) (x = x) (i = i0)) = c (g x) : D B
  path (g x) (?0 (f = g) (x = x) (i = i1)) = c (g x) : D B

It would be great if we could get the user-provided names in the clause all the way to checkIApplyConfluence. However we get the clauses from the coverage checker, while the names seem most accessible from checkClause.

[plt-amy]

I had forgotten about this issue, but it was actually fixed in 1fd6b9f. Constraints printed now:

Checking Test30 (/home/amelia/default/Projects/agda/Test30.agda).
Failed to solve the following constraints:
  path (f x) (?0 (f = f) (x = x) (i = i1)) = c (f x) : D B
    (blocked on _12)
  path (f x) (?0 (f = f) (x = x) (i = i0)) = c (f x) : D B
    (blocked on _12)
Unsolved interaction metas at the following locations:
  /home/amelia/default/Projects/agda/Test30.agda:15,31-35

[plt-amy]

Actually, give me just a second to add a test case.

[asr]

I had forgotten about this issue, but it was actually fixed in 1fd6b9f.

That commit is included in 2.6.3 RC2, so I'll change the milestone to 2.6.3.

[asr]

@plt-amy, please cherry-pick the test case into the release-2.6.3 branch.

[plt-amy]

@asr Done, thanks for the reminder 🙂