c55f8c2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Unification fix to avoid giving up on recoverable errors

If function names don't unify, we shouldn't try to univy arguments! Otherwise, we can get unrecoverable unification failures if some unrelated arguments later unify. Fixes #465

commitc55f8c2dfede43f772ea72d7a9b912cd8f7a6077 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 19 Sep 2013, 16:56 (13 years ago) parentdaab1a3

4 files changed+14−9

compare with master

unifiedsplit

src/Core/ProofState.hs+3−3 src/Core/Unify.hs+6−1 src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/Parser.hs+2−2

src/Core/ProofState.hs+3−3

@@ -176,13 +176,13 @@ unify' :: Context -> Env -> TT Name -> TT Name ->

176176unify' ctxt env topx topy =

177177 do ps <- get

178178 let dont = dontunify ps

179− (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $

179+ (u, fails) <- traceWhen (unifylog ps) ("Trying " ++ show (topx, topy)) $

180180 lift $ unify ctxt env topx topy dont (holes ps)

181181 traceWhen (unifylog ps)

182182 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

183183 " in " ++ show env ++

184− "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

185− ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"

184+ "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails ++ "\nCurrent problems:\n"

185+ ++ qshow (problems ps) ++ "\nHoles: " ++ show (holes ps) ++ "\n"

186186-- ++ show (pterm ps)

187187 ++ "\n----------") $

188188 case fails of

src/Core/Unify.hs+6−1

@@ -154,6 +154,9 @@ unify ctxt env topx topy dont holes =

154154 sc i = do UI s f <- get

155155 put (UI (s+i) f)

156156

157+ errors = do UI s f <- get

158+ return (not (null f))

159+

157160 uplus u1 u2 = do UI s f <- get

158161 r <- u1

159162 UI s f' <- get

@@ -290,7 +293,9 @@ unify ctxt env topx topy dont holes =

290293 then

291294-- (notFn headx && notFn heady))) then

292295 do uf <- un' True bnames headx heady

293− unArgs uf argsx argsy

296+ failed <- errors

297+ if (not failed) then unArgs uf argsx argsy

298+ else return []

294299 else -- trace ("TMPFAIL " ++ show (appx, appy, injective appx, injective appy)) $

295300 unifyTmpFail appx appy)

296301 (unifyTmpFail appx appy) -- whole application fails

src/Idris/AbsSyntaxTree.hs+3−3

@@ -1098,6 +1098,9 @@ showImp ist impl colour tm = se 10 [] tm where

10981098 se p bnd (PQuote r) = "![" ++ show r ++ "]"

10991099 se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n

11001100 se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"

1101+ se p bnd e

1102+ | Just str <- slist p bnd e = str

1103+ | Just num <- snat p e = perhapsColourise colouriseData (show num)

11011104 se p bnd (PRef fc n) = showName ist bnd impl colour n

11021105 se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++

11031106 (if impl then " : " ++ se 10 bnd ty else "") ++ " => "

@@ -1130,9 +1133,6 @@ showImp ist impl colour tm = se 10 [] tm where

11301133 = bracket p 2 $

11311134 "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

11321135 se 10 ((n, False):bnd) sc

1133− se p bnd e

1134− | Just str <- slist p bnd e = str

1135− | Just num <- snat p e = perhapsColourise colouriseData (show num)

11361136 se p bnd (PMatchApp _ f) = "match " ++ show f

11371137 se p bnd (PApp _ hd@(PRef _ f) [])

11381138 | not impl = se p bnd hd

src/Idris/Parser.hs+2−2

@@ -147,8 +147,8 @@ loadSource lidr f

147147 -- build size change graph from simplified definitions

148148 iLOG "Totality checking"

149149 i <- getIState

150−-- mapM_ buildSCG (idris_totcheck i)

151−-- mapM_ checkDeclTotality (idris_totcheck i)

150+ mapM_ buildSCG (idris_totcheck i)

151+ mapM_ checkDeclTotality (idris_totcheck i)

152152 iLOG ("Finished " ++ f)

153153 ibcsd <- valIBCSubDir i

154154 iLOG "Universe checking"