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

git.iko.soy/Idris-dev

Don't unify explicit lambda types

Fixes #734

commit8ac33569f9d8e9ed58d7f0b76096ae55ee0df7b8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 23 Dec 2013, 11:42 (13 years ago) parent73e81f7

2 files changed+8−2

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+5 src/Idris/ElabTerm.hs+3−2

src/Idris/Core/Elaborate.hs+5

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

4949 return a

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

5151

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+

5257saveState :: Elab' aux ()

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

5459 put (ES p s (Just e))

src/Idris/ElabTerm.hs+3−2

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

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

257257 checkPiGoal n

258258 claim tyn RType

259+ explicit tyn

259260 attack

260261 ptm <- get_term

261262 hs <- get_holes

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

264265 introTy (Var tyn) (Just n)

265266 -- end_unify

266267 focus tyn

267− ptm <- get_term

268− hs <- get_holes

269268 elabE (True, a) ty

270269 elabE (True, a) sc

271270 solve

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

288287 claim tyn RType

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

290289 claim valn (Var tyn)

290+ explicit valn

291291 letbind n (Var tyn) (Var valn)

292292 case ty of

293293 Placeholder -> return ()

294294 _ -> do focus tyn

295+ explicit tyn

295296 elabE (True, a) ty

296297 focus valn

297298 elabE (True, a) val