@@ -755,14 +755,14 @@ allNamesIn tm = nub $ ni [] tm
755755 ni env (PAlternative ls) = concatMap (ni env) ls
756756 ni env _ = []
757757
758−namesIn :: IState -> PTerm -> [Name]
759−namesIn ist tm = nub $ ni [] tm
758+namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
759+namesIn uvars ist tm = nub $ ni [] tm
760760 where
761761 ni env (PRef _ n)
762762 | not (n `elem` env)
763763 = case lookupTy Nothing n (tt_ctxt ist) of
764764 [] -> [n]
765− _ -> []
765+ _ -> if n `elem` (map fst uvars) then [n] else []
766766 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
767767 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
768768 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
@@ -911,7 +911,7 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)
911911 where
912912 expandParamsC (PClause n lhs ws rhs ds)
913913 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
914− ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
914+ ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
915915 n' = if n `elem` ns then dec n else n in
916916 PClause n' (expandParams dec ps'' ns lhs)
917917 (map (expandParams dec ps'' ns) ws)
@@ -919,7 +919,7 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)
919919 (map (expandParamsD ist dec ps'' ns) ds)
920920 expandParamsC (PWith n lhs ws wval ds)
921921 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
922− ps'' = updateps False (namesIn ist lhs) (zip ps [0..])
922+ ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
923923 n' = if n `elem` ns then dec n else n in
924924 PWith n' (expandParams dec ps'' ns lhs)
925925 (map (expandParams dec ps'' ns) ws)
@@ -983,39 +983,40 @@ implicit syn n ptm
983983
984984implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])
985985implicitise syn ist tm
986− = let uvars = using syn
987− pvars = syn_params syn
988− (declimps, ns') = execState (imps True [] tm) ([], [])
986+ = let (declimps, ns') = execState (imps True [] tm) ([], [])
989987 ns = ns' \\ (map fst pvars ++ no_imp syn) in
990988 if null ns
991989 then (tm, reverse declimps)
992990 else implicitise syn ist (pibind uvars ns tm)
993991 where
992+ uvars = using syn
993+ pvars = syn_params syn
994+
994995 dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
995996 | otherwise = x : dropAll xs ys
996997 dropAll [] ys = []
997998
998999 imps top env (PApp _ f as)
9991000 = do (decls, ns) <- get
1000− let isn = concatMap (namesIn ist) (map getTm as)
1001+ let isn = concatMap (namesIn uvars ist) (map getTm as)
10011002 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10021003 imps top env (PPi (Imp l _) n ty sc)
1003− = do let isn = nub (namesIn ist ty) `dropAll` [n]
1004+ = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
10041005 (decls , ns) <- get
10051006 put (PImp (getPriority ist ty) l n ty : decls,
10061007 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10071008 imps True (n:env) sc
10081009 imps top env (PPi (Exp l _) n ty sc)
1009− = do let isn = nub (namesIn ist ty ++ case sc of
1010− (PRef _ x) -> namesIn ist sc `dropAll` [n]
1010+ = do let isn = nub (namesIn uvars ist ty ++ case sc of
1011+ (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
10111012 _ -> [])
10121013 (decls, ns) <- get -- ignore decls in HO types
10131014 put (PExp (getPriority ist ty) l ty : decls,
10141015 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10151016 imps True (n:env) sc
10161017 imps top env (PPi (Constraint l _) n ty sc)
1017− = do let isn = nub (namesIn ist ty ++ case sc of
1018− (PRef _ x) -> namesIn ist sc `dropAll` [n]
1018+ = do let isn = nub (namesIn uvars ist ty ++ case sc of
1019+ (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
10191020 _ -> [])
10201021 (decls, ns) <- get -- ignore decls in HO types
10211022 put (PConstraint 10 l ty : decls,
@@ -1023,23 +1024,24 @@ implicitise syn ist tm
10231024 imps True (n:env) sc
10241025 imps top env (PEq _ l r)
10251026 = do (decls, ns) <- get
1026− let isn = namesIn ist l ++ namesIn ist r
1027+ let isn = namesIn uvars ist l ++ namesIn uvars ist r
10271028 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10281029 imps top env (PPair _ l r)
10291030 = do (decls, ns) <- get
1030− let isn = namesIn ist l ++ namesIn ist r
1031+ let isn = namesIn uvars ist l ++ namesIn uvars ist r
10311032 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10321033 imps top env (PDPair _ (PRef _ n) t r)
10331034 = do (decls, ns) <- get
1034− let isn = nub (namesIn ist t ++ namesIn ist r) \\ [n]
1035+ let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
10351036 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
10361037 imps top env (PDPair _ l t r)
10371038 = do (decls, ns) <- get
1038− let isn = namesIn ist l ++ namesIn ist t ++ namesIn ist r
1039+ let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
1040+ namesIn uvars ist r
10391041 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
10401042 imps top env (PAlternative as)
10411043 = do (decls, ns) <- get
1042− let isn = concatMap (namesIn ist) as
1044+ let isn = concatMap (namesIn uvars ist) as
10431045 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
10441046 imps top env (PLam n ty sc)
10451047 = do imps False env ty
@@ -1149,9 +1151,9 @@ findStatics ist tm = let (ns, ss) = fs tm in
11491151 where fs (PPi p n t sc)
11501152 | Static <- pstatic p
11511153 = let (ns, ss) = fs sc in
1152− (namesIn ist t : ns, namesIn ist t ++ n : ss)
1154+ (namesIn [] ist t : ns, namesIn [] ist t ++ n : ss)
11531155 | otherwise = let (ns, ss) = fs sc in
1154− (namesIn ist t : ns, ss)
1156+ (namesIn [] ist t : ns, ss)
11551157 fs _ = ([], [])
11561158
11571159 inOne n ns = length (filter id (map (elem n) ns)) == 1