interface methods: Haskell Typechecker (#11028)

part of #11006

changelog_begin
changelog_end

compiler/daml-lf-ast/src/DA/Daml/LF/Ast/World.hs

@@ -19,6 +19,7 @@ module DA.Daml.LF.Ast.World(
     lookupDataType,
     lookupChoice,
     lookupInterfaceChoice,
+    lookupInterfaceMethod,
     lookupValue,
     lookupModule,
     lookupInterface,
@@ -100,6 +101,7 @@ data LookupError
   | LEException !(Qualified TypeConName)
   | LEChoice !(Qualified TypeConName) !ChoiceName
   | LEInterface !(Qualified TypeConName)
+  | LEInterfaceMethod !(Qualified TypeConName) !MethodName
   deriving (Eq, Ord, Show)
 
 lookupModule :: Qualified a -> World -> Either LookupError Module
@@ -154,12 +156,19 @@ lookupChoice (tplRef, chName) world = do
 
 lookupInterfaceChoice ::
      (Qualified TypeConName, ChoiceName) -> World -> Either LookupError InterfaceChoice
-lookupInterfaceChoice (tplRef, chName) world = do
-  iface <- lookupInterface tplRef world
+lookupInterfaceChoice (ifaceRef, chName) world = do
+  iface <- lookupInterface ifaceRef world
   case NM.lookup chName (intChoices iface) of
-    Nothing -> Left (LEChoice tplRef chName)
+    Nothing -> Left (LEChoice ifaceRef chName)
     Just choice -> Right choice
 
+lookupInterfaceMethod :: (Qualified TypeConName, MethodName) -> World -> Either LookupError InterfaceMethod
+lookupInterfaceMethod (ifaceRef, methodName) world = do
+  iface <- lookupInterface ifaceRef world
+  case NM.lookup methodName (intMethods iface) of
+      Nothing -> Left (LEInterfaceMethod ifaceRef methodName)
+      Just method -> Right method
+
 instance Pretty LookupError where
   pPrint = \case
     LEPackage pkgId -> "unknown package:" <-> pretty pkgId
@@ -171,4 +180,5 @@ instance Pretty LookupError where
     LETemplate tplRef -> "unknown template:" <-> pretty tplRef
     LEException exnRef -> "unknown exception:" <-> pretty exnRef
     LEChoice tplRef chName -> "unknown choice:" <-> pretty tplRef <> ":" <> pretty chName
-    LEInterface ifaceRef -> "unknown interface" <-> pretty ifaceRef
+    LEInterface ifaceRef -> "unknown interface:" <-> pretty ifaceRef
+    LEInterfaceMethod ifaceRef methodName -> "unknown interface method:" <-> pretty ifaceRef <> "." <> pretty methodName

compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs

@@ -748,9 +748,10 @@ typeOf' = \case
     checkImplements tpl iface
     checkExpr val (TCon iface)
     pure (TOptional (TCon tpl))
-  ECallInterface _ _ _ ->
-    -- TODO https://github.com/digital-asset/daml/issues/11006
-    error "ECallInterface not yet implemented"
+  ECallInterface iface method val -> do
+    method <- inWorld (lookupInterfaceMethod (iface, method))
+    checkExpr val (TCon iface)
+    pure (ifmType method)
   EUpdate upd -> typeOfUpdate upd
   EScenario scen -> typeOfScenario scen
   ELocation _ expr -> typeOf' expr
@@ -808,15 +809,21 @@ checkDefTypeSyn DefTypeSyn{synParams,synType} = do
 
 
 checkIface :: MonadGamma m => DefInterface -> m ()
-checkIface DefInterface{intName, intChoices} = do
+checkIface DefInterface{intName, intChoices, intMethods} = do
   checkUnique (EDuplicateInterfaceChoiceName intName) $ NM.names intChoices
+  checkUnique (EDuplicateInterfaceMethodName intName) $ NM.names intMethods
   forM_ intChoices checkIfaceChoice
+  forM_ intMethods checkIfaceMethod
 
 checkIfaceChoice :: MonadGamma m => InterfaceChoice -> m ()
 checkIfaceChoice InterfaceChoice{ifcArgType,ifcRetType} = do
   checkType ifcArgType KStar
   checkType ifcRetType KStar
 
+checkIfaceMethod :: MonadGamma m => InterfaceMethod -> m ()
+checkIfaceMethod InterfaceMethod{ifmType} = do
+  checkType ifmType KStar
+
 -- | Check that a type constructor definition is well-formed.
 checkDefDataType :: MonadGamma m => Module -> DefDataType -> m ()
 checkDefDataType m (DefDataType _loc name _serializable params dataCons) = do
@@ -876,9 +883,10 @@ checkTemplate m t@(Template _loc tpl param precond signatories observers text ch
 
 checkIfaceImplementation :: MonadGamma m => Qualified TypeConName -> TemplateImplements -> m ()
 checkIfaceImplementation tplTcon TemplateImplements{..} = do
-  -- TODO https://github.com/digital-asset/daml/issues/11006
-  --  check methods, not just choices
-  DefInterface {intChoices} <- inWorld $ lookupInterface tpiInterface
+  let tplName = qualObject tplTcon
+  DefInterface {intChoices, intMethods} <- inWorld $ lookupInterface tpiInterface
+
+  -- check choices
   forM_ intChoices $ \InterfaceChoice {ifcName, ifcConsuming, ifcArgType, ifcRetType} -> do
     TemplateChoice {chcConsuming, chcArgBinder, chcReturnType} <-
       inWorld $ lookupChoice (tplTcon, ifcName)
@@ -889,6 +897,17 @@ checkIfaceImplementation tplTcon TemplateImplements{..} = do
     unless (alphaType chcReturnType ifcRetType) $
       throwWithContext $ EBadInterfaceChoiceImplRetType ifcName ifcRetType chcReturnType
 
+  -- check methods
+  let missingMethods = HS.difference (NM.namesSet intMethods) (NM.namesSet tpiMethods)
+  case HS.toList missingMethods of
+    [] -> pure ()
+    (methodName:_) -> throwWithContext (EMissingInterfaceMethod tplName tpiInterface methodName)
+  forM_ tpiMethods $ \TemplateImplementsMethod{tpiMethodName, tpiMethodExpr} -> do
+    case NM.lookup tpiMethodName intMethods of
+      Nothing -> throwWithContext (EUnknownInterfaceMethod tplName tpiInterface tpiMethodName)
+      Just InterfaceMethod{ifmType} ->
+        checkExpr tpiMethodExpr (TCon tplTcon :-> ifmType)
+
 _checkFeature :: MonadGamma m => Feature -> m ()
 _checkFeature feature = do
     version <- getLfVersion
@@ -922,7 +941,9 @@ checkModule m@(Module _modName _path _flags synonyms dataTypes values templates
   let with ctx f x = withContext (ctx x) (f x)
   traverse_ (with (ContextDefTypeSyn m) checkDefTypeSyn) synonyms
   traverse_ (with (ContextDefDataType m) $ checkDefDataType m) dataTypes
+  -- NOTE(SF): Interfaces should be checked before templates, because the typechecking
+  -- for templates relies on well-typed interface definitions.
+  traverse_ (with (ContextDefInterface m) checkIface) interfaces
   traverse_ (with (\t -> ContextTemplate m t TPWhole) $ checkTemplate m) templates
   traverse_ (with (ContextDefException m) (checkDefException m)) exceptions
   traverse_ (with (ContextDefValue m) checkDefValue) values
-  traverse_ (with (ContextDefInterface m) checkIface) interfaces

compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs

@@ -132,11 +132,14 @@ data Error
   | EInterfaceTypeWithParams
   | EMissingInterfaceDefinition !TypeConName
   | EDuplicateInterfaceChoiceName !TypeConName !ChoiceName
+  | EDuplicateInterfaceMethodName !TypeConName !MethodName
   | EUnknownInterface !TypeConName
   | EMissingInterfaceChoice !ChoiceName
   | EBadInterfaceChoiceImplConsuming !ChoiceName !Bool !Bool
   | EBadInterfaceChoiceImplArgType !ChoiceName !Type !Type
   | EBadInterfaceChoiceImplRetType !ChoiceName !Type !Type
+  | EMissingInterfaceMethod !TypeConName !(Qualified TypeConName) !MethodName
+  | EUnknownInterfaceMethod !TypeConName !(Qualified TypeConName) !MethodName
   | ETemplateDoesNotImplementInterface !(Qualified TypeConName) !(Qualified TypeConName)
 
 contextLocation :: Context -> Maybe SourceLoc
@@ -380,6 +383,8 @@ instance Pretty Error where
       "Missing interface definition for interface type: " <> pretty iface
     EDuplicateInterfaceChoiceName iface choice ->
       "Duplicate choice name '" <> pretty choice <> "' in interface definition for " <> pretty iface
+    EDuplicateInterfaceMethodName iface method ->
+      "Duplicate method name '" <> pretty method <> "' in interface definition for " <> pretty iface
     EUnknownInterface tcon -> "Unknown interface: " <> pretty tcon
     EMissingInterfaceChoice ch -> "Missing interface choice implementation for " <> pretty ch
     EBadInterfaceChoiceImplConsuming ch ifaceConsuming tplConsuming ->
@@ -400,6 +405,10 @@ instance Pretty Error where
       , "Expected: " <> pretty ifaceRetType
       , "But got: " <> pretty tplRetType
       ]
+    EMissingInterfaceMethod tpl iface method ->
+      "Template " <> pretty tpl <> " is missing method " <> pretty method <> " for interface " <> pretty iface
+    EUnknownInterfaceMethod tpl iface method ->
+      "Template " <> pretty tpl <> " implements " <> pretty method <> " but interface " <> pretty iface <> " has no such method."
     ETemplateDoesNotImplementInterface tpl iface ->
       "Template " <> pretty tpl <> " does not implement interface " <> pretty iface