Wow. Essentially this example relies on the fact that *all* kinds are open (and is a good example of code that is rarely seen outside of a dynamically typed language). Maybe better support for reflection would help.

I see. Thanks for the clarification. Without `Stuck`

you could define

```
oops2 :: forall (s :: Type -> Type -> Type -> (Type,Type)). Int -> Bool
oops2 = castWith (hmm @Int @Int @(s Bool Bool Bool))
```

but that wouldn't be as bad, perhaps(?)

Here, you use `Stuck`

to inhabit that kind, which is a fishy step.

I guess I don't understand your example.

Is this what you are thinking in the typing of `oops`

:

The instantiation of `hmm`

gives us

```
F Int Int (Stuck Bool Bool Bool) :~:
F Int Int ((,) (Stuck Bool Bool Bool) (Stuck Bool Bool Bool))
```

Furthermore, in the RHS: `F Int Int (Stuck Bool Bool Bool)`

matches against `F x y (f a b c)`

to produce `Int`

and in the LHS: `F Int Int ((,) (Stuck Bool Bool Bool) (Stuck Bool Bool Bool))`

is apart from the first pattern, so matches the second pattern to produce `Bool`

. So that gives us `Int :~: Bool`

?

However, I don't think that the RHS reduction should hold. Why should `Stuck Bool Bool Bool`

match against `(f a b c)`

? Shouldn't it be stuck?

@RyanGlScott is this a bug? I wouldn't expect `F x y (Stuck a b c)`

to be apart from
`F x y (f a b c)`

. So it should just be stuck.

Or, do we need matchable kinds to rule it out?