Generate parametrized types to inject into evaluation context

[mastarija]

I want to have certain types available in my evaluation context. From the substitutions tutorial that's easy enough for simple types, and I can even use something like this declared $ inject @MySumType to generate Expr Src Void value of my type.

However, if I have a bit more complex type that has a type parameter, I can't use the ToDhall instance and have to manually write the type Expr.

Is there perhaps something that could help with this, or do I have to do it manually?

This is a bit cumbersome to write and maintain, especially if I have a lot of fields:

data MyData n = MyData
   { field1 :: n
   , field2 :: n
   ...
   }

typeRect :: Expr Src Void
typeRect = Lam Nothing (FunctionBinding Nothing "n" Nothing Nothing (Const Type)) $ Record $ DMap.fromList
    [ ("field1", RecordField Nothing "n" Nothing Nothing)
    , ("field2", RecordField Nothing "n" Nothing Nothing)
    ...
    ]

[Gabriella439]

There is not a good way to do this using the Haskell API, as far as I can tell.

[mastarija]

@Gabriella439 I was thinking a bit yesterday about this. I'm not sure what those "annotations" are for that I see sprinkled around, but maybe we can add annotation which tell us if this particular type was introduced by a type variable e.g.

data ExType v = ExType
{ field1 :: Double
, field2 :: v
}

So, when I use a dummy type with inject, e.g. declared $ inject @(ExType Double) the resulting Expr will contain info that the field2 received its Double type from the type variable v while field1 didn't. Then we could use a function that will read the Expr, find all of the dummy types that were introduced via a type variable, wrapp the whole value in lambda and replace dummy types with a variable.

I haven't worked with generics in a while, so I'm not sure if their API exposes enough information though.

Anyway, great library and language. I really like it.