git.iko.soy/Idris-dev
on master help sign in
Don't propagate unique names to 'where'
b591600Edwin Brady
src/Idris/Elab/Clause.hs+20−1
compare with master
unifiedsplit
@@ -442,6 +442,18 @@ propagateParams i ps t (PRef fc n)
442 isImplicit (_ : is) n = isImplicit is n
442 isImplicit (_ : is) n = isImplicit is n
443propagateParams i ps t x = x
443propagateParams i ps t x = x
444
444
445+findUnique :: Context -> Env -> Term -> [Name]
446+findUnique ctxt env (Bind n b sc)
447+ = let rawTy = forgetEnv (map fst env) (binderTy b)
448+ uniq = case check ctxt env rawTy of
449+ OK (_, UType UniqueType) -> True
450+ OK (_, UType NullType) -> True
451+ OK (_, UType AllTypes) -> True
452+ _ -> False in
453+ if uniq then n : findUnique ctxt ((n, b) : env) sc
454+ else findUnique ctxt ((n, b) : env) sc
455+findUnique _ _ _ = []
456+
445-- Return the elaborated LHS/RHS, and the original LHS with implicits added
457-- Return the elaborated LHS/RHS, and the original LHS with implicits added
446elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
458elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
447 Idris (Either Term (Term, Term), PTerm)
459 Idris (Either Term (Term, Term), PTerm)
@@ -520,7 +532,14 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
520 windex <- getName
532 windex <- getName
521 let decls = nub (concatMap declared whereblock)
533 let decls = nub (concatMap declared whereblock)
522 let defs = nub (decls ++ concatMap defined whereblock)
534 let defs = nub (decls ++ concatMap defined whereblock)
523− let newargs = pvars ist lhs_tm
535+ let newargs_all = pvars ist lhs_tm
536+
537+ -- Unique arguments must be passed to the where block explicitly
538+ -- (since we can't control "usage" easlily otherwise). Remove them
539+ -- from newargs here
540+ let uniqargs = findUnique (tt_ctxt ist) [] lhs_tm
541+ let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all
542+
524 let winfo = pinfo info newargs defs windex
543 let winfo = pinfo info newargs defs windex
525 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
544 let wb = map (expandParamsD False ist decorate newargs defs) whereblock
526
545
test/unique002/unique002.idr+3−3
@@ -14,7 +14,7 @@ showU xs = "[" ++ showU' xs ++ "]" where
14foo : UList Int -> IO ()
14foo : UList Int -> IO ()
15foo xs = do -- let f = \x : Int => showU xs
15foo xs = do -- let f = \x : Int => showU xs
16 putStrLn $ free xs
16 putStrLn $ free xs
17− putStrLn $ f 42
17+ putStrLn $ f 42 xs
18 return ()
18 return ()
19− where f : Int -> String
19+ where f : Int -> Borrowed (UList Int) -> String
20− f x = showU xs
20+ f x xs = showU xs