git.iko.soy/Idris-dev
on master help sign in
No need to check LHS for unique usage
e1a2cf8Edwin Brady
src/Idris/Core/Typecheck.hs+4−4
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)
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