@@ -203,28 +203,15 @@ check' holes ctxt env top = chk env top where
203 discharge n (NLet t v) scv sct
203 discharge n (NLet t v) scv sct
204 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
204 = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
205 discharge n (Hole t) scv sct
205 discharge n (Hole t) scv sct
206− = do -- A hole can't appear in the type of its scope
208− return (Bind n (Hole t) scv, sct)
206+ = return (Bind n (Hole t) scv, sct)
209 discharge n (GHole t) scv sct
207 discharge n (GHole t) scv sct
210− = do -- A hole can't appear in the type of its scope
212− return (Bind n (GHole t) scv, sct)
208+ = return (Bind n (GHole t) scv, sct)
213 discharge n (Guess t v) scv sct
209 discharge n (Guess t v) scv sct
214− = do -- A hole can't appear in the type of its scope
216− return (Bind n (Guess t v) scv, sct)
210+ = return (Bind n (Guess t v) scv, sct)
217 discharge n (PVar t) scv sct
211 discharge n (PVar t) scv sct
218 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)
212 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)
219 discharge n (PVTy t) scv sct
213 discharge n (PVTy t) scv sct
220 = return (Bind n (PVTy t) scv, sct)
214 = return (Bind n (PVTy t) scv, sct)
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
226− checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
227− checkNotHoley _ _ = return ()
230checkProgram :: Context -> RProgram -> TC Context
217checkProgram :: Context -> RProgram -> TC Context