Allow exercising choices on generic templates in a generic context (#2871)

* Allow exercising choices on generic templates in a generic context

Every `template T a_1 a_n` gets desugared into a `class TInstance a_1 ... a_n`,
an instance
```
(*)    instance TInstance a_1 ... a_n => Template (T a_1 ... a_n)
```
and instances `instance TInstance a_1 ... a_n => Choice (T a_1 ... a_n) C R`
for each choice `C`.

Thus, a _generic_ exercise of a choice on `T t_1 ... t_n` needs to have the
`TInstance t_1 ... t_n` constraint in scope. However, we want to keep the
existence of the `TInstance` class an implementation detail and not expose
it to our users. Instead we want our users to add a `Template (T t_1 ... t_n)`
constraint when they want to perform the generic exercise.

Due to the (*) instance above, the constraint `Template (T t_1 ... t_n)`
is satisfied if and only if the constraint `TInstance t_1 ... t_n` is
satisfied. For the intent described above it would be necessary that GHC
conlcudes the latter from the former. Unfortunately, GHC's type system only
allows for concluding the former from the latter.

Thus, we add a preprocessing step which rewrites all constraints of
the form `Template (T t_1 ... t_n)` into `TInstance t_1 ... t_n`.

* Add test for fetchByKey
This commit is contained in:
Martin Huschenbett 2019-09-11 11:41:21 +02:00 committed by mergify[bot]
parent a58cf857d4
commit 2411fdb0e0
4 changed files with 123 additions and 2 deletions

View File

@ -149,7 +149,7 @@ xExtensionsSet =
, ConstraintKinds
-- type classes
, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, TypeSynonymInstances
, DefaultSignatures, StandaloneDeriving, FunctionalDependencies, DeriveFunctor
, DefaultSignatures, StandaloneDeriving, FunctionalDependencies, DeriveFunctor, UndecidableSuperClasses
-- let generalization
, MonoLocalBinds
-- replacing primitives

View File

@ -9,6 +9,7 @@ module DA.Daml.Preprocessor
import DA.Daml.Preprocessor.Records
import DA.Daml.Preprocessor.Generics
import DA.Daml.Preprocessor.TemplateConstraint
import qualified "ghc-lib" GHC
import Outputable
@ -39,7 +40,7 @@ mayImportInternal =
damlPreprocessor :: Maybe String -> GHC.ParsedSource -> ([(GHC.SrcSpan, String)], GHC.ParsedSource)
damlPreprocessor mbPkgName x
| maybe False (isInternal ||^ (`elem` mayImportInternal)) name = ([], x)
| otherwise = (checkImports x ++ checkDataTypes x ++ checkModuleDefinition x, recordDotPreprocessor $ importDamlPreprocessor $ genericsPreprocessor mbPkgName x)
| otherwise = (checkImports x ++ checkDataTypes x ++ checkModuleDefinition x, recordDotPreprocessor $ importDamlPreprocessor $ genericsPreprocessor mbPkgName $ templateConstraintPreprocessor x)
where name = fmap GHC.unLoc $ GHC.hsmodName $ GHC.unLoc x
-- | No preprocessing. Used for generated code.

View File

@ -0,0 +1,83 @@
-- Copyright (c) 2019 The DAML Authors. All rights reserved.
-- SPDX-License-Identifier: Apache-2.0
-- | Every `template T a_1 a_n` gets desugared into a `class TInstance a_1 ... a_n`,
-- an instance
-- ```
-- (*) instance TInstance a_1 ... a_n => Template (T a_1 ... a_n)
-- ```
-- and instances `instance TInstance a_1 ... a_n => Choice (T a_1 ... a_n) C R`
-- for each choice `C`.
--
-- Thus, a _generic_ exercise of a choice on `T t_1 ... t_n` needs to have the
-- `TInstance t_1 ... t_n` constraint in scope. However, we want to keep the
-- existence of the `TInstance` class an implementation detail and not expose
-- it to our users. Instead we want our users to add a `Template (T t_1 ... t_n)`
-- constraint when they want to perform the generic exercise.
--
-- Due to the (*) instance above, the constraint `Template (T t_1 ... t_n)`
-- is satisfied if and only if the constraint `TInstance t_1 ... t_n` is
-- satisfied. For the intent described above it would be necessary that GHC
-- conlcudes the latter from the former. Unfortunately, GHC's type system only
-- allows for concluding the former from the latter.
--
-- Thus, we add a preprocessing step which rewrites all constraints of
-- the form `Template (T t_1 ... t_n)` into `TInstance t_1 ... t_n`.
module DA.Daml.Preprocessor.TemplateConstraint (
templateConstraintPreprocessor
) where
import "ghc-lib" GHC
import "ghc-lib-parser" BasicTypes
import "ghc-lib-parser" OccName
import "ghc-lib-parser" RdrName
import Data.Generics.Uniplate.Data
templateConstraintPreprocessor :: ParsedSource -> ParsedSource
templateConstraintPreprocessor = fmap onModule
onModule :: HsModule GhcPs -> HsModule GhcPs
onModule = transformBi onType . transformBi onTyClDecl
-- | The contexts of class and data definitions do not live inside an
-- `HsType` but in their respective AST nodes. That's why we need to chase
-- them down separately.
onTyClDecl :: TyClDecl GhcPs -> TyClDecl GhcPs
onTyClDecl decl = case decl of
ClassDecl{tcdCtxt} -> decl{tcdCtxt = fmap onContext tcdCtxt}
DataDecl{tcdDataDefn = defn@HsDataDefn{dd_ctxt}} -> decl{tcdDataDefn = defn{dd_ctxt = fmap onContext dd_ctxt}}
_ -> decl
onType :: HsType GhcPs-> HsType GhcPs
onType = \case
HsQualTy ext ctxt t -> HsQualTy ext (fmap onContext ctxt) (fmap onType t)
t -> descend onType t
onContext :: HsContext GhcPs -> HsContext GhcPs
onContext = map . fmap $ \case
HsAppTy _ (L _ (HsTyVar _ _ (L _ (occNameString . rdrNameOcc -> "Template")))) (L _ t)
| Just t' <- instantifyType t
-> t'
t -> t
-- | Check if the type is of the form `T t_1 ... t_n` for some type constructor
-- `T` and return the constraint `TInstance t_1 ... t_n` in case it is.
instantifyType :: HsType GhcPs -> Maybe (HsType GhcPs)
instantifyType = \case
HsTyVar ext NotPromoted (L loc x) -> HsTyVar ext NotPromoted . L loc <$> instantifyRdrName x
HsAppTy ext (L loc t1) t2 -> (\t1' -> HsAppTy ext (L loc t1') t2) <$> instantifyType t1
HsParTy ext (L loc t) -> HsParTy ext . L loc <$> instantifyType t
_ -> Nothing
instantifyRdrName :: RdrName -> Maybe RdrName
instantifyRdrName = \case
Unqual occ -> Unqual <$> instantifyOccName occ
Qual m occ -> Qual m <$> instantifyOccName occ
Orig{}-> Nothing
Exact{} -> Nothing
instantifyOccName :: OccName -> Maybe OccName
instantifyOccName occ
| occNameSpace occ == tcName = Just $ mkOccNameFS clsName $ occNameFS occ <> "Instance"
| otherwise = Nothing

View File

@ -0,0 +1,37 @@
-- Copyright (c) 2019 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
-- SPDX-License-Identifier: Apache-2.0
{-# LANGUAGE AllowAmbiguousTypes #-}
-- Check that choices on generic templates can be exercised in generic contexts.
daml 1.2
module GenericChoice where
template Foo c with
p : Party
a : c
where
signatory p
key p : Party
maintainer key
choice Delete: ()
controller p
do pure ()
template Template (Foo c) => FooTrigger c with
p : Party
where
signatory p
choice Trigger: () with
fooCid: ContractId (Foo c)
controller p
do exercise fooCid Delete
deleteFoo : Template (Foo c) => ContractId (Foo c) -> Update ()
deleteFoo fooCid = exercise fooCid Delete
deleteFooByKey : forall c. Template (Foo c) => Party -> Update ()
deleteFooByKey fooKey = do
(fooCid, _) <- fetchByKey @(Foo c) fooKey
exercise fooCid Delete