@@ -107,7 +107,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
107 return (TType (UVar v), TType (UVar (v+1)))
107 return (TType (UVar v), TType (UVar (v+1)))
108 chk u env (RUType un)
108 chk u env (RUType un)
109 | holes = return (UType un, TType (UVal 0))
109 | 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
111 -- let c = ULT (UVar v) (UVar (v+1))
113 -- let c = ULT (UVar v) (UVar (v+1))
112 -- put (v+2, (c:cs))
114 -- put (v+2, (c:cs))
113 -- return (TType (UVar v), TType (UVar (v+1)))
115 -- return (TType (UVar v), TType (UVar (v+1)))
@@ -292,6 +294,8 @@ checkUnique borrowed ctxt env tm
292 chkBinderName env n b
294 chkBinderName env n b
293 = do let rawty = forgetEnv (map fst env) (binderTy b)
295 = do let rawty = forgetEnv (map fst env) (binderTy b)
294 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?
296 (_, 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
295 case kind of
299 case kind of
296 UType UniqueType -> do ns <- get
300 UType UniqueType -> do ns <- get
297 if n `elem` borrowed
301 if n `elem` borrowed