git.iko.soy/Idris-dev
on master help sign in
Merge branch 'unique'
6097efcEdwin Brady
src/Idris/Core/Typecheck.hs+4−13
compare with master
unifiedsplit
@@ -51,17 +51,17 @@ isType ctxt env tm = isType' (normalise ctxt env tm)
51 | otherwise = fail (showEnv env tm ++ " is not a Type")
51 | otherwise = fail (showEnv env tm ++ " is not a Type")
52
52
53recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
53recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
54−recheck = recheck_borrowing []
54+recheck = recheck_borrowing False []
55
55
56−recheck_borrowing :: [Name] -> Context -> Env -> Raw -> Term ->
56+recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->
57 TC (Term, Type, UCs)
57 TC (Term, Type, UCs)
58−recheck_borrowing bs ctxt env tm orig
58+recheck_borrowing uniq_check bs ctxt env tm orig
59 = let v = next_tvar ctxt in
59 = let v = next_tvar ctxt in
60 case runStateT (check' False ctxt env tm) (v, []) of -- holes banned
60 case runStateT (check' False ctxt env tm) (v, []) of -- holes banned
61 Error (IncompleteTerm _) -> Error $ IncompleteTerm orig
61 Error (IncompleteTerm _) -> Error $ IncompleteTerm orig
62 Error e -> Error e
62 Error e -> Error e
63 OK ((tm, ty), constraints) ->
63 OK ((tm, ty), constraints) ->
64− do checkUnique bs ctxt env tm
64+ do when uniq_check $ checkUnique bs ctxt env tm
65 return (tm, ty, constraints)
65 return (tm, ty, constraints)
66
66
67check :: Context -> Env -> Raw -> TC (Term, Type)
67check :: Context -> Env -> Raw -> TC (Term, Type)
@@ -281,20 +281,11 @@ checkUnique borrowed ctxt env tm
281 chkBinders env (App f a) = do chkBinders env f; chkBinders env a
281 chkBinders env (App f a) = do chkBinders env f; chkBinders env a
282 chkBinders env (Bind n b t)
282 chkBinders env (Bind n b t)
283 = do chkBinderName env n b
283 = do chkBinderName env n b
284− -- Must be safe whether we evaluate the scope or binder first
285− -- (Surely there is a tidier rule than this...?)
286 st <- get
284 st <- get
287− chkBinders env (binderTy b)
288 case b of
285 case b of
289 Let t v -> chkBinders env v
286 Let t v -> chkBinders env v
290 _ -> return ()
287 _ -> return ()
291 chkBinders ((n, b) : env) t
288 chkBinders ((n, b) : env) t
292−-- put st
293−-- chkBinders env (binderTy b)
294−-- case b of
295−-- Let t v -> chkBinders env v
296−-- _ -> return ()
297−-- chkBinders ((n, b) : env) t
298 chkBinders env t = return ()
289 chkBinders env t = return ()
299
290
300 chkBinderName :: Env -> Name -> Binder Term ->
291 chkBinderName :: Env -> Name -> Binder Term ->
src/Idris/Elab/Clause.hs+1−1
@@ -600,7 +600,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
600 logLvl 6 $ " ==> " ++ show (forget rhs')
600 logLvl 6 $ " ==> " ++ show (forget rhs')
601
601
602 (crhs, crhsty) <- if not inf
602 (crhs, crhsty) <- if not inf
603− then recheckC_borrowing borrowed fc [] rhs'
603+ then recheckC_borrowing True borrowed fc [] rhs'
604 else return (rhs', clhsty)
604 else return (rhs', clhsty)
605 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
605 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
606 case converts ctxt [] clhsty crhsty of
606 case converts ctxt [] clhsty crhsty of
src/Idris/Elab/Utils.hs+3−3
@@ -21,12 +21,12 @@ import Debug.Trace
21
21
22import qualified Data.Map as Map
22import qualified Data.Map as Map
23
23
24−recheckC = recheckC_borrowing []
24+recheckC = recheckC_borrowing False []
25
25
26−recheckC_borrowing bs fc env t
26+recheckC_borrowing uniq_check bs fc env t
27 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
27 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
28 ctxt <- getContext
28 ctxt <- getContext
29− (tm, ty, cs) <- tclift $ case recheck_borrowing bs ctxt env (forget t) t of
29+ (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of
30 Error e -> tfail (At fc e)
30 Error e -> tfail (At fc e)
31 OK x -> return x
31 OK x -> return x
32 addConstraints fc cs
32 addConstraints fc cs