@@ -107,7 +107,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
107107 return (TType (UVar v), TType (UVar (v+1)))
108108 chk u env (RUType un)
109109 | holes = return (UType un, TType (UVal 0))
110− | otherwise = do -- TODO! (v, cs) <- get
110+ | otherwise = do -- TODO! Issue #1715 on the issue tracker.
111+ -- https://github.com/idris-lang/Idris-dev/issues/1715
112+ -- (v, cs) <- get
111113 -- let c = ULT (UVar v) (UVar (v+1))
112114 -- put (v+2, (c:cs))
113115 -- return (TType (UVar v), TType (UVar (v+1)))
@@ -292,6 +294,8 @@ checkUnique borrowed ctxt env tm
292294 chkBinderName env n b
293295 = do let rawty = forgetEnv (map fst env) (binderTy b)
294296 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?
297+ -- Issue #1714 on the issue tracker
298+ -- https://github.com/idris-lang/Idris-dev/issues/1714
295299 case kind of
296300 UType UniqueType -> do ns <- get
297301 if n `elem` borrowed