@@ -1178,21 +1178,28 @@ addUsingImpls syn n fc t
11781178-- status of each pi-bound argument, and whether it's inaccessible (True) or not.
11791179
11801180getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
1181−getUnboundImplicits i (Bind n (Pi t) sc) (PPi p n' t' sc')
1182− | n == n' = argInfo n p : getUnboundImplicits i sc sc'
1183− where
1184− argInfo n (Imp opt _ _) = (True, PImp (getPriority i t') True opt n t')
1185− argInfo n (Exp opt _ _) = (InaccessibleArg `elem` opt,
1186− PExp (getPriority i t') opt n t')
1187− argInfo n (Constraint opt _) = (InaccessibleArg `elem` opt,
1188− PConstraint 10 opt n t')
1189− argInfo n (TacImp opt _ scr) = (InaccessibleArg `elem` opt,
1190− PTacImplicit 10 opt n scr t')
1191−getUnboundImplicits i (Bind n (Pi t) sc) tm
1192− = impBind n t : getUnboundImplicits i sc tm
1193− where
1194− impBind n t = (True, PImp 1 True [] n Placeholder)
1195−getUnboundImplicits i sc tm = []
1181+getUnboundImplicits i t tm = getImps t (collectImps tm)
1182+ where collectImps (PPi p n t sc)
1183+ = (n, (p, t)) : collectImps sc
1184+ collectImps _ = []
1185+
1186+ getImps (Bind n (Pi t) sc) imps
1187+ | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
1188+ where
1189+ argInfo n (Imp opt _ _) t'
1190+ = (True, PImp (getPriority i t') True opt n t')
1191+ argInfo n (Exp opt _ _) t'
1192+ = (InaccessibleArg `elem` opt,
1193+ PExp (getPriority i t') opt n t')
1194+ argInfo n (Constraint opt _) t'
1195+ = (InaccessibleArg `elem` opt,
1196+ PConstraint 10 opt n t')
1197+ argInfo n (TacImp opt _ scr) t'
1198+ = (InaccessibleArg `elem` opt,
1199+ PTacImplicit 10 opt n scr t')
1200+ getImps (Bind n (Pi t) sc) imps = impBind n t : getImps sc imps
1201+ where impBind n t = (True, PImp 1 True [] n Placeholder)
1202+ getImps sc tm = []
11961203
11971204-- Add implicit Pi bindings for any names in the term which appear in an
11981205-- argument position.