Idris auto-generates implicits with clashing names

[yanok]

Steps to Reproduce

Here is the source:

module Clash

import Data.Fin

data X : Bool -> Type where
     MkX : Nat -> X b

f : X b -> Nat
f (MkX n) = n

data D : Bool -> Type where
     MkD : Fin (f (MkX 0)) -> D b

Here the implicit b argument of f and MkX has nothing to do with the implicit b in the output type, so Idris does the right thing by introducing an extra implicit of type Bool. The problem is it uses the same name.

Expected Behavior

The MkD type should be

{b : Bool} -> {b0 : Bool} -> Fin (f {b = b0} (MkX {b = b0} 0)) -> D b

Observed Behavior

λΠ> :t MkD
Clash.MkD : {b : Prelude.Bool.Bool} -> {b : Prelude.Bool.Bool} ->
            Data.Fin.Fin (Clash.f {b = b} (Clash.MkX {b = b} 0)) -> Clash.D b

[yanok]

I think this is mostly pretty printing issue: internally these two bs are distinct, one being machine-generated. It's the pretty-printer who displays MN i "b" as "b".

[ahmadsalim]

Thanks for reporting the issue.