@@ -1058,10 +1058,17 @@ getPriority i tm = 1 -- pri tm
1058addStatics :: Name -> Term -> PTerm -> Idris ()
1058addStatics :: Name -> Term -> PTerm -> Idris ()
1059addStatics n tm ptm =
1059addStatics n tm ptm =
1060 do let (statics, dynamics) = initStatics tm ptm
1060 do let (statics, dynamics) = initStatics tm ptm
1062+ let paramnames = case lookupCtxtExact n (idris_fninfo ist) of
1063+ Just p -> getNamesFrom 0 (fn_params p) tm
1061 let stnames = nub $ concatMap freeArgNames (map snd statics)
1066 let stnames = nub $ concatMap freeArgNames (map snd statics)
1062 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1067 let dnames = nub $ concatMap freeArgNames (map snd dynamics)
1063 -- also get the arguments which are 'uniquely inferrable' from
1069 -- also get the arguments which are 'uniquely inferrable' from
1064 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1070 -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
1071+ -- or parameters to the type of a static
1065 let statics' = nub $ map fst statics ++
1072 let statics' = nub $ map fst statics ++
1066 filter (\x -> not (elem x dnames)) stnames
1073 filter (\x -> not (elem x dnames)) stnames
1067 let stpos = staticList statics' tm
1074 let stpos = staticList statics' tm
@@ -1084,8 +1091,13 @@ addStatics n tm ptm =
1084 else (static, dynamic)
1091 else (static, dynamic)
1085 initStatics t pt = ([], [])
1092 initStatics t pt = ([], [])
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 = []
1087 freeArgNames (Bind n (Pi ty _) sc)
1099 freeArgNames (Bind n (Pi ty _) sc)
1088− = nub $ freeArgNames ty
1100+ = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
1089 freeArgNames tm = let (_, args) = unApply tm in
1101 freeArgNames tm = let (_, args) = unApply tm in
1090 concatMap freeNames args
1102 concatMap freeNames args