Make with more general again?

[nad]

Agda rejects the following code:

Type-of : {A : Set} → A → Set
Type-of {A = A} _ = A

module _ (A : Set) where

  Foo : A → Set
  Foo a with Type-of a
  ... | B = B

Error message:

Cannot `with` on variable Type-of a bound in a module telescope (or
patterns of a parent clause)
when inferring the type of Type-of a

There are two issues here:

• Type-of a is not a variable, so the error message is misleading.
• Shouldn't it be possible to drop this restriction now that we have parameter refinement? (The code is accepted by Agda 2.4.2. I seem to recall that this restriction was introduced by @andreasabel.)

[andreasabel]

Once we print also non-identity parameter substitutions, we can lift the restriction.
I cannot find the original issue now, but my restriction was built in to prevent errors like f != f where the first f has a different parameter instantiation than the second.

[UlfNorell]

The issue Andreas couldn't find is #1342 (which could maybe do with a better title).

[nickcollins]

What's the status on this? I had the impression this was being worked on in 2016 but I'm having this issue today. Is there a workaround?

[UlfNorell]

The discussion has moved to #1342.