idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #1421 ] Use resolved names for the impossible LHS

Browse Source
This commit is contained in:
Guillaume ALLAIS 2021-05-17 17:34:56 +01:00 committed by G. Allais
parent d0a6c9b5dd
commit ac4b31b41f
5 changed files with 22 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/TTImp/Impossible.idr
View File

@ -134,7 +134,7 @@ mutual
throw (InternalError "Can't deal with constants here yet") throw (InternalError "Can't deal with constants here yet")
gdefs <- lookupNameBy id n (gamma defs) gdefs <- lookupNameBy id n (gamma defs)
[(n', _, gdef)] <- dropNoMatch mty gdefs [(n', i, gdef)] <- dropNoMatch mty gdefs
| [] => undefinedName fc n | [] => undefinedName fc n
| ts => throw (AmbiguousName fc (map fst ts)) | ts => throw (AmbiguousName fc (map fst ts))
tynf <- nf defs [] (type gdef) tynf <- nf defs [] (type gdef)
@ -148,7 +148,7 @@ mutual
DCon t a _ => DataCon t a DCon t a _ => DataCon t a
TCon t a _ _ _ _ _ _ => TyCon t a TCon t a _ _ _ _ _ _ => TyCon t a
_ => Func _ => Func
processArgs (Ref fc head n') tynf exps autos named processArgs (Ref fc head (Resolved i)) tynf exps autos named
mkTerm : {auto c : Ref Ctxt Defs} -> mkTerm : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} -> {auto q : Ref QVar Int} ->

3
tests/Main.idr
View File

@ -55,7 +55,8 @@ idrisTestsCoverage = MkTestPool "Coverage checking" []
["coverage001", "coverage002", "coverage003", "coverage004", ["coverage001", "coverage002", "coverage003", "coverage004",
"coverage005", "coverage006", "coverage007", "coverage008", "coverage005", "coverage006", "coverage007", "coverage008",
"coverage009", "coverage010", "coverage011", "coverage012", "coverage009", "coverage010", "coverage011", "coverage012",
"coverage013", "coverage014", "coverage015", "coverage016"] "coverage013", "coverage014", "coverage015", "coverage016",
"coverage017"]
idrisTestsCasetree : TestPool idrisTestsCasetree : TestPool
idrisTestsCasetree = MkTestPool "Case tree building" [] idrisTestsCasetree = MkTestPool "Case tree building" []

14
tests/idris2/coverage017/Issue1421.idr Normal file
View File

@ -0,0 +1,14 @@
plus2 : Nat -> Nat
plus2 = S . S
okplus2Injective : (x, y : Nat) -> Equal (plus2 x) (plus2 y) -> Equal x y
okplus2Injective Z Z Refl = Refl
okplus2Injective (S n) (S n) Refl = Refl
okplus2Injective Z (S _) _ impossible
okplus2Injective (S _) Z _ impossible
badplus2Injective : (x, y : Nat) -> Equal (plus2 x) (plus2 y) -> Equal x y
badplus2Injective Z Z Refl = Refl
badplus2Injective Z (S _) _ impossible
badplus2Injective (S _) Z _ impossible
badplus2Injective (S n) (S n) Refl = Refl

1
tests/idris2/coverage017/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Issue1421 (Issue1421.idr)

3
tests/idris2/coverage017/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --check Issue1421.idr
rm -rf build