@@ -86,7 +86,10 @@ check ctxt env tm
8686 = evalStateT (check' True [] ctxt env tm) (0, [])
8787
8888check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
89−check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top where
89+check' holes tcns ctxt env top
90+ = do (tm, ty, _) <- chk Rig1 (TType (UVar tcns (-5))) Nothing env top
91+ return (tm, ty)
92+ where
9093
9194 smaller (UType NullType) _ = UType NullType
9295 smaller _ (UType NullType) = UType NullType
@@ -97,22 +100,33 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh
97100 astate | holes = MaybeHoles
98101 | otherwise = Complete
99102
100− chk :: Type -> -- uniqueness level
103+ chk :: RigCount -> -- multiplicity (need enough in context to produce this many of the term)
104+ Type -> -- uniqueness level
101105 Maybe UExp -> -- universe for kind
102− Env -> Raw -> StateT UCs TC (Term, Type)
103− chk u lvl env (Var n)
104− | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
106+ Env -> Raw -> StateT UCs TC (Term, Type, [Name])
107+ chk rigc u lvl env (Var n)
108+ | Just (i, erig, ty) <- lookupTyEnv n env
109+ = case rigSafe holes erig rigc n of
110+ Nothing -> return (P Bound n ty, ty, used rigc n)
111+ Just msg -> lift $ tfail $ Msg msg
105112 -- If we're elaborating, we don't want the private names; if we're
106113 -- checking an already elaborated term, we do
107114 | [P nt n' ty] <- lookupP_all (not holes) False n ctxt
108− = return (P nt n' ty, ty)
115+ = return (P nt n' ty, ty, [])
109116 -- If the names are ambiguous, require it to be fully qualified
110117 | [P nt n' ty] <- lookupP_all (not holes) True n ctxt
111− = return (P nt n' ty, ty)
118+ = return (P nt n' ty, ty, [])
112119 | otherwise = do lift $ tfail $ NoSuchVariable n
113− chk u lvl env ap@(RApp f RType) | not holes
120+ where rigSafe True _ _ n = Nothing
121+ rigSafe _ Rig1 RigW n = Just ("Trying to use linear name " ++ show n ++ " in non-linear context")
122+ rigSafe _ _ _ n = Nothing
123+
124+ used Rig0 n = []
125+ used _ n = [n]
126+
127+ chk rigc u lvl env ap@(RApp f RType) | not holes
114128 -- special case to reduce constraintss
115− = do (fv, fty) <- chk u Nothing env f
129+ = do (fv, fty, fns) <- chk rigc u Nothing env f
116130 let fty' = case uniqueBinders (map fstEnv env) (finalise fty) of
117131 ty@(Bind x (Pi _ i s k) t) -> ty
118132 _ -> uniqueBinders (map fstEnv env)
@@ -125,47 +139,49 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh
125139 put (v+1, ULT (UVar tcns v) v' : cs)
126140 let apty = simplify initContext env
127141 (Bind x (Let (TType v') (TType (UVar tcns v))) t)
128− return (App Complete fv (TType (UVar tcns v)), apty)
142+ return (App Complete fv (TType (UVar tcns v)), apty, fns)
129143 Bind x (Pi rig i s k) t ->
130− do (av, aty) <- chk u Nothing env RType
144+ do (av, aty, _) <- chk rigc u Nothing env RType
131145 convertsC ctxt env aty s
132146 let apty = simplify initContext env
133147 (Bind x (Let aty av) t)
134− return (App astate fv av, apty)
148+ return (App astate fv av, apty, fns)
135149 t -> lift $ tfail $ NonFunctionType fv fty
136− chk u lvl env ap@(RApp f a)
137− = do (fv, fty) <- chk u Nothing env f
138− let fty' = case uniqueBinders (map fstEnv env) (finalise fty) of
139− ty@(Bind x (Pi rig i s k) t) -> ty
140− _ -> uniqueBinders (map fstEnv env)
141− $ case normalise ctxt env fty of
142− ty@(Bind x (Pi rig i s k) t) -> ty
143− _ -> normalise ctxt env fty
144− (av, aty) <- chk u Nothing env a
150+ chk rigc u lvl env ap@(RApp f a)
151+ = do (fv, fty, fns) <- chk rigc u Nothing env f
152+ let (rigf, fty') =
153+ case uniqueBinders (map fstEnv env) (finalise fty) of
154+ ty@(Bind x (Pi rig i s k) t) -> (rig, ty)
155+ _ -> case normalise ctxt env fty of
156+ ty@(Bind x (Pi rig i s k) t) ->
157+ (rig, uniqueBinders (map fstEnv env) ty)
158+ _ -> (RigW, uniqueBinders (map fstEnv env)
159+ (normalise ctxt env fty)) -- This is an error, caught below...
160+ (av, aty, ans) <- chk (rigMult rigc rigf) u Nothing env a
145161 case fty' of
146162 Bind x (Pi rig i s k) t ->
147163 do convertsC ctxt env aty s
148164 let apty = simplify initContext env
149165 (Bind x (Let aty av) t)
150− return (App astate fv av, apty)
166+ return (App astate fv av, apty, fns ++ ans)
151167 t -> lift $ tfail $ NonFunctionType fv fty
152− chk u lvl env RType
153− | holes = return (TType (UVal 0), TType (UVal 0))
168+ chk rigc u lvl env RType
169+ | holes = return (TType (UVal 0), TType (UVal 0), [])
154170 | otherwise = do (v, cs) <- get
155171 let c = ULT (UVar tcns v) (UVar tcns (v+1))
156172 put (v+2, (c:cs))
157− return (TType (UVar tcns v), TType (UVar tcns (v+1)))
158− chk u lvl env (RUType un)
159− | holes = return (UType un, TType (UVal 0))
173+ return (TType (UVar tcns v), TType (UVar tcns (v+1)), [])
174+ chk rigc u lvl env (RUType un)
175+ | holes = return (UType un, TType (UVal 0), [])
160176 | otherwise = do -- TODO! Issue #1715 on the issue tracker.
161177 -- https://github.com/idris-lang/Idris-dev/issues/1715
162178 -- (v, cs) <- get
163179 -- let c = ULT (UVar v) (UVar (v+1))
164180 -- put (v+2, (c:cs))
165181 -- return (TType (UVar v), TType (UVar (v+1)))
166− return (UType un, TType (UVal 0))
167− chk u lvl env (RConstant Forgot) = return (Erased, Erased)
168− chk u lvl env (RConstant c) = return (Constant c, constType c)
182+ return (UType un, TType (UVal 0), [])
183+ chk rigc u lvl env (RConstant Forgot) = return (Erased, Erased, [])
184+ chk rigc u lvl env (RConstant c) = return (Constant c, constType c, [])
169185 where constType (I _) = Constant (AType (ATInt ITNative))
170186 constType (BI _) = Constant (AType (ATInt ITBig))
171187 constType (Fl _) = Constant (AType ATFloat)
@@ -178,15 +194,15 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh
178194 constType TheWorld = Constant WorldType
179195 constType Forgot = Erased
180196 constType _ = TType (UVal 0)
181− chk u lvl env (RBind n (Pi rig i s k) t)
182− = do (sv, st) <- chk u Nothing env s
197+ chk rigc u lvl env (RBind n (Pi rig i s k) t)
198+ = do (sv, st, sns) <- chk Rig0 u Nothing (envZero env) s
183199 (v, cs) <- get
184− (kv, kt) <- chk u Nothing env k -- no need to validate these constraints, they are independent
200+ (kv, kt, _) <- chk Rig0 u Nothing (envZero env) k -- no need to validate these constraints, they are independent
185201 put (v+1, cs)
186202 let maxu = case lvl of
187203 Nothing -> UVar tcns v
188204 Just v' -> v'
189− (tv, tt) <- chk st (Just maxu) ((n, rig, Pi rig i sv kv) : env) t
205+ (tv, tt, tns) <- chk Rig0 st (Just maxu) ((n, Rig0, Pi Rig0 i sv kv) : envZero env) t
190206
191207-- convertsC ctxt env st (TType maxu)
192208-- convertsC ctxt env tt (TType maxu)
@@ -201,11 +217,11 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh
201217 ULE tu maxu : cs)
202218 let k' = TType (UVar tcns v) `smaller` st `smaller` kv `smaller` u
203219 return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')
204− (pToV n tv), k')
220+ (pToV n tv), k', sns ++ tns)
205221 (un, un') ->
206222 let k' = st `smaller` kv `smaller` un `smaller` un' `smaller` u in
207223 return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')
208− (pToV n tv), k')
224+ (pToV n tv), k', sns ++ tns)
209225
210226 where mkUniquePi kv (Bind n (Pi rig i s k) sc)
211227 = let k' = smaller kv k in
@@ -222,85 +238,96 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh
222238 mostUnique (Pi _ _ _ pk : es) k = mostUnique es (smaller pk k)
223239 mostUnique (_ : es) k = mostUnique es k
224240
225− chk u lvl env (RBind n b sc)
226− = do (b', bt') <- checkBinder b
227− (scv, sct) <- chk (smaller bt' u) Nothing ((n, getCount b, b'):env) sc
228− discharge n b' bt' (pToV n scv) (pToV n sct)
229− where getCount (Pi rig _ _ _) = rig
230− getCount (PVar rig _) = rig
231− getCount _ = Rig0
232−
241+ chk rigc u lvl env (RBind n b sc)
242+ = do (b', bt', bns) <- checkBinder b
243+ (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc
244+ checkUsageOK (getCount b) scns
245+ discharge n b' bt' (pToV n scv) (pToV n sct) (bns ++ scns)
246+ where getCount (Pi rig _ _ _) = rigMult rigc rig
247+ getCount (PVar rig _) = rigMult rigc rig
248+ getCount _ = rigMult rigc RigW
249+
250+ checkUsageOK Rig0 _ = return ()
251+ checkUsageOK RigW _ = return ()
252+ checkUsageOK Rig1 ns
253+ = let used = length (filter (==n) ns) in
254+ if used == 1 then return ()
255+ else lift $ tfail $ Msg $ "There are " ++ (show used) ++
256+ " uses of linear name " ++ show n
257+
233258 checkBinder (Lam t)
234− = do (tv, tt) <- chk u Nothing env t
259+ = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
235260 let tv' = normalise ctxt env tv
236261 convType tcns ctxt env tt
237− return (Lam tv, tt)
262+ return (Lam tv, tt, [])
238263 checkBinder (Let t v)
239− = do (tv, tt) <- chk u Nothing env t
240− (vv, vt) <- chk u Nothing env v
264+ = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
265+ -- May have multiple uses, check at RigW.
266+ -- (Consider: adding a single use let?)
267+ (vv, vt, vns) <- chk RigW u Nothing env v
241268 let tv' = normalise ctxt env tv
242269 convertsC ctxt env vt tv
243270 convType tcns ctxt env tt
244− return (Let tv vv, tt)
271+ return (Let tv vv, tt, vns)
245272 checkBinder (NLet t v)
246− = do (tv, tt) <- chk u Nothing env t
247− (vv, vt) <- chk u Nothing env v
273+ = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
274+ (vv, vt, vns) <- chk rigc u Nothing env v
248275 let tv' = normalise ctxt env tv
249276 convertsC ctxt env vt tv
250277 convType tcns ctxt env tt
251− return (NLet tv vv, tt)
278+ return (NLet tv vv, tt, vns)
252279 checkBinder (Hole t)
253280 | not holes = lift $ tfail (IncompleteTerm undefined)
254281 | otherwise
255− = do (tv, tt) <- chk u Nothing env t
282+ = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
256283 let tv' = normalise ctxt env tv
257284 convType tcns ctxt env tt
258− return (Hole tv, tt)
285+ return (Hole tv, tt, [])
259286 checkBinder (GHole i ns t)
260− = do (tv, tt) <- chk u Nothing env t
287+ = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
261288 let tv' = normalise ctxt env tv
262289 convType tcns ctxt env tt
263− return (GHole i ns tv, tt)
290+ return (GHole i ns tv, tt, [])
264291 checkBinder (Guess t v)
265292 | not holes = lift $ tfail (IncompleteTerm undefined)
266293 | otherwise
267− = do (tv, tt) <- chk u Nothing env t
268− (vv, vt) <- chk u Nothing env v
294+ = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
295+ (vv, vt, vns) <- chk rigc u Nothing env v
269296 let tv' = normalise ctxt env tv
270297 convertsC ctxt env vt tv
271298 convType tcns ctxt env tt
272− return (Guess tv vv, tt)
299+ return (Guess tv vv, tt, vns)
273300 checkBinder (PVar rig t)
274− = do (tv, tt) <- chk u Nothing env t
301+ = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
275302 let tv' = normalise ctxt env tv
276303 convType tcns ctxt env tt
277304 -- Normalised version, for erasure purposes (it's easier
278305 -- to tell if it's a collapsible variable)
279− return (PVar rig tv, tt)
306+ return (PVar rig tv, tt, [])
280307 checkBinder (PVTy t)
281− = do (tv, tt) <- chk u Nothing env t
308+ = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
282309 let tv' = normalise ctxt env tv
283310 convType tcns ctxt env tt
284− return (PVTy tv, tt)
285−
286− discharge n (Lam t) bt scv sct
287− = return (Bind n (Lam t) scv, Bind n (Pi RigW Nothing t bt) sct)
288− discharge n (Pi r i t k) bt scv sct
289− = return (Bind n (Pi r i t k) scv, sct)
290− discharge n (Let t v) bt scv sct
291− = return (Bind n (Let t v) scv, Bind n (Let t v) sct)
292− discharge n (NLet t v) bt scv sct
293− = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
294− discharge n (Hole t) bt scv sct
295− = return (Bind n (Hole t) scv, sct)
296− discharge n (GHole i ns t) bt scv sct
297− = return (Bind n (GHole i ns t) scv, sct)
298− discharge n (Guess t v) bt scv sct
299− = return (Bind n (Guess t v) scv, sct)
300− discharge n (PVar r t) bt scv sct
301− = return (Bind n (PVar r t) scv, Bind n (PVTy t) sct)
302− discharge n (PVTy t) bt scv sct
303− = return (Bind n (PVTy t) scv, sct)
311+ return (PVTy tv, tt, [])
312+
313+ discharge n (Lam t) bt scv sct ns
314+ = return (Bind n (Lam t) scv, Bind n (Pi RigW Nothing t bt) sct, ns)
315+ discharge n (Pi r i t k) bt scv sct ns
316+ = return (Bind n (Pi r i t k) scv, sct, ns)
317+ discharge n (Let t v) bt scv sct ns
318+ = return (Bind n (Let t v) scv, Bind n (Let t v) sct, ns)
319+ discharge n (NLet t v) bt scv sct ns
320+ = return (Bind n (NLet t v) scv, Bind n (Let t v) sct, ns)
321+ discharge n (Hole t) bt scv sct ns
322+ = return (Bind n (Hole t) scv, sct, ns)
323+ discharge n (GHole i ns t) bt scv sct uns
324+ = return (Bind n (GHole i ns t) scv, sct, uns)
325+ discharge n (Guess t v) bt scv sct ns
326+ = return (Bind n (Guess t v) scv, sct, ns)
327+ discharge n (PVar r t) bt scv sct ns
328+ = return (Bind n (PVar r t) scv, Bind n (PVTy t) sct, ns)
329+ discharge n (PVTy t) bt scv sct ns
330+ = return (Bind n (PVTy t) scv, sct, ns)
304331
305332-- Number of times a name can be used
306333data UniqueUse = Never -- no more times