@@ -203,28 +203,15 @@ check' holes ctxt env top = chk env top where
203203 discharge n (NLet t v) scv sct
204204 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
205205 discharge n (Hole t) scv sct
206− = do -- A hole can't appear in the type of its scope
207− checkNotHoley 0 sct
208− return (Bind n (Hole t) scv, sct)
206+ = return (Bind n (Hole t) scv, sct)
209207 discharge n (GHole t) scv sct
210− = do -- A hole can't appear in the type of its scope
211− checkNotHoley 0 sct
212− return (Bind n (GHole t) scv, sct)
208+ = return (Bind n (GHole t) scv, sct)
213209 discharge n (Guess t v) scv sct
214− = do -- A hole can't appear in the type of its scope
215− checkNotHoley 0 sct
216− return (Bind n (Guess t v) scv, sct)
210+ = return (Bind n (Guess t v) scv, sct)
217211 discharge n (PVar t) scv sct
218212 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)
219213 discharge n (PVTy t) scv sct
220214 = return (Bind n (PVTy t) scv, sct)
221−
222− checkNotHoley i (V v)
223− | v == i = fail "You can't put a hole where a hole don't belong"
224− checkNotHoley i (App f a) = do checkNotHoley i f
225− checkNotHoley i a
226− checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
227− checkNotHoley _ _ = return ()
228215
229216
230217checkProgram :: Context -> RProgram -> TC Context