Push constraint name into default method impls

If a default method implementation refers to another method in the
interface, it's going to be one from the interface being defined, so
push it through explicitly.
This is only going to be guaranteed to be the case for default method
implementations - we can't assume anything for other implementations.
Fixes #77

src/Core/Context.idr

@@ -1268,6 +1268,13 @@ addOpenHint hintn_in
          hintn <- toResolvedNames hintn_in
          put Ctxt (record { openHints $= insert hintn () } defs)
 
+export
+dropOpenHint : {auto c : Ref Ctxt Defs} -> Name -> Core ()
+dropOpenHint hintn_in
+    = do defs <- get Ctxt
+         hintn <- toResolvedNames hintn_in
+         put Ctxt (record { openHints $= delete hintn } defs)
+
 export
 setOpenHints : {auto c : Ref Ctxt Defs} -> NameMap () -> Core ()
 setOpenHints hs

src/Idris/Elab/Implementation.idr

@@ -37,22 +37,37 @@ bindConstraints fc p [] ty = ty
 bindConstraints fc p ((n, ty) :: rest) sc
     = IPi fc RigW p n ty (bindConstraints fc p rest sc)
 
-addDefaults : FC -> List Name -> List (Name, List ImpClause) ->
+addDefaults : FC -> Name -> List Name -> List (Name, List ImpClause) ->
               List ImpDecl -> 
               (List ImpDecl, List Name) -- Updated body, list of missing methods
-addDefaults fc ms defs body
-    = let missing = dropGot ms body in
+addDefaults fc impName allms defs body
+    = let missing = dropGot allms body in
           extendBody [] missing body
   where
+    -- Given the list of missing names, if any are among the default definitions,
+    -- add them to the body
     extendBody : List Name -> List Name -> List ImpDecl -> 
                  (List ImpDecl, List Name)
     extendBody ms [] body = (body, ms)
     extendBody ms (n :: ns) body
         = case lookup n defs of
                Nothing => extendBody (n :: ms) ns body
-               Just cs => extendBody ms ns 
-                              (IDef fc n (map (substLocClause fc) cs) :: body)
+               Just cs => 
+                    -- If any method names appear in the clauses, they should
+                    -- be applied to the constraint name __con because they
+                    -- are going to be referring to the present implementation.
+                    -- That is, default method implementations could depend on
+                    -- other methods.
+                    -- (See test idris2/interface014 for an example!)
+                    let mupdates 
+                            = map (\n => (n, IImplicitApp fc (IVar fc n)
+                                                          (Just (UN "__con"))
+                                                          (IVar fc impName))) allms
+                        cs' = map (substNamesClause [] mupdates) cs in
+                        extendBody ms ns 
+                             (IDef fc n (map (substLocClause fc) cs') :: body)
 
+    -- Find which names are missing from the body
     dropGot : List Name -> List ImpDecl -> List Name
     dropGot ms [] = ms
     dropGot ms (IDef _ n _ :: ds)
@@ -139,13 +154,12 @@ elabImplementation {vars} fc vis pass env nest cons iname ps impln mbody
 
                -- 1.5. Lookup default definitions and add them to to body
                let (body, missing)
-                     = addDefaults fc (map (dropNS . fst) (methods cdata)) 
+                     = addDefaults fc impName (map (dropNS . fst) (methods cdata)) 
                                       (defaults cdata) body_in
 
                log 5 $ "Added defaults: body is " ++ show body
                log 5 $ "Missing methods: " ++ show missing
 
-
                -- 2. Elaborate top level function types for this interface
                defs <- get Ctxt
                fns <- topMethTypes [] impName methImps impsp (params cdata)

src/TTImp/Utils.idr

@@ -111,6 +111,7 @@ mutual
       = IForce fc (substNames bound ps t)
   substNames bound ps tm = tm
 
+  export
   substNamesClause : List Name -> List (Name, RawImp) -> 
                      ImpClause -> ImpClause 
   substNamesClause bound ps (PatClause fc lhs rhs)

tests/Main.idr

@@ -39,7 +39,7 @@ idrisTests
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",
        "interface009", "interface010", "interface011", "interface012",
-       "interface013",
+       "interface013", "interface014",
        "lazy001",
        "linear001", "linear002", "linear003", "linear004", "linear005",
        "linear006", "linear007",

tests/idris2/error004/expected

@@ -2,7 +2,7 @@
 Error1.idr:8:9--9:1:While processing right hand side of Main.wrong at Error1.idr:8:1--9:1:
 Can't find an implementation for Show (Vect (S (S (S (S Z)))) Integer)
 1/1: Building Error2 (Error2.idr)
-Error2.idr:11:1--15:1:While processing right hand side of Main.showPrec at Error2.idr:11:1--15:1:
+Error2.idr:13:38--15:1:While processing right hand side of Main.show at Error2.idr:13:3--15:1:
 Multiple solutions found in search. Possible correct results:
 	Show implementation at Error2.idr:11:1--15:1
 	Show implementation at Error2.idr:7:1--11:1

tests/idris2/interface014/DepInt.idr

@@ -0,0 +1,13 @@
+import Control.Monad.Identity
+
+public export
+interface Foo (sA : Type) where
+  A : Type
+  Elem : A -> sA -> Type
+  Empty : sA -> Type
+  Empty as = (a : A) -> Not (Elem a as)
+
+public export
+implementation Foo (Identity Bool) where
+  A = Bool
+  Elem x (Id y) = x = y

tests/idris2/interface014/expected

@@ -0,0 +1 @@
+1/1: Building DepInt (DepInt.idr)

tests/idris2/interface014/run

@@ -0,0 +1,3 @@
+$1 DepInt.idr --check
+
+rm -rf build