Propagation of explicit arguments in typeclasses

Given that we know what they're going to be, and this gives resolution a
better chance with dependent classes in particular

src/Idris/AbsSyntax.hs

@@ -1685,9 +1685,9 @@ aiFn inpat expat qq imp_meths ist fc f ds as
         case find n imps [] of
             Just (tm, imps') ->
               PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'
-            Nothing ->
-              PImp p True l n Placeholder :
-                insImpAcc (M.insert n Placeholder pnas) ps given imps
+            Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in
+              PImp p True l n ph :
+                insImpAcc (M.insert n ph pnas) ps given imps
     insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
       let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
         case find n imps [] of

src/Idris/Elab/Class.hs

@@ -94,7 +94,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
          mapM_ (rec_elabDecl info EAll info) (concat cfns)
 
          -- for each method, build a top level function
-         fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods
+         fns <- mapM (tfun cn constraint (syn { imp_methods = mnames })
+                           (map fst imethods)) imethods
          logLvl 5 $ "Functions " ++ show fns
          -- Elaborate the the top level methods
          mapM_ (rec_elabDecl info EAll info) (concat fns)
@@ -199,7 +200,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
              let anames = map (\x -> sMN x "arg") [0..]
              let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
              let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
-             iLOG (showTmImpls ty)
+             iLOG (showTmImpls ty')
              iLOG (show (m, ty', capp, margs))
              iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
              return [PTy doc [] syn fc o m ty',