diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index a58e01042..d52bb147c 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/src/Idris/Elab/Implementation.idr
@@ -13,6 +13,7 @@ import Idris.Syntax
 
 import TTImp.BindImplicits
 import TTImp.Elab.Check
+import TTImp.Elab
 import TTImp.ProcessDecls
 import TTImp.TTImp
 import TTImp.TTImp.Functor
@@ -181,7 +182,25 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
 
          log "elab.implementation" 5 $ "Implementation type: " ++ show impTy
 
-         when (typePass pass) $ processDecl [] nest env impTyDecl
+         -- Handle the case where it was already declared with a Nothing mbody
+         when (typePass pass) $ do
+           gdefm <- lookupCtxtExactI impName (gamma defs)
+           case gdefm of
+              Nothing => processDecl [] nest env impTyDecl
+              -- If impName exists, check that it is a forward declaration of the same type
+              Just (tidx,gdef) =>
+                do u <- uniVar vfc
+                   -- If the definition is filled in, it wasn't a forward declaration
+                   let None = definition gdef
+                     | _ => throw (AlreadyDefined vfc impName)
+                   (ty,_) <- elabTerm tidx InType [] nest env
+                                      (IBindHere vfc (PI erased) impTy)
+                                      (Just (gType vfc u))
+                   let fullty = abstractFullEnvType vfc env ty
+                   ok <- convert defs [] fullty (type gdef)
+                   unless ok $ do logTermNF "elab.implementation" 1 "Previous" [] (type gdef)
+                                  logTermNF "elab.implementation" 1 "Now" [] fullty
+                                  throw (CantConvert (getFC impTy) (gamma defs) [] fullty (type gdef))
 
          -- If the body is empty, we're done for now (just declaring that
          -- the implementation exists and define it later)
diff --git a/tests/Main.idr b/tests/Main.idr
index 89e5a23ae..4f6047064 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -119,7 +119,8 @@ idrisTestsInterface = MkTestPool "Interface" [] Nothing
        "interface013", "interface014", "interface015", "interface016",
        "interface017", "interface018", "interface019", "interface020",
        "interface021", "interface022", "interface023", "interface024",
-       "interface025", "interface026", "interface027", "interface028"]
+       "interface025", "interface026", "interface027", "interface028",
+       "interface029"]
 
 idrisTestsLinear : TestPool
 idrisTestsLinear = MkTestPool "Quantities" [] Nothing
diff --git a/tests/idris2/interface029/ForwardImpl1.idr b/tests/idris2/interface029/ForwardImpl1.idr
new file mode 100644
index 000000000..4749bf133
--- /dev/null
+++ b/tests/idris2/interface029/ForwardImpl1.idr
@@ -0,0 +1,23 @@
+
+interface Pretty a where
+    pretty : a -> String
+
+data Bar : Type -> Type
+data Foo a = FNil | FCons a (Bar a)
+data Bar a = BNil | BCons a (Foo a)
+
+Pretty a => Pretty (Foo a)
+
+implementation Pretty a => Pretty (Bar a) where
+    pretty (BNil) = "Nil"
+    pretty (BCons a f) = "\{pretty a} :: \{pretty f}"
+
+implementation Pretty a => Pretty (Foo a) where
+    pretty (FNil) = "Nil"
+    pretty (FCons a f) = "\{pretty a} :: \{pretty f}"
+
+implementation Pretty String where
+    pretty a = a
+
+main : IO ()
+main = putStrLn $ pretty (BCons "1" (FCons "2" (BCons "3" FNil)))
diff --git a/tests/idris2/interface029/ForwardImpl2.idr b/tests/idris2/interface029/ForwardImpl2.idr
new file mode 100644
index 000000000..1edeab1f7
--- /dev/null
+++ b/tests/idris2/interface029/ForwardImpl2.idr
@@ -0,0 +1,16 @@
+interface IsEven a where
+    isEven : a -> Bool
+
+interface IsOdd b where
+    isOdd : b -> Bool
+
+implementation IsOdd Nat
+
+implementation IsEven Nat where
+    isEven 0 = True
+    isEven (S k) = not $ isOdd k
+
+implementation Show Nat => IsOdd Nat where
+    isOdd 0 = True
+    isOdd (S k) = not $ isEven k
+
diff --git a/tests/idris2/interface029/ForwardImpl3.idr b/tests/idris2/interface029/ForwardImpl3.idr
new file mode 100644
index 000000000..79314ed83
--- /dev/null
+++ b/tests/idris2/interface029/ForwardImpl3.idr
@@ -0,0 +1,9 @@
+interface IsOdd b where
+    isOdd : b -> Bool
+
+implementation IsOdd Bool where
+  isOdd b = b
+
+implementation IsOdd Bool where
+  isOdd b = b
+
diff --git a/tests/idris2/interface029/expected b/tests/idris2/interface029/expected
new file mode 100644
index 000000000..a5a00d674
--- /dev/null
+++ b/tests/idris2/interface029/expected
@@ -0,0 +1,16 @@
+1 :: 2 :: 3 :: Nil
+1/1: Building ForwardImpl2 (ForwardImpl2.idr)
+Error: Mismatch between: Show Nat => IsOdd Nat and IsOdd Nat.
+
+ForwardImpl2:13:1--15:33
+ 13 | implementation Show Nat => IsOdd Nat where
+ 14 |     isOdd 0 = True
+ 15 |     isOdd (S k) = not $ isEven k
+
+1/1: Building ForwardImpl3 (ForwardImpl3.idr)
+Error: Main.IsOdd implementation at ForwardImpl3:7:1--8:14 is already defined.
+
+ForwardImpl3:7:1--8:14
+ 7 | implementation IsOdd Bool where
+ 8 |   isOdd b = b
+
diff --git a/tests/idris2/interface029/run b/tests/idris2/interface029/run
new file mode 100644
index 000000000..9c7acf2f7
--- /dev/null
+++ b/tests/idris2/interface029/run
@@ -0,0 +1,5 @@
+rm -rf build
+
+$1 --no-banner --no-color --console-width 0 -x main ForwardImpl1.idr
+$1 --no-banner --no-color --console-width 0 --check ForwardImpl2.idr
+$1 --no-banner --no-color --console-width 0 --check ForwardImpl3.idr