@@ -1336,7 +1336,7 @@ addUsingImpls syn n fc t
13361336 bindFree (n:ns) tm
13371337 | elem n (map iname uimpls) = bindFree ns tm
13381338 | 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)
13401340
13411341 getArgnames (PPi _ n _ c sc)
13421342 = n : getArgnames sc
@@ -1376,8 +1376,9 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)
13761376-- argument position.
13771377
13781378-- 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
1380−-- a couple of places which use it. Clean them up!
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
1381+-- it. Clean them up!
13811382--
13821383-- Issue 1739 in the issue tracker
13831384-- https://github.com/idris-lang/Idris-dev/issues/1739
@@ -1512,9 +1513,10 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
15121513 pibind using [] sc = sc
15131514 pibind using (n:ns) sc
15141515 = case lookup n using of
1515− Just ty -> PPi (Imp [] Dynamic False Nothing) n NoFC ty (pibind using ns sc)
1516− Nothing -> PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder
1517− (pibind using ns sc)
1516+ Just ty -> PPi (Imp [] Dynamic False Nothing)
1517+ n NoFC ty (pibind using ns sc)
1518+ Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)
1519+ n NoFC Placeholder (pibind using ns sc)
15181520
15191521-- Add implicit arguments in function calls
15201522addImplPat :: IState -> PTerm -> PTerm
@@ -2091,9 +2093,8 @@ shadow n n' t = sm t where
20912093 sm (PNoImplicits x) = PNoImplicits (sm x)
20922094 sm x = x
20932095
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
20952097-- about with shadowing anywhere else).
2096−
20972098mkUniqueNames :: [Name] -> PTerm -> PTerm
20982099mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
20992100 inScope :: S.Set Name