f82a1c4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change a lookupCtxt to lookupCtxtExact

Except when disambiguating, we should always use the latter to look up resolved names. Otherwise, we get surprising ambiguity errors where there is no ambiguity, or similarly odd behaviour. Fixes #3625

commitf82a1c47ec0f79b53a17fbad67e691b00bc86dbd authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 5 Mar 2017, 17:27 (10 years ago) parent6dffcc7

1 file changed+3−4

compare with master

unifiedsplit

src/Idris/Termination.hs+3−4

src/Idris/Termination.hs+3−4

@@ -270,8 +270,8 @@ verifyTotality (fc, n)

270270buildSCG :: (FC, Name) -> Idris ()

271271buildSCG (_, n) = do

272272 ist <- getIState

273− case lookupCtxt n (idris_callgraph ist) of

274− [cg] -> case lookupDefExact n (tt_ctxt ist) of

273+ case lookupCtxtExact n (idris_callgraph ist) of

274+ Just cg -> case lookupDefExact n (tt_ctxt ist) of

275275 Just (CaseOp _ _ _ pats _ cd) ->

276276 let (args, sc) = cases_compiletime cd in

277277 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"

@@ -280,8 +280,7 @@ buildSCG (_, n) = do

280280 logCoverage 5 $ "SCG is: " ++ show newscg

281281 addToCG n ( cg { scg = newscg } )

282282 _ -> return () -- CG comes from a type declaration only

283− [] -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"

284− x -> error $ "buildSCG: " ++ show (n, x)

283+ _ -> logCoverage 5 $ "Could not build SCG for " ++ show n ++ "\n"

285284

286285delazy = delazy' False -- not lazy codata

287286delazy' all t@(App _ f a)