@@ -53,7 +53,7 @@ isType ctxt env tm = isType' (normalise ctxt env tm)
5353recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
5454recheck = recheck_borrowing False []
5555
56−recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->
56+recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->
5757 TC (Term, Type, UCs)
5858recheck_borrowing uniq_check bs ctxt env tm orig
5959 = let v = next_tvar ctxt in
@@ -65,7 +65,7 @@ recheck_borrowing uniq_check bs ctxt env tm orig
6565 return (tm, ty, constraints)
6666
6767check :: Context -> Env -> Raw -> TC (Term, Type)
68−check ctxt env tm
68+check ctxt env tm
6969 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed
7070
7171check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
@@ -93,12 +93,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
9393 ty@(Bind x (Pi s k) t) -> ty
9494 _ -> normalise ctxt env fty
9595 case fty' of
96− Bind x (Pi s k) t ->
96+ Bind x (Pi s k) t ->
9797 do convertsC ctxt env aty s
9898 let apty = simplify initContext env
9999 (Bind x (Let aty av) t)
100100 return (App fv av, apty)
101− t -> lift $ tfail $ NonFunctionType fv fty
101+ t -> lift $ tfail $ NonFunctionType fv fty
102102 chk u env RType
103103 | holes = return (TType (UVal 0), TType (UVal 0))
104104 | otherwise = do (v, cs) <- get
@@ -135,7 +135,6 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
135135 = do (sv, st) <- chk u env s
136136 (kv, kt) <- chk u env k
137137 (tv, tt) <- chk st ((n, Pi sv kv) : env) t
138−-- let tv = mkUniquePi kv tv_in
139138 (v, cs) <- get
140139 case (normalise ctxt env st, normalise ctxt env tt) of
141140 (TType su, TType tu) -> do
@@ -148,12 +147,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where
148147 return (Bind n (Pi (uniqueBinders (map fst env) sv) k')
149148 (pToV n tv), k')
150149
151− where mkUniquePi kv (Bind n (Pi s k) sc)
150+ where mkUniquePi kv (Bind n (Pi s k) sc)
152151 = let k' = smaller kv k in
153152 Bind n (Pi s k') (mkUniquePi k' sc)
154− mkUniquePi kv (Bind n (Lam t) sc)
153+ mkUniquePi kv (Bind n (Lam t) sc)
155154 = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)
156− mkUniquePi kv (Bind n (Let t v) sc)
155+ mkUniquePi kv (Bind n (Let t v) sc)
157156 = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)
158157 mkUniquePi kv t = t
159158
@@ -257,9 +256,9 @@ data UniqueUse = Never -- no more times
257256-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears
258257-- in the scope more than once, this is an error.
259258checkUnique :: [Name] -> Context -> Env -> Term -> TC ()
260−checkUnique borrowed ctxt env tm
259+checkUnique borrowed ctxt env tm
261260 = evalStateT (chkBinders env (explicitNames tm)) []
262− where
261+ where
263262 isVar (P _ _ _) = True
264263 isVar (V _) = True
265264 isVar _ = False
@@ -272,10 +271,10 @@ checkUnique borrowed ctxt env tm
272271 chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)
273272 | isVar a && owner == txt "Ownership" &&
274273 (lend == txt "lend" || lend == txt "Read")
275− = do chkBinders env t -- Check the type normally
274+ = do chkBinders env t -- Check the type normally
276275 st <- get
277276 -- Remove the 'LendOnly' names from the unusable set
278− put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)
277+ put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)
279278 chkBinders env a
280279 put st -- Reset the old state after checking the argument
281280 chkBinders env (App f a) = do chkBinders env f; chkBinders env a
@@ -288,14 +287,14 @@ checkUnique borrowed ctxt env tm
288287 chkBinders ((n, b) : env) t
289288 chkBinders env t = return ()
290289
291− chkBinderName :: Env -> Name -> Binder Term ->
290+ chkBinderName :: Env -> Name -> Binder Term ->
292291 StateT [(Name, (UniqueUse, Universe))] TC ()
293292 chkBinderName env n b
294293 = do let rawty = forgetEnv (map fst env) (binderTy b)
295294 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?
296295 case kind of
297296 UType UniqueType -> do ns <- get
298− if n `elem` borrowed
297+ if n `elem` borrowed
299298 then put ((n, (LendOnly, NullType)) : ns)
300299 else put ((n, (Once, UniqueType)) : ns)
301300 UType NullType -> do ns <- get
@@ -304,13 +303,12 @@ checkUnique borrowed ctxt env tm
304303 put ((n, (Once, AllTypes)) : ns)
305304 _ -> return ()
306305
307− chkName n
306+ chkName n
308307 = do ns <- get
309308 case lookup n ns of
310309 Nothing -> return ()
311310 Just (Many, k) -> return ()
312311 Just (Never, k) -> lift $ tfail (UniqueError k n)
313312 Just (LendOnly, k) -> lift $ tfail (UniqueError k n)
314− Just (Once, k) -> put ((n, (Never, k)) :
313+ Just (Once, k) -> put ((n, (Never, k)) :
315314 filter (\x -> fst x /= n) ns)
316−