5984b2f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't use top level elab for resolveTC

Otherwise it'll attempt to resolve ambiguities and the elaborator could think there's an interface resolution failure, when actually it's just an ambiguity that hasn't been resolved yet.

commit5984b2ff0e16c2779d334dffe786b3da91f4c994 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 19 Apr 2016, 22:25 (10 years ago) parentcf0b54e

6 files changed+26−3

compare with master

unifiedsplit

idris.cabal+3 src/Idris/Elab/Term.hs+5−3 test/error008/error008.idr+5 test/error008/error008a.idr+5 test/error008/expected+4 test/error008/run+4

idris.cabal+3

@@ -473,6 +473,9 @@ Extra-source-files:

473473 test/error007/run

474474 test/error007/*.idr

475475 test/error007/expected

476+ test/error008/run

477+ test/error008/*.idr

478+ test/error008/expected

476479

477480 test/ffi001/run

478481 test/ffi001/*.idr

src/Idris/Elab/Term.hs+5−3

@@ -269,6 +269,8 @@ elab ist info emode opts fn tm

269269 (h: hs) -> do patvar h; mkPat

270270 [] -> return ()

271271

272+ elabRec = elabE initElabCtxt Nothing

273+

272274 -- | elabE elaborates an expression, possibly wrapping implicit coercions

273275 -- and forces/delays. If you make a recursive call in elab', it is

274276 -- normally correct to call elabE - the ones that don't are desugarings

@@ -369,7 +371,7 @@ elab ist info emode opts fn tm

369371 UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

370372 _ -> elab' ina (Just fc) (PRef fc [] unitCon)

371373 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

372− = do g <- goal; resolveTC' False False 5 g fn ist

374+ = do g <- goal; resolveTC False False 5 g fn elabRec ist

373375 elab' ina fc (PResolveTC fc')

374376 = do c <- getNameFrom (sMN 0 "__class")

375377 instanceArg c

@@ -722,7 +724,7 @@ elab ist info emode opts fn tm

722724 hs <- get_holes

723725 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

724726 then handleError (tcRecoverable emode)

725− (resolveTC' True False 10 g fn ist)

727+ (resolveTC True False 10 g fn elabRec ist)

726728 (movelast n)

727729 else movelast n)

728730 (ivs' \\ ivs)

@@ -895,7 +897,7 @@ elab ist info emode opts fn tm

895897 hs <- get_holes

896898 if all (\n -> not (n `elem` hs)) (freeNames g)

897899 then handleError (tcRecoverable emode)

898− (resolveTC' False False 10 g fn ist)

900+ (resolveTC False False 10 g fn elabRec ist)

899901 (movelast n)

900902 else movelast n)

901903 (ivs' \\ ivs)

test/error008/error008.idrnew file+5

@@ -0,0 +1,5 @@

1+import Data.Vect

3+s2 : x + sum Nil = x * fromInteger 0

4+s2 = Refl

test/error008/error008a.idrnew file+5

@@ -0,0 +1,5 @@

1+import Data.Vect

3+s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0

4+s1 = Refl

test/error008/expectednew file+4

@@ -0,0 +1,4 @@

1+error008.idr:3:4:When checking type of Main.s2:

2+Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil

3+error008a.idr:3:4:When checking type of Main.s1:

4+Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil

test/error008/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --check --nocolour error008.idr

3+${IDRIS:-idris} $@ --check --nocolour error008a.idr

4+rm -f *.ibc