Cannot unify variable with itself

[klkblake]

When typechecking this instance declaration (Note that this is the only use of the name v1 in the program):

instance Show v1 => Show (PType {v=v1} e a) where
  show = showPrec 0

I get the following error message:

type.idr:48:10:When elaborating type of Prelude.PType e a instance of Prelude.Show, method show:
Can't unify
        Set v1
with
        Set v1

Specifically:
        Can't unify
                v1
        with
                v1

I don't know if the error itself is a bug, but if it's not, the uninformitive error message probably should be. Possibly relevant context for the above:

PType : Set v -> Type -> Type
showPrec : Show v => {e : Set v} -> Nat -> PType e a -> String

I am using the latest git version (0.9.11.2-git:ecfb293), so I have the recent unification changes.

[edwinb]

Do you have a self contained program which demonstrates this issue? I've just constructed one and it typechecks fine. It is possible that I've just fixed it while fixing another problem, though.

The "Can't unify x with x" thing is irritating, and I'm not sure how we might fix it yet. It arises because of shadowing - probably some kind of hint as to which bits are different would be useful.

[david-christiansen]

If you load it in Emacs, mousing over the variables will show internal IDs. This can distinguish them.

Perhaps we can print binding site information in errors when there's shadowing?

[klkblake]

Unfortunately, I do not have a test program -- I changed the way PType works, and I didn't think to keep a copy. I do remember that removing the "a" type variable was enough to make it type-check. However, I've found that Idris seems to do more theorem-proving about the program than I thought, and the fact that Set only had temporary constructors that did not reflect the actual invariants may or may not have influenced it (I had another type error where that was the problem).

[edwinb]

I'm closing this because I can't do anything without more information, and as reported it works fine! If it happens again and you still have the test case, please reopen the issue.