8ac3356 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Don't unify explicit lambda types

8ac3356Edwin Brady13 years ago

src/Idris/Core/Elaborate.hs+5

compare with master

unifiedsplit

@@ -49,6 +49,11 @@ proofFail e = do s <- get

49 return a

50 Error err -> lift $ Error (ProofSearchFail err)

52+explicit :: Name -> Elab' aux ()

53+explicit n = do ES (p, a) s m <- get

54+ let p' = p { dontunify = n : dontunify p }

55+ put (ES (p', a) s m)

56+

52saveState :: Elab' aux ()

57saveState :: Elab' aux ()

53saveState = do e@(ES p s _) <- get

58saveState = do e@(ES p s _) <- get

54 put (ES p s (Just e))

59 put (ES p s (Just e))

src/Idris/ElabTerm.hs+3−2

@@ -256,6 +256,7 @@ elab ist info pattern tcgen fn tm

256 tyn <- unique_hole (MN 0 "lamty")

257 checkPiGoal n

258 claim tyn RType

259+ explicit tyn

259 attack

260 attack

260 ptm <- get_term

261 ptm <- get_term

261 hs <- get_holes

262 hs <- get_holes

@@ -264,8 +265,6 @@ elab ist info pattern tcgen fn tm

264 introTy (Var tyn) (Just n)

265 introTy (Var tyn) (Just n)

265 -- end_unify

266 -- end_unify

266 focus tyn

267 focus tyn

267− ptm <- get_term

268− hs <- get_holes

269 elabE (True, a) ty

268 elabE (True, a) ty

270 elabE (True, a) sc

269 elabE (True, a) sc

271 solve

270 solve

@@ -288,10 +287,12 @@ elab ist info pattern tcgen fn tm

288 claim tyn RType

287 claim tyn RType

289 valn <- unique_hole (MN 0 "letval")

288 valn <- unique_hole (MN 0 "letval")

290 claim valn (Var tyn)

289 claim valn (Var tyn)

290+ explicit valn

291 letbind n (Var tyn) (Var valn)

292 case ty of

293 Placeholder -> return ()

294 _ -> do focus tyn

295+ explicit tyn

295 elabE (True, a) ty

296 elabE (True, a) ty

296 focus valn

297 focus valn

297 elabE (True, a) val

298 elabE (True, a) val