Support for existentially quantified nats?

[emarzion]

Is there any plan to support existential quantification over nats in the future? For example, the following fairly reasonable code will compile but won't synthesize:

{-# LANGUAGE ExistentialQuantification #-}

module Test where

import Clash.Prelude

myvec :: Vec 4 Int
myvec = 1 :> 2 :> 3 :> 4 :> Nil

data Vec' a = forall n. KnownNat n => Vec' (Vec n a)

myvec' :: Vec' Int
myvec' = Vec' myvec

topEntity :: Vec' Int
topEntity = myvec'

I can understand where this could go awry in general, since existentially quantified vectors are more or less lists in disguise. However, in cases like the one above where the lengths are already determined at compile time, I would hope that there's a way that this could be handled.

Of course, the example above is silly, but there are times when it'd be nice to be able to have heterogeneous collections of vectors whose lengths are nonetheless fixed at compile time.

[christiaanb]

So in general the issue is when you have existentials at the very top of the function hierarchy; in all other cases Clash should already handle them through inlining and specialisation. We can basically distinguish four situations, where in the cases below Representable means we can infer from the type alone how many bits we need to represent values:

1. topEntity :: Existential The existential value is either a constant or undefined; it should be a trivial engineering issue to figure out the shape of the value to determine how many bits we need.

2. topEntity :: Representable -> Existential The existential value is either a constant, undefined, or created from the representable argument; not as trivial as situation 1, but hopefully still trivial.

3. topEntity :: Existential -> Representable This is where the difficulties, or even impossibilities start, as information needs to flow "backwards". It becomes like splitting coffee into clear water and dry ground coffee beans. For example the representable result might be an Int which we've gotten through a foldr over the existential Vec' Int; and this could get even worse: we might branch on the existential length and fold with addition for even-length vectors, and fold with multiplication for odd-length vectors.

We might however still be able to generate VHDL or (System)Verilog: we could generate HDL that uses a generic/parameter for the existential. But we would have two additional limitations:

• The existential must basically be always of type Nat, we can't parametrize over anything else in VHDL-1993 or Verilog-2001.
• We cannot do things like map (+) on the existential vector, i.e. have an intermediate result that has a non-representable type and can only be synthesized by unrolling the definition of the map function at the Clash/Haskell level.

4. topEntity :: Existential -> Existential Now, the existential result can be made out of the existential argument, and all hope for achieving synthesis seems completely lost.

So it seems that situations 1 and 2 seem trivial, but also somewhat useless, as we could've just used a representational type instead of an existential type. And then situations 3 and 4 seem to be extremely difficult or even impossible.

Do you perhaps have a larger example where existentials are used in a meaningful way at the very top level of your function hierarchy, and Clash is failing to synthesize? Or is your issue that you're using existential not at the very top, and Clash is still failing to synthesize?