Lift restriction that pattern matching on existentials must be strict
You can’t pattern-match on an existentially quantified constructor in a let or where group of bindings.
and later on
In general, you can only pattern-match on an existentially-quantified constructor in a case expression or in the patterns of a function definition. The reason for this restriction is really an implementation one. Type-checking binding groups is already a nightmare without existentials complicating the picture. Also an existential pattern binding at the top level of a module doesn’t make sense, because it’s not clear how to prevent the existentially-quantified type “escaping”. So for now, there’s a simple-to-state restriction. We’ll see how annoying it is.
I am here to tell you that I find it very much annoying.
In Darcs it forces us to use nested cases (with increasing indentation depth, bad). If we happen to be in a
do block, which is often the case, we can resort to
do Sealed xs <- read some patches Sealed qs <- read more patches ...
Here, I am using, as an example, an existential defined as
data Sealed a where Sealed :: a wX -> Sealed a
where the type variable
wX is a phantom type that symbolically stands for the range of the partial bijection represented by a patch.
This style is acceptable, though sometimes I would like to extract a piece of code and factor it into a local function and this doesn't work because of the let restriction. I usually find a work-around but it can be a hassle.
Anyway, lately I came across something that I really don't like. We use
unsafeInterleaveIO when reading hashed files from disk; this is okay because the file name determines the content, so these are essentially write-once, so nothing bad can happen. In order to preserve laziness I would like to say
do ~(Sealed xs) <- unsafeInterleaveIO $ read some patches ~(Sealed qs) <- unsafeInterleaveIO $ read more patches ...
and now GHC (8.6.5) tells me that I cannot do that. Without the laziness annotation, the pattern match on the Sealed constructor forces evaluation until we know at least that we have an actual Sealed, not bottom. And that may mean we must read a file, which we don't want to do, for efficiency, since it may not be needed at all. That's what the
unsafeInterleaveIO is for.
The only way to achieve laziness here is to use an unsafe coercion on the wX phantom type that allows us to pull out the existentially quantified content of a Sealed, then unconditionally re-seal it:
unsafeUnseal :: Sealed a -> a wX unsafeUnseal (Sealed a) = unsafeCoerce a ... do Sealed xs <- Sealed $ unsafeUnseal $ unsafeInterleaveIO $ read some patches Sealed qs <- Sealed $ unsafeUnseal $ unsafeInterleaveIO $ read more patches ...
This is quite an ugly hack.
I don't have a ready made proposal but I think you get the gist. Lift the above cited restriction, at least allow to use matching on an existentials inside a lazy pattern.