Projecting existential variables

https://richarde.dev/papers/2021/exists/exists.pdf shows how we can project existential variables, using the expressions themselves to "non-generatively" introduce special skolems, rather than be confined to pattern matching and getting fresh skolems confined to scopes. These "applicative skolems" (to continue to borrow the ML functor terminology), are a nice thing to have with or without exists a. ... new "structural" existential types.

With lots of other hypothetical syntax:

data Foo where
  MkFoo :: forall a. Show a => a :: Foo

_1 :: Foo -> Type -- but indicate non-relevant somehow?
_2 :: forall (a :: Foo) -> Dict (Show (fst a))
_3 :: forall (a :: Foo) -> fst a

foo :: Foo -> String
foo f = case _2 a of
    Dict -> show x
  where
    type T = _1 a
    x :: T = _3 a 

_2 requires case, but that is only because of Dict. We could imagine explicit dictionary arguments or something instead, but that is separate.

The paper also goes into term-level constraints, which seems good for Dependent Haskell in general, but I suppose that should also have a separate issue.

CC @rae