interfaces: lf typechecker implementation (#10843)

* interfaces: lf typechecker implementation CHANGELOG_BEGIN CHANGELOG_END * review suggestions
2024-09-20 01:07:18 +03:00 · 2021-09-13 14:58:33 +02:00 · 2021-09-13 14:58:33 +02:00 · 6dc769b7ad
commit 6dc769b7ad
parent d9178d2ac2
3 changed files with 90 additions and 12 deletions
--- a/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/World.hs
+++ b/compiler/daml-lf-ast/src/DA/Daml/LF/Ast/World.hs
@ -19,7 +19,8 @@ module DA.Daml.LF.Ast.World(
    lookupDataType,
    lookupChoice,
    lookupValue,
-    lookupModule
+    lookupModule,
+    lookupInterface
    ) where

 import DA.Pretty
@ -97,6 +98,7 @@ data LookupError
  | LETemplate !(Qualified TypeConName)
  | LEException !(Qualified TypeConName)
  | LEChoice !(Qualified TypeConName) !ChoiceName
+  | LEInterface !(Qualified TypeConName)
  deriving (Eq, Ord, Show)

 lookupModule :: Qualified a -> World -> Either LookupError Module
@ -136,6 +138,9 @@ lookupValue = lookupDefinition moduleValues LEValue
 lookupTemplate :: Qualified TypeConName -> World -> Either LookupError Template
 lookupTemplate = lookupDefinition moduleTemplates LETemplate

+lookupInterface :: Qualified TypeConName -> World -> Either LookupError DefInterface
+lookupInterface = lookupDefinition moduleInterfaces LEInterface
+
 lookupException :: Qualified TypeConName -> World -> Either LookupError DefException
 lookupException = lookupDefinition moduleExceptions LEException

@ -157,3 +162,4 @@ 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
--- a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs
+++ b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Check.hs
@ -536,8 +536,7 @@ typeOfCase scrut alts = do
                DataEnum cons ->  (,,) (length cons) (\k -> CPEnum scrutTCon (cons !! k))
                    <$> typeOfAltsEnum scrutTCon cons alts
                DataRecord{} -> (,,) 1 (const CPDefault) <$> typeOfAltsOnlyDefault scrutType alts
-                -- TODO https://github.com/digital-asset/daml/issues/10810
-                DataInterface -> error "interfaces are not implemented"
+                DataInterface -> (,,) 1 (const CPDefault) <$> typeOfAltsOnlyDefault scrutType alts
        TUnit -> (,,) 1 (const CPUnit) <$> typeOfAltsUnit alts
        TBool -> (,,) 2 (CPBool . toEnum) <$> typeOfAltsBool alts
        TList elemType -> (,,) 2 ([CPNil, CPCons wildcard wildcard] !!) <$> typeOfAltsList elemType alts
@ -773,9 +772,20 @@ checkDefTypeSyn DefTypeSyn{synParams,synType} = do
  where
    base = checkType synType KStar

+
+checkIface :: MonadGamma m => DefInterface -> m ()
+checkIface DefInterface{intName, intChoices} = do
+  checkUnique (EDuplicateInterfaceChoiceName intName) $ NM.names intChoices
+  forM_ intChoices checkIfaceChoice
+
+checkIfaceChoice :: MonadGamma m => InterfaceChoice -> m ()
+checkIfaceChoice InterfaceChoice{ifcArgType,ifcRetType} = do
+  checkType ifcArgType KStar
+  checkType ifcRetType KStar
+
 -- | Check that a type constructor definition is well-formed.
-checkDefDataType :: MonadGamma m => DefDataType -> m ()
-checkDefDataType (DefDataType _loc _name _serializable params dataCons) = do
+checkDefDataType :: MonadGamma m => Module -> DefDataType -> m ()
+checkDefDataType m (DefDataType _loc name _serializable params dataCons) = do
  checkUnique EDuplicateTypeParam $ map fst params
  mapM_ (checkKind . snd) params
  foldr (uncurry introTypeVar) base params
@ -788,8 +798,9 @@ checkDefDataType (DefDataType _loc _name _serializable params dataCons) = do
      DataEnum names -> do
        unless (null params) $ throwWithContext EEnumTypeWithParams
        checkUnique EDuplicateConstructor names
-      -- TODO https://github.com/digital-asset/daml/issues/10810
-      DataInterface -> error "interfaces are not implemented"
+      DataInterface -> do
+        unless (null params) $ throwWithContext EInterfaceTypeWithParams
+        void $ inWorld $ lookupInterface (Qualified PRSelf (moduleName m) name)

 checkDefValue :: MonadGamma m => DefValue -> m ()
 checkDefValue (DefValue _loc (_, typ) _noParties (IsTest isTest) expr) = do
@ -813,8 +824,7 @@ checkTemplateChoice tpl (TemplateChoice _loc _ _ controllers mbObservers selfBin
    checkExpr upd (TUpdate retType)

 checkTemplate :: MonadGamma m => Module -> Template -> m ()
-checkTemplate m t@(Template _loc tpl param precond signatories observers text choices mbKey _implements) = do
-  -- TODO https://github.com/digital-asset/daml/issues/10810 check implements
+checkTemplate m t@(Template _loc tpl param precond signatories observers text choices mbKey implements) = do
  let tcon = Qualified PRSelf (moduleName m) tpl
  DefDataType _loc _naem _serializable tparams dataCons <- inWorld (lookupDataType tcon)
  unless (null tparams) $ throwWithContext (EExpectedTemplatableType tpl)
@ -826,9 +836,27 @@ checkTemplate m t@(Template _loc tpl param precond signatories observers text ch
    withPart TPAgreement $ checkExpr text TText
    for_ choices $ \c -> withPart (TPChoice c) $ checkTemplateChoice tcon c
  whenJust mbKey $ checkTemplateKey param tcon
+  forM_ implements $ checkIfaceImplementation (moduleName m) tcon
  where
    withPart p = withContext (ContextTemplate m t p)

+checkIfaceImplementation ::
+     MonadGamma m
+  => ModuleName
+  -> Qualified TypeConName
+  -> Qualified TypeConName
+  -> m ()
+checkIfaceImplementation modName tplTcon ifTcon
+  | Qualified PRSelf m _tconName <- ifTcon
+  , m == modName = do
+    DefInterface {intChoices} <- inWorld $ lookupInterface ifTcon
+    forM_ intChoices $ \InterfaceChoice {ifcName, ifcConsuming, ifcArgType, ifcRetType} -> do
+      TemplateChoice {chcConsuming, chcArgBinder, chcReturnType} <- inWorld $ lookupChoice (tplTcon, ifcName)
+      unless (chcConsuming == ifcConsuming) $ throwWithContext $ EBadInterfaceChoiceImplConsuming ifcName ifcConsuming chcConsuming
+      unless (alphaType (snd chcArgBinder) ifcArgType) $ throwWithContext $ EBadInterfaceChoiceImplArgType ifcName ifcArgType (snd chcArgBinder)
+      unless (alphaType chcReturnType ifcRetType) $ throwWithContext $ EBadInterfaceChoiceImplRetType ifcName ifcRetType chcReturnType
+  | otherwise = throwWithContext $ EForeignInterfaceImplementation ifTcon
+
 _checkFeature :: MonadGamma m => Feature -> m ()
 _checkFeature feature = do
    version <- getLfVersion
@ -858,11 +886,11 @@ checkDefException m DefException{..} = do
 -- The type checker for expressions relies on the fact that data type
 -- definitions do _not_ contain free variables.
 checkModule :: MonadGamma m => Module -> m ()
-checkModule m@(Module _modName _path _flags synonyms dataTypes values templates exceptions _interfaces) = do
-  -- TODO https://github.com/digital-asset/daml/issues/10810 check interfaces
+checkModule m@(Module _modName _path _flags synonyms dataTypes values templates exceptions interfaces) = do
  let with ctx f x = withContext (ctx x) (f x)
  traverse_ (with (ContextDefTypeSyn m) checkDefTypeSyn) synonyms
-  traverse_ (with (ContextDefDataType m) checkDefDataType) dataTypes
+  traverse_ (with (ContextDefDataType m) $ checkDefDataType m) dataTypes
  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
--- a/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs
+++ b/compiler/daml-lf-tools/src/DA/Daml/LF/TypeChecker/Error.hs
@ -29,6 +29,7 @@ data Context
  | ContextTemplate !Module !Template !TemplatePart
  | ContextDefValue !Module !DefValue
  | ContextDefException !Module !DefException
+  | ContextDefInterface !Module !DefInterface

 data TemplatePart
  = TPWhole
@ -128,6 +129,15 @@ data Error
  | EForbiddenNameCollision !T.Text ![T.Text]
  | ESynAppWrongArity       !DefTypeSyn ![Type]
  | ENatKindRightOfArrow    !Kind
+  | EInterfaceTypeWithParams
+  | EMissingInterfaceDefinition !TypeConName
+  | EDuplicateInterfaceChoiceName !TypeConName !ChoiceName
+  | EUnknownInterface !TypeConName
+  | EMissingInterfaceChoice !ChoiceName
+  | EBadInterfaceChoiceImplConsuming !ChoiceName !Bool !Bool
+  | EBadInterfaceChoiceImplArgType !ChoiceName !Type !Type
+  | EBadInterfaceChoiceImplRetType !ChoiceName !Type !Type
+  | EForeignInterfaceImplementation !(Qualified TypeConName)

 contextLocation :: Context -> Maybe SourceLoc
 contextLocation = \case
@ -137,6 +147,7 @@ contextLocation = \case
  ContextTemplate _ t _  -> tplLocation t
  ContextDefValue _ v    -> dvalLocation v
  ContextDefException _ e -> exnLocation e
+  ContextDefInterface _ i -> intLocation i

 errorLocation :: Error -> Maybe SourceLoc
 errorLocation = \case
@ -156,6 +167,8 @@ instance Show Context where
      "value " <> show (moduleName m) <> "." <> show (fst $ dvalBinder v)
    ContextDefException m e ->
      "exception " <> show (moduleName m) <> "." <> show (exnName e)
+    ContextDefInterface m i ->
+      "interface " <> show (moduleName m) <> "." <> show (intName i)

 instance Show TemplatePart where
  show = \case
@ -224,6 +237,7 @@ instance Pretty Error where
    EDuplicateModule mname -> "duplicate module: " <> pretty mname
    EDuplicateScenario name -> "duplicate scenario: " <> pretty name
    EEnumTypeWithParams -> "enum type with type parameters"
+    EInterfaceTypeWithParams -> "interface type with type parameters"
    EExpectedRecordType tapp ->
      vcat [ "expected record type:", "* found: ", nest 4 $ string (show tapp) ]
    EFieldMismatch tapp rexpr ->
@ -362,6 +376,34 @@ instance Pretty Error where
        [ "Kind is invalid: " <> pretty k
        , "Nat kind is not allowed on the right side of kind arrow."
        ]
+    EMissingInterfaceDefinition iface ->
+      "Missing interface definition for interface type: " <> pretty iface
+    EDuplicateInterfaceChoiceName iface choice ->
+      "Duplicate choice name '" <> pretty choice <> "' 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 ->
+      vcat
+      [ "Choice implementation and interface definition for " <> pretty ch <> " differ in consuming/non-consuming behaviour."
+      , "Expected: " <> prettyConsuming ifaceConsuming
+      , "But got: " <> prettyConsuming tplConsuming
+      ]
+    EBadInterfaceChoiceImplArgType ch ifaceArgType tplArgType ->
+      vcat
+      [ "Choice implementation and interface definition for " <> pretty ch <> " differ in argument type."
+      , "Expected: " <> pretty ifaceArgType
+      , "But got: " <> pretty tplArgType
+      ]
+    EBadInterfaceChoiceImplRetType ch ifaceRetType tplRetType ->
+      vcat
+      [ "Choice implementation and interface definition for " <> pretty ch <> " differ in return type."
+      , "Expected: " <> pretty ifaceRetType
+      , "But got: " <> pretty tplRetType
+      ]
+    EForeignInterfaceImplementation tcon -> "The definition and implementation for the interface " <> pretty tcon <> " need to be in the same module."
+
+prettyConsuming :: Bool -> Doc ann
+prettyConsuming consuming = if consuming then "consuming" else "non-consuming"

 instance Pretty Context where
  pPrint = \case
@ -377,6 +419,8 @@ instance Pretty Context where
      hsep [ "value", pretty (moduleName m) <> "." <> pretty (fst $ dvalBinder v) ]
    ContextDefException m e ->
      hsep [ "exception", pretty (moduleName m) <> "." <> pretty (exnName e) ]
+    ContextDefInterface m i ->
+      hsep [ "interface", pretty (moduleName m) <> "." <> pretty (intName i)]

 toDiagnostic :: DiagnosticSeverity -> Error -> Diagnostic
 toDiagnostic sev err = Diagnostic