@@ -1282,27 +1282,27 @@ getFixedInType i env is tm@(App f a)
12821282 getFixedInType i env is a
12831283getFixedInType i _ _ _ = []
12841284
1285−getFlexInType i env (Bind n (Pi t) sc)
1286− = nub $ getFlexInType i env t ++
1287− getFlexInType i (n : env) (instantiate (P Bound n t) sc)
1288−getFlexInType i env tm@(App f a)
1285+getFlexInType i env ps (Bind n (Pi t) sc)
1286+ = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++
1287+ getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)
1288+getFlexInType i env ps tm@(App f a)
12891289 | (P _ tn _, args) <- unApply tm
12901290 = case lookupCtxt tn (idris_datatypes i) of
12911291 [t] -> nub $ paramNames args env [x | x <- [0..length args],
12921292 not (x `elem` param_pos t)]
1293− ++ getFlexInType i env f ++
1294− getFlexInType i env a
1295− [] -> nub $ getFlexInType i env f ++
1296− getFlexInType i env a
1297− | otherwise = nub $ getFlexInType i env f ++
1298− getFlexInType i env a
1299−getFlexInType i _ _ = []
1293+ ++ getFlexInType i env ps f ++
1294+ getFlexInType i env ps a
1295+ [] -> nub $ getFlexInType i env ps f ++
1296+ getFlexInType i env ps a
1297+ | otherwise = nub $ getFlexInType i env ps f ++
1298+ getFlexInType i env ps a
1299+getFlexInType i _ _ _ = []
13001300
13011301-- Treat a name as a parameter if it appears in parameter positions in
1302−-- types, and never in a non-parameter position in a type.
1302+-- types, and never in a non-parameter position in a (non-param) argument type.
13031303
13041304getParamsInType i env ps t = let fix = getFixedInType i env ps t
1305− flex = getFlexInType i env t in
1305+ flex = getFlexInType i env fix t in
13061306 [x | x <- fix, not (x `elem` flex)]
13071307
13081308paramNames args env [] = []
@@ -1354,11 +1354,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13541354 [t] -> t
13551355 _ -> []
13561356 let params = getParamsInType i [] fn_is fn_ty
1357− let flex = getFlexInType i [] fn_ty
13581357 let lhs = mkLHSapp $ stripUnmatchable i $
13591358 propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1360− logLvl 5 ("LHS: " ++ show fc ++ " " ++ show lhs)
1361− logLvl 4 ("Fixed parameters: " ++ show (flex, params) ++ " from " ++ show lhs_in ++
1359+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
1360+ logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++
13621361 "\n" ++ show (fn_ty, fn_is))
13631362
13641363 (((lhs', dlhs, []), probs, inj), _) <-