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

idris.cabal+3

compare with master

unifiedsplit

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

473 test/error007/run

474 test/error007/*.idr

475 test/error007/expected

476+ test/error008/run

477+ test/error008/*.idr

478+ test/error008/expected

476

479

477 test/ffi001/run

480 test/ffi001/run

478 test/ffi001/*.idr

481 test/ffi001/*.idr

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

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

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

270 [] -> return ()

271

272+ elabRec = elabE initElabCtxt Nothing

273+

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

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

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

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

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

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

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

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

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

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

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

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

373 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

373 elab' ina fc (PResolveTC fc')

375 elab' ina fc (PResolveTC fc')

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

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

375 instanceArg c

377 instanceArg c

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

722 hs <- get_holes

724 hs <- get_holes

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

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

724 then handleError (tcRecoverable emode)

726 then handleError (tcRecoverable emode)

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

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

726 (movelast n)

728 (movelast n)

727 else movelast n)

729 else movelast n)

728 (ivs' \\ ivs)

730 (ivs' \\ ivs)

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

895 hs <- get_holes

897 hs <- get_holes

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

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

897 then handleError (tcRecoverable emode)

899 then handleError (tcRecoverable emode)

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

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

899 (movelast n)

901 (movelast n)

900 else movelast n)

902 else movelast n)

901 (ivs' \\ ivs)

903 (ivs' \\ ivs)

test/error008/error008.idrnew file+5

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

1+import Data.Vect

2+

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

4+s2 = Refl

5+

test/error008/error008a.idrnew file+5

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

1+import Data.Vect

2+

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

4+s1 = Refl

5+

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