Tactic decomposing_intros loop infinitely on goals containing the list type

[necrosovereign]

Tactic decomposing_intros (and, therefore, make_equiv) cannot be used when the goal contains the list type, because it goes into a infinite loop.

Example.

Require Import HoTT.Basics.

Goal forall A, { l : list A, l = l } -> Unit.
    decomposing intros. (* never finishes *)

My guess is that it has something to do with list being a recursive type

[Alizter]

Are you doing this with regular coq? I can't get it to work in the library.

[necrosovereign]

Sorry, I've just noticed that I've made a typo in the example: it should be decomposing_intros instead of decomposing intros. The corrected example:

Require Import HoTT.Basics.

Goal forall A, { l : list A, l = l } -> Unit.
    decomposing_intros. (* never finishes *)

I tested it in hoqtop version 8.12+alpha, but the definition of decomposing_intros on my installation is identical to the one in the repository, so I've assumed that it's still an issue.

If it has been fixed in the latest version, that I'm okay with this.

[Alizter]

Yes, this seems to be a problem. @JasonGross is the author of this tactic.

[JasonGross]

You probably want to add a fail 1 case for any recursive types you want it to handle to https://github.com/HoTT/HoTT/blob/46f10ef3c7218b912c6686ecec650e728c69085e/theories/Basics/Equivalences.v#L565-L569

Alternatively, we could try writing a tactic to determine whether or not some type is recursive or something. What should the spec of the tactic be?