@@ -1058,10 +1058,17 @@ getPriority i tm = 1 -- pri tm
10581058addStatics :: Name -> Term -> PTerm -> Idris ()
10591059addStatics n tm ptm =
10601060 do let (statics, dynamics) = initStatics tm ptm
1061+ ist <- getIState
1062+ let paramnames = case lookupCtxtExact n (idris_fninfo ist) of
1063+ Just p -> getNamesFrom 0 (fn_params p) tm
1064+ _ -> []
1065+
10611066 let stnames = nub $ concatMap freeArgNames (map snd statics)
10621067 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1068+ \\ paramnames
10631069 -- also get the arguments which are 'uniquely inferrable' from
10641070 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1071+ -- or parameters to the type of a static
10651072 let statics' = nub $ map fst statics ++
10661073 filter (\x -> not (elem x dnames)) stnames
10671074 let stpos = staticList statics' tm
@@ -1084,8 +1091,13 @@ addStatics n tm ptm =
10841091 else (static, dynamic)
10851092 initStatics t pt = ([], [])
10861093
1094+ getNamesFrom i ps (Bind n (Pi _ _) sc)
1095+ | i `elem` ps = n : getNamesFrom (i + 1) ps sc
1096+ | otherwise = getNamesFrom (i + 1) ps sc
1097+ getNamesFrom i ps sc = []
1098+
10871099 freeArgNames (Bind n (Pi ty _) sc)
1088− = nub $ freeArgNames ty
1100+ = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
10891101 freeArgNames tm = let (_, args) = unApply tm in
10901102 concatMap freeNames args
10911103