@@ -186,27 +186,29 @@ getFixedInType i _ _ _ = []
186186getFlexInType i env ps (Bind n (Pi _ t _) sc)
187187 = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++
188188 getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)
189+
189190getFlexInType i env ps tm@(App _ f a)
190− | (P _ tn _, args) <- unApply tm
191+ | (P nt tn _, args) <- unApply tm, nt /= Bound
191192 = case lookupCtxt tn (idris_datatypes i) of
192193 [t] -> nub $ paramNames args env [x | x <- [0..length args],
193194 not (x `elem` param_pos t)]
194195 ++ getFlexInType i env ps f ++
195196 getFlexInType i env ps a
196− [] -> let ppos = case lookupCtxt tn (idris_fninfo i) of
197− [fi] -> fn_params fi
198− [] -> [] in
199− nub $ paramNames args env [x | x <- [0..length args],
200− not (x `elem` ppos)]
201− ++ getFlexInType i env ps f ++
202− getFlexInType i env ps a
197+ [] -> let ppos = case lookupCtxtName tn (idris_fninfo i) of
198+ [fi] -> fn_params (snd fi)
199+ [] -> []
200+ xs -> error ("Too much function info: " ++ show xs)
201+ in nub $ paramNames args env [x | x <- [0..length args],
202+ not (x `elem` ppos)]
203+ ++ getFlexInType i env ps f ++
204+ getFlexInType i env ps a
203205 | otherwise = nub $ getFlexInType i env ps f ++
204206 getFlexInType i env ps a
205207getFlexInType i _ _ _ = []
206208
207−-- Treat a name as a parameter if it appears in parameter positions in
209+-- | Treat a name as a parameter if it appears in parameter positions in
208210-- types, and never in a non-parameter position in a (non-param) argument type.
209−
211+getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
210212getParamsInType i env ps t = let fix = getFixedInType i env ps t
211213 flex = getFlexInType i env fix t in
212214 [x | x <- fix, not (x `elem` flex)]