diff --git a/src/TTImp/Impossible.idr b/src/TTImp/Impossible.idr
index 8f132f6df..9b7398a4f 100644
--- a/src/TTImp/Impossible.idr
+++ b/src/TTImp/Impossible.idr
@@ -134,7 +134,7 @@ mutual
                throw (InternalError "Can't deal with constants here yet")
 
            gdefs <- lookupNameBy id n (gamma defs)
-           [(n', _, gdef)] <- dropNoMatch mty gdefs
+           [(n', i, gdef)] <- dropNoMatch mty gdefs
               | [] => undefinedName fc n
               | ts => throw (AmbiguousName fc (map fst ts))
            tynf <- nf defs [] (type gdef)
@@ -148,7 +148,7 @@ mutual
                         DCon t a _ => DataCon t a
                         TCon t a _ _ _ _ _ _ => TyCon t a
                         _ => 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} ->
            {auto q : Ref QVar Int} ->
diff --git a/tests/Main.idr b/tests/Main.idr
index 4046cf938..8eb96156a 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -55,7 +55,8 @@ idrisTestsCoverage = MkTestPool "Coverage checking" []
       ["coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",
        "coverage009", "coverage010", "coverage011", "coverage012",
-       "coverage013", "coverage014", "coverage015", "coverage016"]
+       "coverage013", "coverage014", "coverage015", "coverage016",
+       "coverage017"]
 
 idrisTestsCasetree : TestPool
 idrisTestsCasetree = MkTestPool "Case tree building" []
diff --git a/tests/idris2/coverage017/Issue1421.idr b/tests/idris2/coverage017/Issue1421.idr
new file mode 100644
index 000000000..0c29c1df9
--- /dev/null
+++ b/tests/idris2/coverage017/Issue1421.idr
@@ -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
diff --git a/tests/idris2/coverage017/expected b/tests/idris2/coverage017/expected
new file mode 100644
index 000000000..6ad95d76d
--- /dev/null
+++ b/tests/idris2/coverage017/expected
@@ -0,0 +1 @@
+1/1: Building Issue1421 (Issue1421.idr)
diff --git a/tests/idris2/coverage017/run b/tests/idris2/coverage017/run
new file mode 100755
index 000000000..f18de8e74
--- /dev/null
+++ b/tests/idris2/coverage017/run
@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --check Issue1421.idr
+
+rm -rf build