So, I’ve been playing a bit with the ideas from the `trees that grow`

paper, and I’ve stumbled into something I don’t quite get.

Consider the following silly existential:

```
type family SomeX (tag :: Type ) (x :: Type) :: Type
data Some tag x where
Some :: SomeX tag x -> x -> Some tag ()
```

If we let:

```
-- Proof carries a prof for `psi a`
data Proof (psi :: k -> Constraint) (a :: k) where
P :: psi a => Proof psi a
```

Then we can “inject” constraints by:

```
data Foo
type instance SomeX Foo x = (Proof Show x)
```

But, if I try to make a pattern, it throws a compilation error:

```
-- Doesn't work 'x' does not unify with 'x1'
pattern SomeFoo :: (Show x) => x -> Some Foo ()
pattern SomeFoo x = Some P x
```

I thought that this unidirectional pattern is supposed to work as an ordinary (possibly smart) constructor. If i “downgrade” it to an ordinary function, it compiles as expected:

```
someFoo :: (Show x) => x -> Some Foo ()
someFoo x = Some P x
```