Should ExistentialQuantification language pragma be an error in Daml?

Questions
,
1

If I include this language pragma in a Daml file:

{-# LANGUAGE ExistentialQuantification  #-}

I get the following compiler warning:

  Modules compiled with the ExistentialQuantification language extension
  might not work properly with data-dependencies. This might stop the
  whole package from being extensible or upgradable using other versions
  of the SDK. Use this language extension at your own risk.

However, based on this response to an earlier question, existential types are not supported at all in Daml.

Is there any reason why using this language pragma in Daml shouldn’t be an error rather than a warning? Is this a warning for backwards compatibility reasons?

1 Like
2

I don’t think there is a good reason, this is more of an artifact of the implementation:

The warnings on extensions are based on an allow list of extensions that we know are safe. Everything else produces this type of warning.

In addition to that, we blow up when converting to LF on unsupported features some of which can only be used via extensions. If you actually try to write an existential type you will see an error (although it’s not quite as clear that it blows up due to ExistentialQuantification from the error).

Having a deny list of extensions that we know don’t work in Daml seems very sensible and would at least produce nicer error messages.

2 Likes
3

This isn’t true; they are supported, just not as serializable data, just like rank-N types.

I recently considered using them for a lazy list, for which they worked fine but I chose an alternative design. This compiles fine with ExistentialQuantification

data Apply a = Apply (forall e. (e -> a, e))

runApply : Apply a -> a
runApply (Apply (f, e)) = f e

You just have to avoid having it generate record types.

As such, I request caution with the definition of such a “deny list”, as it isn’t immediately obvious which extensions really don’t work.

2 Likes
4 
data Apply a = Apply (forall e. (e -> a, e))

That’s not an existential type, that’s a RankNType. You don’t need any extension to use that because we turn on RankNTypes by default.

The existential version is

data Apply a = forall e. Apply (e -> a, e)

which fails to compile with

Failure to process DAML program, this feature is not currently supported.
Type variable not bound in conversion environment with {abstract:var}.
2 Likes
5

Ugh, right, I can’t believe I got that far in the earlier development without noticing that I had them mixed up.

2 Likes