@@ -1282,27 +1282,27 @@ getFixedInType i env is tm@(App f a)
1282 getFixedInType i env is a
1282 getFixedInType i env is a
1283getFixedInType i _ _ _ = []
1283getFixedInType i _ _ _ = []
1285−getFlexInType i env (Bind n (Pi t) sc)
1285+getFlexInType i env ps (Bind n (Pi t) sc)
1286− = nub $ getFlexInType i env t ++
1286+ = nub $ (if (not (n `elem` ps)) then getFlexInType i env ps t else []) ++
1287− getFlexInType i (n : env) (instantiate (P Bound n t) sc)
1287+ getFlexInType i (n : env) ps (instantiate (P Bound n t) sc)
1288−getFlexInType i env tm@(App f a)
1288+getFlexInType i env ps tm@(App f a)
1289 | (P _ tn _, args) <- unApply tm
1289 | (P _ tn _, args) <- unApply tm
1290 = case lookupCtxt tn (idris_datatypes i) of
1290 = case lookupCtxt tn (idris_datatypes i) of
1291 [t] -> nub $ paramNames args env [x | x <- [0..length args],
1291 [t] -> nub $ paramNames args env [x | x <- [0..length args],
1292 not (x `elem` param_pos t)]
1292 not (x `elem` param_pos t)]
1293− ++ getFlexInType i env f ++
1293+ ++ getFlexInType i env ps f ++
1294− getFlexInType i env a
1294+ getFlexInType i env ps a
1295− [] -> nub $ getFlexInType i env f ++
1295+ [] -> nub $ getFlexInType i env ps f ++
1296− getFlexInType i env a
1296+ getFlexInType i env ps a
1297− | otherwise = nub $ getFlexInType i env f ++
1297+ | otherwise = nub $ getFlexInType i env ps f ++
1298− getFlexInType i env a
1298+ getFlexInType i env ps a
1299−getFlexInType i _ _ = []
1299+getFlexInType i _ _ _ = []
1301-- Treat a name as a parameter if it appears in parameter positions in
1301-- 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.
1304getParamsInType i env ps t = let fix = getFixedInType i env ps t
1304getParamsInType 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
1306 [x | x <- fix, not (x `elem` flex)]
1306 [x | x <- fix, not (x `elem` flex)]
1308paramNames args env [] = []
1308paramNames args env [] = []
@@ -1354,11 +1354,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1354 [t] -> t
1354 [t] -> t
1356 let params = getParamsInType i [] fn_is fn_ty
1356 let params = getParamsInType i [] fn_is fn_ty
1357− let flex = getFlexInType i [] fn_ty
1358 let lhs = mkLHSapp $ stripUnmatchable i $
1357 let lhs = mkLHSapp $ stripUnmatchable i $
1359 propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1358 propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1360− logLvl 5 ("LHS: " ++ show fc ++ " " ++ show lhs)
1359+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
1361− logLvl 4 ("Fixed parameters: " ++ show (flex, params) ++ " from " ++ show lhs_in ++
1360+ logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++
1362 "\n" ++ show (fn_ty, fn_is))
1361 "\n" ++ show (fn_ty, fn_is))
1364 (((lhs', dlhs, []), probs, inj), _) <-
1363 (((lhs', dlhs, []), probs, inj), _) <-