[Agda] unification and HITs

[Dan Licata]

Hi all,

I noticed an odd thing related to unification and the trick we use to implement higher inductive types with private data types.  It's a bit worrisome but I haven't been able to prove anything wrong from it (maybe someone else can?).  I was hoping someone would be able to explain what's going on here.  This happens in both 2.3.2.1 and the development version.  

A self-contained file with the code is here:
https://github.com/dlicata335/hott-agda/blob/master/misc/UnificationWeirdness.agda

Here's what I notice that seems wrong: Given

bad : S¹.S¹ → S¹.S¹
bad = S¹.S¹-rec S¹.base {!!}

The goal has type S1.base == S1.base (path from base to base).  If you do agda2-show-constraints, then there is a unification constraint
?0 := id
This seems wrong to me, because there is no reason that this path should be id.  


However, I wasn't able to exploit this to prove something incorrect:

It's clearly related to the trick for HITs, because it doesn't happen if we do the same thing with a postulate version of S1-rec, instead of with the version that reduces:
notbad1 : S¹.S¹ → S¹.S¹
notbad1 = S¹.S¹-rec-postulate S¹.base {!!}

If we write the loop in place of that goal (which unification said had to be id), then Agda accepts it:
fillbad : S¹.S¹ → S¹.S¹
fillbad = S¹.S¹-rec S¹.base S¹.loop

If there is some variable of type base=base, then the unification constraint is not generated:
notbad2 : (S¹.base == S¹.base) → S¹.S¹ → S¹.S¹
notbad2 t = S¹.S¹-rec S¹.base {!!} -- no constraint

We cannot equate S1-rec's with loop and id by unification:
notbad3 : (S¹.S¹-rec S¹.base S¹.loop) == (S¹.S¹-rec S¹.base id)
notbad3 = {!id!} -- id doesn't work

If there is something else in scope (locally) then the constraint is not generated:
l = S¹.loop
notbad4 : S¹.S¹ → S¹.S¹
notbad4 = S¹.S¹-rec S¹.base {!!} -- no constraint is generated


Any ideas about where this constraint comes from?

Thanks!
-Dan