Pretty printing of duplicate names should avoid name clashes

[plastpappa]

Steps to Reproduce

f : { a, b : Type } -> Either a b -> Either b a
f {a=b} x = x
f (Right x) = Left x
f (Left x) = Right x

Expected Behavior

Something like:

When unifying Either b1 b and Either b b1
Mismatch between:
        b1
and
        b
(duplicate b renamed to b1 to avoid name clash)

Observed Behavior

When unifying Either b b and Either b b
Mismatch between:
        b
and
        b

[ohad]

I think this is a bug with the idris name pretty printer.
Were you to introduce b, as in:

f {a=b} {b=b} x = x

you'd get the error:

Can't match on ?b [no locals in scope] (Non linear pattern variable)

which is idris2 saying: I'm not allowing you to ask me to compare values of pattern variables at runtime, you're going to have to choose an equality function yourself.

I think what's happening behind the scenes is that idris2 prints out the string representation of the name for the pattern variable for a, namely b, and the string representation of the name for the pattern variable for b, which is b again, and so they look the same.

@edwinb : do you think this could be the bug I've been having with Frex? I'm keen on having it fixed. If you're too busy, I'll take a crack at it. (Though if it's what I think it is, you'll be able to do it in a jiffy.)

If my summary above is correct, a fix would be to change the error message into:

When unifying Either b b' and Either b' b
Mismatch between:
        b
and
        b'
(we renamed b to b' to avoid a name clash.)

[plastpappa]

Yeah, that's what I figured. I actually noticed after posting that the Atom plugin prints the second b as a b1 like I suggested in my post (obviously b' works too), but I guess that's just a left-over from what it does in Idris 1. I'm not sure whether that's specific to the package or how Idris wants to handle these problems.

To me, once you introduce pattern matching on types etc. like Idris 2 does, being able to do things like this smoothly seems quite natural (and surely half the point of not blindly erasing them). Obviously you can't pattern match like this on values normally, but that's also because it's hard to think of scenarios where you would - and I think these features need to be rethought when they work on a much wider scope too, ie types. Isn't it possible to at least have an Eq Type instance now so this can be done via a with clause? I'm definitely out of my depth here so I invite anyone smarter than me to tell me why this doesn't make sense, but...

Also, come to think of it, if "names which are in scope in a type are also always in scope in the body of the corresponding definition," is there any feasible scenario in Idris 2 where you would need to introduce a new variable b equal to a in the definition like that? It seems like any working variant of {a=b} could be replaced let b = a in the actual function body. Is it only there for backwards compatibility?

[ohad]

I'm not going to defend the design decision 'names which are in scope in a type are also always in scope in the body of the corresponding definition' as I don't agree with it :D.

I think that what you are arguing for is that we should be able to write this function:

f : {a, b : Type} -> Bool
f {a = b} {b=b} = True
f               = False

I don't think we should.

I think it might be some kind of philosophy in dependently typed programming: pattern variables (i.e., binding occurences) should be given distinct names (rather than enforce equality). Case splitting should be driven by runtime information in constructors. Equality between names in different places in the pattern must only be deduced by other kind of type-dependency, induced by a concrete constructor. But what do I know, I'm a newbie in this area, so I'll leave the philosophy to the experts.

A less philosophical argument --- here's a different program, but related to your program:

namespace A
  f : {a : Type} -> Either a a -> Either a a
  f x = x

namespace B
  f : {a, b : Type} -> Either a b -> Either b a
  f (Right x) = Left x
  f (Left x) = Right x


test : Either String Int
test = f (the (Either Int String) $ Left 5)

This type-checks in Idris1 but not in Idris 2:

Ambiguous name [Main.B.f, Main.A.f]

so, unless this is a bug in idris2, it seems like we're moving away from nuanced disambiguation using type information for overloading resolution, let alone for actual case-splitting.

[plastpappa]

Thank you, that's an interesting insight. I never thought to separate them into distinct namespaces like that. I also think I agree with you that this is not a problem for a pattern match to solve.

I still think it'd be useful to leverage that same syntactical equivalence of types, or whatever you call it, (where Int = Int =/= String and Either a b = Either b a <-> a = b) like with Refl into something I can use to disambiguate certain cases of more general function calls. Again, maybe there's a reason why not. But say we did have type equality on ==: do you think the following is an at all reasonable pattern? Or is there somehow an alternative I'm not thinking of?

f : {a, b : Type} -> Either a b -> Either b a
f x with (a == b)
    f x         | True  = x
    f (Right x) | False = Left x
    f (Left x)  | False = Right x

I suppose there's no point anyway if this wouldn't lead to the necessary type information for the x to actually typecheck, which I'm not sure is there yet.

[gallais]

Isn't it possible to at least have an Eq Type instance now so this can be done via a with clause?

You can write a simulator run(M,n) running a Turing machine for n steps and
returning a Bool: True if it stopped in less than n steps, False otherwise.

To be able to decide the equality between type (n : Nat) -> () and type
(n : nat) -> if run(M,n) then Nat else (), you'd need to be able to decide
whether the Turing machine M ever terminates. For an arbitrary M.

The solution to your problem is to define a universe of the types you are
interested in. If it is restricted enough, you will be able to test the
equality of the codes representing the types rather than the types themselves.
Equality of codes implies equality of their interpretation i.e. the types
they represent.

David Christiansen has a talk about this idea

[plastpappa]

Thanks, makes sense. That idea will work for me. Apologies for the confusion! I'll modify this issue to be about the part that's actually (maybe) unintentional.

[edwinb]

I'm not going to defend the design decision 'names which are in scope in a type are also always in
scope in the body of the corresponding definition' as I don't agree with it :D.

Okay, then I will! One reason is that this way is consistent with what is displayed in holes. For example, if you have:

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = ?help

Then you say

Main> :t help

You get:

 0 m : Nat
 0 a : Type
   xs : Vect len a
   x : a
   ys : Vect m a
 0 n : Nat
-------------------------------------
help : Vect (S (plus len m)) a

If the names are displayed but not in scope, that's strange. So the point of the decision is, among other things, to make the display consistent with what's in scope.

As for the duplicate display, I've been wondering how to do this nicely for ages. One risk, if we're not careful, is we end up displaying a different name than the one which is in scope. I haven't thought about it very deeply though. This issue gives a good chance to think about a nice way to do it (it's probably not one I'll look at urgently, though, sorry.)

[gallais]

In Agda, the goals' context is simply listing the renamed variables which is
not very helpful. The goal itself however (or rather: any telescope) explicitly
mentions the user-provided name and the machine-picked renaming.

So if you ask the type of

id : {A : Set} {A : Set} {A : Set} -> A -> A
id = λ x → x

then the printer tells you it's

{A : Set} {A = A₁ : Set} {A = A₂ : Set} → A₂ → A₂

Cf. agda/agda#2572 (comment)

I think that is a pretty good design. I wonder whether it would make
contexts too verbose though in case users are shadowing variables a lot.

[ohad]

Responding to @edwinb :
I may have saw it somewhere (likely Agda?), but we can also prefix variables-from-type-scope-that-aren't-in-scope-yet with some symbol like .m, .a., .n to tell the user that these names aren't in scope yet.