@@ -69,7 +69,7 @@ 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)
72−check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
72+check' holes ctxt env top = chk (TType (UVar (-5))) env top where
7373
7474 smaller (UType NullType) _ = UType NullType
7575 smaller _ (UType NullType) = UType NullType
@@ -78,18 +78,17 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
7878 smaller x _ = x
7979
8080 chk :: Type -> -- uniqueness level
81− Maybe UExp -> -- maximum universe level, if known
8281 Env -> Raw -> StateT UCs TC (Term, Type)
83− chk u maxu env (Var n)
82+ chk u env (Var n)
8483 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
8584 -- If we're elaborating, we don't want the private names; if we're
8685 -- checking an already elaborated term, we do
8786 | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt
8887 = return (P nt n' ty, ty)
8988 | otherwise = do lift $ tfail $ NoSuchVariable n
90− chk u maxu env ap@(RApp f RType) | not holes
89+ chk u env ap@(RApp f RType) | not holes
9190 -- special case to reduce constraintss
92− = do (fv, fty) <- chk u maxu env f
91+ = do (fv, fty) <- chk u env f
9392 let fty' = case uniqueBinders (map fst env) (finalise fty) of
9493 ty@(Bind x (Pi i s k) t) -> ty
9594 _ -> uniqueBinders (map fst env)
@@ -104,21 +103,21 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
104103 (Bind x (Let (TType v') (TType (UVar v))) t)
105104 return (App fv (TType (UVar v)), apty)
106105 Bind x (Pi i s k) t ->
107− do (av, aty) <- chk u maxu env RType
106+ do (av, aty) <- chk u env RType
108107 convertsC ctxt env aty s
109108 let apty = simplify initContext env
110109 (Bind x (Let aty av) t)
111110 return (App fv av, apty)
112111 t -> lift $ tfail $ NonFunctionType fv fty
113− chk u maxu env ap@(RApp f a)
114− = do (fv, fty) <- chk u maxu env f
112+ chk u env ap@(RApp f a)
113+ = do (fv, fty) <- chk u env f
115114 let fty' = case uniqueBinders (map fst env) (finalise fty) of
116115 ty@(Bind x (Pi i s k) t) -> ty
117116 _ -> uniqueBinders (map fst env)
118117 $ case hnf ctxt env fty of
119118 ty@(Bind x (Pi i s k) t) -> ty
120119 _ -> normalise ctxt env fty
121− (av, aty) <- chk u maxu env a
120+ (av, aty) <- chk u env a
122121 case fty' of
123122 Bind x (Pi i s k) t ->
124123 do convertsC ctxt env aty s
@@ -126,13 +125,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
126125 (Bind x (Let aty av) t)
127126 return (App fv av, apty)
128127 t -> lift $ tfail $ NonFunctionType fv fty
129− chk u maxu env RType
128+ chk u env RType
130129 | holes = return (TType (UVal 0), TType (UVal 0))
131130 | otherwise = do (v, cs) <- get
132131 let c = ULT (UVar v) (UVar (v+1))
133132 put (v+2, (c:cs))
134133 return (TType (UVar v), TType (UVar (v+1)))
135− chk u maxu env (RUType un)
134+ chk u env (RUType un)
136135 | holes = return (UType un, TType (UVal 0))
137136 | otherwise = do -- TODO! Issue #1715 on the issue tracker.
138137 -- https://github.com/idris-lang/Idris-dev/issues/1715
@@ -141,8 +140,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
141140 -- put (v+2, (c:cs))
142141 -- return (TType (UVar v), TType (UVar (v+1)))
143142 return (UType un, TType (UVal 0))
144− chk u maxu env (RConstant Forgot) = return (Erased, Erased)
145− chk u maxu env (RConstant c) = return (Constant c, constType c)
143+ chk u env (RConstant Forgot) = return (Erased, Erased)
144+ chk u env (RConstant c) = return (Constant c, constType c)
146145 where constType (I _) = Constant (AType (ATInt ITNative))
147146 constType (BI _) = Constant (AType (ATInt ITBig))
148147 constType (Fl _) = Constant (AType ATFloat)
@@ -159,24 +158,21 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
159158 constType TheWorld = Constant WorldType
160159 constType Forgot = Erased
161160 constType _ = TType (UVal 0)
162− chk u maxu env (RForce t) = do (_, ty) <- chk u maxu env t
163− return (Erased, ty)
164− chk u maxu env (RBind n (Pi i s k) t)
165− = do (sv, st) <- chk u Nothing env s
166− vcs <- get
167− (kv, kt) <- chk u Nothing env k
168− put vcs -- no need to validate these constraints, they are independent
161+ chk u env (RForce t)
162+ = do (_, ty) <- chk u env t
163+ return (Erased, ty)
164+ chk u env (RBind n (Pi i s k) t)
165+ = do (sv, st) <- chk u env s
169166 (v, cs) <- get
170− nmaxu <- case maxu of
171− Nothing -> do put (v+1, cs)
172− return (UVar v)
173− Just m -> return m
174− (tv, tt) <- chk st (Just nmaxu) ((n, Pi i sv kv) : env) t
167+ (kv, kt) <- chk u env k -- no need to validate these constraints, they are independent
168+ put (v+1, cs)
169+ let maxu = UVar v
170+ (tv, tt) <- chk st ((n, Pi i sv kv) : env) t
175171 case (normalise ctxt env st, normalise ctxt env tt) of
176172 (TType su, TType tu) -> do
177173 when (not holes) $ do (v, cs) <- get
178− put (v, ULE su nmaxu :
179− ULE tu nmaxu : cs)
174+ put (v, ULE su maxu :
175+ ULE tu maxu : cs)
180176 let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u
181177 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')
182178 (pToV n tv), k')
@@ -200,27 +196,27 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
200196 mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)
201197 mostUnique (_ : es) k = mostUnique es k
202198
203− chk u maxu env (RBind n b sc)
199+ chk u env (RBind n b sc)
204200 = do (b', bt') <- checkBinder b
205− (scv, sct) <- chk (smaller bt' u) maxu ((n, b'):env) sc
201+ (scv, sct) <- chk (smaller bt' u) ((n, b'):env) sc
206202 discharge n b' bt' (pToV n scv) (pToV n sct)
207203 where checkBinder (Lam t)
208− = do (tv, tt) <- chk u maxu env t
204+ = do (tv, tt) <- chk u env t
209205 let tv' = normalise ctxt env tv
210206 let tt' = normalise ctxt env tt
211207 lift $ isType ctxt env tt'
212208 return (Lam tv, tt')
213209 checkBinder (Let t v)
214− = do (tv, tt) <- chk u maxu env t
215− (vv, vt) <- chk u maxu env v
210+ = do (tv, tt) <- chk u env t
211+ (vv, vt) <- chk u env v
216212 let tv' = normalise ctxt env tv
217213 let tt' = normalise ctxt env tt
218214 convertsC ctxt env vt tv
219215 lift $ isType ctxt env tt'
220216 return (Let tv vv, tt')
221217 checkBinder (NLet t v)
222− = do (tv, tt) <- chk u maxu env t
223− (vv, vt) <- chk u maxu env v
218+ = do (tv, tt) <- chk u env t
219+ (vv, vt) <- chk u env v
224220 let tv' = normalise ctxt env tv
225221 let tt' = normalise ctxt env tt
226222 convertsC ctxt env vt tv
@@ -229,13 +225,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
229225 checkBinder (Hole t)
230226 | not holes = lift $ tfail (IncompleteTerm undefined)
231227 | otherwise
232− = do (tv, tt) <- chk u maxu env t
228+ = do (tv, tt) <- chk u env t
233229 let tv' = normalise ctxt env tv
234230 let tt' = normalise ctxt env tt
235231 lift $ isType ctxt env tt'
236232 return (Hole tv, tt')
237233 checkBinder (GHole i t)
238− = do (tv, tt) <- chk u maxu env t
234+ = do (tv, tt) <- chk u env t
239235 let tv' = normalise ctxt env tv
240236 let tt' = normalise ctxt env tt
241237 lift $ isType ctxt env tt'
@@ -243,15 +239,15 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
243239 checkBinder (Guess t v)
244240 | not holes = lift $ tfail (IncompleteTerm undefined)
245241 | otherwise
246− = do (tv, tt) <- chk u maxu env t
247− (vv, vt) <- chk u maxu env v
242+ = do (tv, tt) <- chk u env t
243+ (vv, vt) <- chk u env v
248244 let tv' = normalise ctxt env tv
249245 let tt' = normalise ctxt env tt
250246 convertsC ctxt env vt tv
251247 lift $ isType ctxt env tt'
252248 return (Guess tv vv, tt')
253249 checkBinder (PVar t)
254− = do (tv, tt) <- chk u maxu env t
250+ = do (tv, tt) <- chk u env t
255251 let tv' = normalise ctxt env tv
256252 let tt' = normalise ctxt env tt
257253 lift $ isType ctxt env tt'
@@ -259,7 +255,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where
259255 -- to tell if it's a collapsible variable)
260256 return (PVar tv, tt')
261257 checkBinder (PVTy t)
262− = do (tv, tt) <- chk u maxu env t
258+ = do (tv, tt) <- chk u env t
263259 let tv' = normalise ctxt env tv
264260 let tt' = normalise ctxt env tt
265261 lift $ isType ctxt env tt'