32f91a6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't Force an implicit Delay

Fixes #2070 (it can be made to typecheck with an implicit Force but it's unknown whether it's a LazyCodata or LazyEval so leads to a mysterious error, without this restriction)

commit32f91a606a105e17738bc515ed3f2d69504fe79d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 29 Mar 2015, 15:52 (12 years ago) parent95eee3c

1 file changed+14−11

compare with master

unifiedsplit

src/Idris/ElabTerm.hs+14−11

src/Idris/ElabTerm.hs+14−11

@@ -289,26 +289,29 @@ elab ist info emode opts fn tm

289289 --trace ("ELAB " ++ show t') $

290290 let fc = fileFC "Force"

291291 env <- get_env

292− handleError (forceErr env)

292+ handleError (forceErr t' env)

293293 (elab' ina fc' t')

294294 (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

295295 [pimp (sUN "t") Placeholder True,

296296 pimp (sUN "a") Placeholder True,

297297 pexp ct])) True

298298

299− forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

299+ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

300300 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

301− ht == txt "Lazy'" = True

302− forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

301+ ht == txt "Lazy'" = notDelay orig

302+ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

303303 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

304− ht == txt "Lazy'" = True

305− forceErr env (InfiniteUnify _ t _)

304+ ht == txt "Lazy'" = notDelay orig

305+ forceErr orig env (InfiniteUnify _ t _)

306306 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

307− ht == txt "Lazy'" = True

308− forceErr env (Elaborating _ _ t) = forceErr env t

309− forceErr env (ElaboratingArg _ _ _ t) = forceErr env t

310− forceErr env (At _ t) = forceErr env t

311− forceErr env t = False

307+ ht == txt "Lazy'" = notDelay orig

308+ forceErr orig env (Elaborating _ _ t) = forceErr orig env t

309+ forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t

310+ forceErr orig env (At _ t) = forceErr orig env t

311+ forceErr orig env t = False

312+

313+ notDelay t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = False

314+ notDelay _ = True

312315

313316 local f = do e <- get_env

314317 return (f `elem` map fst e)