Check for name clashes in impl constraints

We were only checking parameters, meaning that there were potential
clashes leading to confusing behaviour, and meaning that it was somehow
relevant what the names were in the interface!

src/Idris/Elab/Implementation.idr

@@ -98,7 +98,8 @@ elabImplementation {vars} fc vis pass env nest cons iname ps impln mbody
          Just conty <- lookupTyExact (iconstructor cdata) (gamma defs)
               | Nothing => throw (UndefinedName fc (iconstructor cdata))
 
-         let impsp = nub (concatMap findIBinds ps)
+         let impsp = nub (concatMap findIBinds ps ++ 
+                          concatMap findIBinds (map snd cons))
 
          logTerm 3 ("Found interface " ++ show cn) ity
          log 3 $ " with params: " ++ show (params cdata)

tests/Main.idr

@@ -38,6 +38,7 @@ idrisTests
        "interactive009", "interactive010", "interactive011", "interactive012",
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",
+       "interface009",
        "lazy001",
        "linear001", "linear002", "linear003", "linear004", "linear005",
        "linear006", "linear007",

tests/idris2/interface009/Odd.idr

@@ -0,0 +1,9 @@
+interface Foo m where
+  bar : k -> v -> m k v -> m k v
+  
+-- This is kind of meaningless, except it exposes a potential error where
+-- (\s, t => List (s, t)) is substituted in as 'm' in 'm k v' and the ks
+-- clash, so one has to be renamed.
+Eq k => Foo (\s, t => List (s, t)) where
+  bar x y z = ?bang
+

tests/idris2/interface009/expected

@@ -0,0 +1,12 @@
+1/1: Building Odd (Odd.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main>  0 v : Type
+ 0 k' : Type
+ 0 k : Type
+   conArg : Eq k
+   z : List (k', v)
+   y : v
+   x : k'
+-------------------------------------
+bang : List (k', v)
+Main> Bye for now!

tests/idris2/interface009/input

@@ -0,0 +1,3 @@
+:t bang
+:q
+

tests/idris2/interface009/run

@@ -0,0 +1,3 @@
+$1 Odd.idr < input
+
+rm -rf build