@@ -50,8 +50,12 @@ genClauses fc n xs given
50 logLvl 10 $ show argss ++ "\n" ++ show all_args
50 logLvl 10 $ show argss ++ "\n" ++ show all_args
51 logLvl 10 $ "Original: \n" ++
51 logLvl 10 $ "Original: \n" ++
52 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
52 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)
53+ -- add an infinite supply of explicit arguments to update the possible
54+ -- cases for (the return type may be variadic, or function type, sp
55+ -- there may be more case splitting that the idris_implicits record
53 let parg = case lookupCtxt n (idris_implicits i) of
57 let parg = case lookupCtxt n (idris_implicits i) of
54− (p : _) -> p
58+ (p : _) -> p ++ repeat (PExp 0 False Placeholder "")
55 _ -> repeat (pexp Placeholder)
59 _ -> repeat (pexp Placeholder)
56 let tryclauses = mkClauses parg all_args
60 let tryclauses = mkClauses parg all_args
57 logLvl 2 $ show (length tryclauses) ++ " initially to check"
61 logLvl 2 $ show (length tryclauses) ++ " initially to check"