b591600 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't propagate unique names to 'where'

Doing so breaks typechecking, leading to nothing working any more... passing them to lifted 'where' definitions counts as a use in the typechecker, so *any* where clause will fail to typecheck. This is an effect of how 'where' clauses are elaborated, and is probably not the best behaviour (though it is better than the default which rules our where clauses completely) so we should revisit it later if uniqueness typing turns out to work effectively.

commitb591600d12e62ea0c38e6c7e37edca0a43257e9c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 26 Aug 2014, 09:25 (12 years ago) parentbe7bbd7

2 files changed+23−4

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+20−1 test/unique002/unique002.idr+3−3

src/Idris/Elab/Clause.hs+20−1

@@ -442,6 +442,18 @@ propagateParams i ps t (PRef fc n)

442442 isImplicit (_ : is) n = isImplicit is n

443443propagateParams i ps t x = x

444444

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+

445457-- Return the elaborated LHS/RHS, and the original LHS with implicits added

446458elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

447459 Idris (Either Term (Term, Term), PTerm)

@@ -520,7 +532,14 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

520532 windex <- getName

521533 let decls = nub (concatMap declared whereblock)

522534 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+

524543 let winfo = pinfo info newargs defs windex

525544 let wb = map (expandParamsD False ist decorate newargs defs) whereblock

526545

test/unique002/unique002.idr+3−3

@@ -14,7 +14,7 @@ showU xs = "[" ++ showU' xs ++ "]" where

1414foo : UList Int -> IO ()

1515foo xs = do -- let f = \x : Int => showU xs

1616 putStrLn $ free xs

17− putStrLn $ f 42

17+ putStrLn $ f 42 xs

1818 return ()

19− where f : Int -> String

20− f x = showU xs

19+ where f : Int -> Borrowed (UList Int) -> String

20+ f x xs = showU xs