Illegal polymorphic type error

Hey,

I’m trying to do the following:

module Main where

import DA.Record (HasField(..))

data Foo m ctx = Foo with
    bar : forall ctx. HasField "bar_field" ctx Bool => m ctx
    baz : forall ctx. HasField "baz_field" ctx Bool => m ctx

But I get the following errors:

/.../daml/Main.daml:1:1: error:
    • Illegal polymorphic type:
        forall ctx. HasField "bar_field" ctx Bool => m ctx
    • In the instance declaration for
        ‘HasField "bar" (Foo m ctx) (forall ctx.
                                     HasField "bar_field" ctx Bool => m ctx)’
/.../daml/Main.daml:1:1: error:
    • Illegal polymorphic type:
        forall ctx. HasField "baz_field" ctx Bool => m ctx
    • In the instance declaration for
        ‘HasField "baz" (Foo m ctx) (forall ctx.
                                     HasField "baz_field" ctx Bool => m ctx)’

What does this error mean? Thank you!

The key is in this part

the instance declaration for
        ‘HasField "bar" (Foo m ctx) (forall ctx.
                                     HasField "bar_field" ctx Bool => m ctx)’

When you define a record type in Daml, you always get an instance of HasField for each field therein; this has nothing to do with your own references of HasField. So the HasField "bar" ... is the one Daml is trying to define, and the other HasField in the above quote is the one you wrote.

damlc doesn’t check in advance whether the resulting HasField instance follows the rules, because chances are if you write something that breaks them, you’re trying to do something expert-level.

You can avoid this specific error by defining a variant type instead, if you are doing something that is otherwise allowed. But I’m not sure you can get the effects you want, based on the following modification of what you’re doing; maybe someone can refine this into something that works.

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

type BarBaz ctx = (HasField "bar_field" ctx Bool,
    HasField "baz_field" ctx Bool)

-- this is a variant, thus avoiding record type stuff
-- you can put a tuple there too
data Foo m ctx = Foo (BarBaz ctx => m ctx)

cata : forall m ctx z. (BarBaz ctx => m ctx -> z) -> Foo m ctx -> z
cata k (Foo c) = k c
--   • No instance for (HasField "bar_field" ctx Bool)
--   arising from a use of ‘k’
--   • In the expression: k c
--   In an equation for ‘cata’: cata k (Foo c) = k c

The following works in Daml and requires no extensions to be enabled

module Test where

import DA.Record (HasField(..))

data Foo m ctx = Foo with
    bar : BarField m
    baz : BazField m

newtype BarField m = BarField (forall ctx. HasField "bar_field" ctx Bool => m ctx)
newtype BazField m = BazField (forall ctx. HasField "baz_field" ctx Bool => m ctx)

Note however, that your ctx variable isn’t actually used because you’re quantifying universally over it in the field types.

My assumption was that @Krisztian_Pinter actually wanted to refer to the ctx tparam to Foo in the constraints, but was trying to get things to compile. (Which I think you need ScopedTypeVariables to get to work.)

You can’t constraint ctx if it’s a type parameter rather than existentially or universally quantified. There used to be (and I believe it technically still exists) an extension in Haskell (but not Daml, at least not in a usable form) called DataTypeContexts but it didn’t do what anyone expected it to do or wanted it to do so these days it sees absolutely no usage.

Instead if that’s what you want add a constraint where you use the type rather than in the type definition.

DataTypeContexts doesn’t do what people expected, but GHC does let you do the thing that people were probably expecting. Which is my guess as to what @Krisztian_Pinter was trying to do.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Test where

data LiftedEq ctx where
  LiftedEq :: Eq ctx => LiftedEq ctx

-- cata is not constrained, Eq c must come from the unpacked 2nd arg
cata :: forall ctx z. (forall c. (c ~ ctx, Eq c) => z) -> LiftedEq ctx -> z
cata k LiftedEq = k

-- edit: more to the point
eq :: LiftedEq a -> a -> a -> Bool
eq LiftedEq = (==)

On the other hand if my guess was wrong this is all just type fun now and @cocreature 's earlier answer is perfectly good :slight_smile:

I don’t even understand what you people are trying to do, let alone how you do it.

I find it a tiny bit reassuring to see that you’re not sure you understand what each other is trying to do either.

Thank you for all the replies!

I’ve been working to provide an example that actually represents the problem to be solved, which is not trivial when part of the problem is the complexity of the system. Here it is:

module Storage where

template Foo with
    x: Int
    b: Bool
    party: Party
  where
    signatory party

type FooId = ContractId Foo

data MonolithicContext = MonolithicContext with
    queryA : Int -> Update FooId
    queryB : Text -> Update FooId
    queryC : Bool -> Update FooId
--  ...
--  queryZ, many fields here

data Storage1 m = Storage1 with
    queryA: Int -> m Foo
    queryB: Text -> m Int
-- changing the above to
--  queryB: forall ctx. HasField "queryB" ctx (Text -> m Int) => ctx -> Text -> m Int
-- causes Daml to give the `Illegal polymorphic type` error

data Storage2 m = Storage2 with
    queryC: Bool -> m Bool

mkStorage1 : MonolithicContext -> Storage1 MyActionStack
mkStorage1 ctx = Storage1 with
    queryA = fromContext ctx.queryA
    queryB = fmap (.x) . fromContext ctx.queryB

mkStorage2 : MonolithicContext -> Storage2 MyActionStack
mkStorage2 ctx = Storage2 with
    queryC = fmap (.b) . fromContext ctx.queryC

emptyContext = MonolithicContext with
    queryA = const . abort $ "queryA missing"
    queryB = const . abort $ "queryB missing"
    queryC = const . abort $ "queryC missing"
--  etc

data ServiceFoo m = ServiceFoo with
-- we would like to be able to show in the type signature with HasField constraints
--   exactly what data from the context is used by the service method
    businessLogic: Int -> m (Foo, Bool)

mkServiceFoo : forall m. Action m => Storage1 m -> Storage2 m -> ServiceFoo m
mkServiceFoo storage1 storage2 = ServiceFoo with
    businessLogic = \n -> do
        x <- storage1.queryA n
        y <- storage2.queryC False
        pure (x, y)

-- monolithic context instantiated for a ServiceFoo call
-- if a field is unintentionally omitted but would be used by a service we get an error
-- we would like to check for this statically by using HasField constraints
contextForServiceFoo = emptyContext with
    queryA = error "return contract Ids"   -- these values come from exercised choices
    queryC = error "return contract Ids"   -- these values come from exercised choices
--  queryB and D to Z is intentionally not provided because it's not used in ServiceFoo

contextForServiceBar = emptyContext with
    queryB = error "return contract Ids"   -- these values come from exercised choices
    queryC = error "return contract Ids"   -- these values come from exercised choices
--  queryA and D to Z is intentionally not provided because it's not used in ServiceBar

fromContext : forall t k. (Template t) => (k -> Update (ContractId t)) -> k -> MyActionStack t
fromContext = error "fromContext"

data MyActionStack a = MyActionStack (Update a)

instance Functor MyActionStack where
    fmap = error "fmap"


I’ve read through your example a few times but I still don’t understand what you’d like to write. If all you’re trying to work around is the type issue on queryB you can newtype it like I showed above.

Assuming there wasn’t a type error for the field, how would the rest of the code look like? If you can get it to typecheck in Haskell that mighgt also be useful reference.

Apologies, I went for brevity when I should have opted for clarity. Here is what the end result might look like:

module Storage2 where

import DA.Record (HasField(..))

template Foo with
    x: Int
    b: Bool
    party: Party
  where
    signatory party

type FooId = ContractId Foo

data Storage1 m = Storage1 with
    queryA: forall ctx. HasField "queryA" ctx (Int -> m Foo) => ctx -> Int -> m Foo
    queryB: forall ctx. HasField "queryB" ctx (Text -> m Int) => ctx -> Text -> m Int

data Storage2 m = Storage2 with
    queryC: forall ctx. HasField "queryC" ctx (Bool -> m Bool) => ctx -> Bool -> m Bool

mkStorage1 : Storage1 MyActionStack
mkStorage1 = Storage1 with
    queryA = \ctx -> fromContext ctx.queryA
    queryB = \ctx -> fmap (.x) . fromContext ctx.queryB

mkStorage2 : Storage2 MyActionStack
mkStorage2 = Storage2 with
    queryC = \ctx -> fmap (.b) . fromContext ctx.queryC

data ServiceFoo m = ServiceFoo with
    businessLogicBar: forall ctx.
        ( HasField "queryA" ctx (Int -> Update FooId)
        , HasField "queryC" ctx (Bool -> Update FooId)
        ) => ctx -> Int -> m (Foo, Bool)
    businessLogicBaz: forall ctx.
        ( HasField "queryC" ctx (Bool -> Update FooId)
        ) => ctx -> Int -> m (Foo, Bool)

mkServiceFoo : forall m. Action m => Storage1 m -> Storage2 m -> ServiceFoo m
mkServiceFoo storage1 storage2 = ServiceFoo with
    businessLogicBar = \ctx n -> do
        x <- storage1.queryA ctx n
        y <- storage2.queryC ctx False
        pure (x, y)

    businessLogicBaz = \ctx -> do
        y <- storage2.queryC ctx False
        pure $ not y

data ContextForBusinessLogicBar = ContextForBusinessLogicBar with
    queryA : Int -> Update FooId
    queryC : Bool -> Update FooId

data ContextForBusinessLogicBaz = ContextForBusinessLogicBaz with
    queryC : Bool -> Update FooId

contextForBusinessLogicBar = ContextForBusinessLogicBar with
    queryA = error "return contract Ids"   -- these values come from exercised choices
    queryC = error "return contract Ids"   -- these values come from exercised choices

contextForBusinessLogicBaz = ContextForBusinessLogicBaz with
    queryB = error "return contract Ids"   -- these values come from exercised choices

main = do
    let
        storage1 = mkStorage1
        storage2 = mkStorage2
        serviceFoo = mkServiceFoo storage1 storage2
    
    serviceFoo.businessLogicBar contextForBusinessLogicBar 123
    serviceFoo.businessLogicBaz contextForBusinessLogicBaz
    

fromContext : forall t k. (Template t) => (k -> Update (ContractId t)) -> k -> MyActionStack t
fromContext = error "fromContext"

data MyActionStack a = MyActionStack (Update a)

instance Functor MyActionStack where
    fmap = error "fmap"

So you can get this to typecheck after fixing a whole bunch of type errors and adding newtypes as needed. However, this seems like a lot of complexity with (to me) an unclear gain so I’d encourage trying to find a more direct way to implement this.

module Main where

import DA.Record (HasField(..))

template Foo with
    x: Int
    b: Bool
    party: Party
  where
    signatory party

type FooId = ContractId Foo

newtype StorageQuery m s a b t = StorageQuery (forall ctx. HasField s ctx (a -> Update (ContractId t)) => ctx -> a -> m b)

runQuery : StorageQuery m s a b t -> forall ctx. HasField s ctx (a -> Update (ContractId t)) => ctx -> a -> m b
runQuery (StorageQuery q) = q

data Storage1 m = Storage1 with
    queryA: StorageQuery m "queryA" Int Foo Foo
    queryB: StorageQuery m "queryB" Text Int Foo

data Storage2 m = Storage2 with
    queryC: StorageQuery m "queryC" Bool Bool Foo

mkStorage1 : Storage1 MyActionStack
mkStorage1 = Storage1 with
    queryA = StorageQuery $ \ctx -> fromContext ctx.queryA
    queryB = StorageQuery $ \ctx -> fmap (.x) . fromContext ctx.queryB

mkStorage2 : Storage2 MyActionStack
mkStorage2 = Storage2 with
    queryC = StorageQuery \ctx -> fmap (.b) . fromContext ctx.queryC

newtype BusinessLogicBar m = BusinessLogicBar (forall ctx. (HasField "queryA" ctx (Int -> Update FooId), HasField "queryC" ctx (Bool -> Update FooId)) => ctx -> Int -> m (Foo, Bool))

newtype BusinessLogicBaz m = BusinessLogicBaz (forall ctx. HasField "queryC" ctx (Bool -> Update FooId) => ctx -> Bool -> m Bool)

data ServiceFoo m = ServiceFoo with
    businessLogicBar: BusinessLogicBar m
    businessLogicBaz: BusinessLogicBaz m

mkServiceFoo : forall m. Action m => Storage1 m -> Storage2 m -> ServiceFoo m
mkServiceFoo storage1 storage2 = ServiceFoo with
    businessLogicBar = BusinessLogicBar $ \ctx n -> do
        x <- runQuery storage1.queryA ctx n
        y <- runQuery storage2.queryC ctx False
        pure (x, y)

    businessLogicBaz = BusinessLogicBaz $ \ctx b -> do
        y <- runQuery storage2.queryC ctx b
        pure (not y)

data ContextForBusinessLogicBar = ContextForBusinessLogicBar with
    queryA : Int -> Update FooId
    queryC : Bool -> Update FooId

data ContextForBusinessLogicBaz = ContextForBusinessLogicBaz with
    queryC : Bool -> Update FooId

contextForBusinessLogicBar = ContextForBusinessLogicBar with
    queryA = error "return contract Ids"   -- these values come from exercised choices
    queryC = error "return contract Ids"   -- these values come from exercised choices

contextForBusinessLogicBaz = ContextForBusinessLogicBaz with
    queryC = error "return contract Ids"   -- these values come from exercised choices

main = do
    let
        storage1 = mkStorage1
        storage2 = mkStorage2
        serviceFoo = mkServiceFoo storage1 storage2

    let BusinessLogicBar businessLogicBar = serviceFoo.businessLogicBar
    businessLogicBar contextForBusinessLogicBar 123
    let BusinessLogicBaz businessLogicBaz = serviceFoo.businessLogicBaz
    businessLogicBaz contextForBusinessLogicBaz False


fromContext : forall t k. (Template t) => (k -> Update (ContractId t)) -> k -> MyActionStack t
fromContext = error "fromContext"

newtype MyActionStack a = MyActionStack (Update a)
  deriving (Functor, Applicative, Action)
2 Likes

Thank you for your code example! I came to the same conclusion as well.

1 Like