@@ -1336,7 +1336,7 @@ addUsingImpls syn n fc t
1336 bindFree (n:ns) tm
1336 bindFree (n:ns) tm
1337 | elem n (map iname uimpls) = bindFree ns tm
1337 | elem n (map iname uimpls) = bindFree ns tm
1338 | otherwise
1338 | otherwise
1339− = PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
1339+ = PPi (Imp [InaccessibleArg] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
1341 getArgnames (PPi _ n _ c sc)
1341 getArgnames (PPi _ n _ c sc)
1342 = n : getArgnames sc
1342 = n : getArgnames sc
@@ -1376,8 +1376,9 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)
1376-- argument position.
1376-- argument position.
1378-- This has become a right mess already. Better redo it some time...
1378-- This has become a right mess already. Better redo it some time...
1379−-- TODO: This is obsoleted by the new way of elaborating types, but there's still
1379+-- TODO: This is obsoleted by the new way of elaborating types, (which
1380+-- calls addUsingImpls) but there's still a couple of places which use
1380−-- a couple of places which use it. Clean them up!
1381+-- it. Clean them up!
1382-- Issue 1739 in the issue tracker
1383-- Issue 1739 in the issue tracker
1383-- https://github.com/idris-lang/Idris-dev/issues/1739
1384-- https://github.com/idris-lang/Idris-dev/issues/1739
@@ -1512,9 +1513,10 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
1512 pibind using [] sc = sc
1513 pibind using [] sc = sc
1513 pibind using (n:ns) sc
1514 pibind using (n:ns) sc
1514 = case lookup n using of
1515 = case lookup n using of
1515− Just ty -> PPi (Imp [] Dynamic False Nothing) n NoFC ty (pibind using ns sc)
1516+ Just ty -> PPi (Imp [] Dynamic False Nothing)
1517+ n NoFC ty (pibind using ns sc)
1516− Nothing -> PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder
1518+ Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)
1517− (pibind using ns sc)
1519+ n NoFC Placeholder (pibind using ns sc)
1519-- Add implicit arguments in function calls
1521-- Add implicit arguments in function calls
1520addImplPat :: IState -> PTerm -> PTerm
1522addImplPat :: IState -> PTerm -> PTerm
@@ -2091,9 +2093,8 @@ shadow n n' t = sm t where
2091 sm (PNoImplicits x) = PNoImplicits (sm x)
2093 sm (PNoImplicits x) = PNoImplicits (sm x)
2092 sm x = x
2094 sm x = x
2094−-- Rename any binders which are repeated (so that we don't have to mess
2096+-- | Rename any binders which are repeated (so that we don't have to mess
2095-- about with shadowing anywhere else).
2097-- about with shadowing anywhere else).
2097mkUniqueNames :: [Name] -> PTerm -> PTerm
2098mkUniqueNames :: [Name] -> PTerm -> PTerm
2098mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2099mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
2099 inScope :: S.Set Name
2100 inScope :: S.Set Name