[ new ] Handle forward declarations of implementations (#2668)

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

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)

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

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)))

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
+

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
+

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
+

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