Alright, I found a nice example of how things fail. See this addition to the previous code: ```Haskell -- | This is the right tensorial strength of a functor with respect to tupling. deasil :: Functor functor => (functor left, right) -> functor (left, right) deasil (functor, value) = fmap (, value) functor deasilsA :: forall peels seed value. ( Squeezy seed (Dress seed peels) peels , ForAll peels Functor ) => (Dress seed peels, value) -> Squeezed peels (seed, value) deasilsA = deasil . first squeeze deasilsB :: forall peels seed value. ( Squeezy (seed , value) (Dress (seed, value) peels) peels ) => Squeezed peels (seed, value) -> Dress (seed, value) peels deasilsB = stretch deasils :: _ => (Dress seed peels, value) -> Dress (seed, value) peels deasils = deasilsB . deasilsA ``` What is the type of `deasils`? ``` % ghci-9.2.2 Squeeze.hs GHCi, version 9.2.2: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/kindaro/code/dotfiles/ghci.conf [1 of 1] Compiling Main ( Squeeze.hs, interpreted ) Ok, one module loaded. λ :type deasilsB . deasilsA deasilsB . deasilsA :: (ForAll peels Functor, Squeezy' seed (Dress seed peels) peels (Strip seed (Dress seed peels) == '[]), Squeezy' (seed, value) (Dress (seed, value) peels) peels (Strip (seed, value) (Dress (seed, value) peels) == '[])) => (Dress seed peels, value) -> Dress (seed, value) peels ``` Looks good, but… ``` λ f = deasilsB . deasilsA <interactive>:2:1: error: • Could not deduce: Dress seed0 peels0 ~ Dress seed peels ``` What is going on? How can I have my `deasils`? I tried attaching all kinds of type annotations, but nothing works so far. I do not even understand the problem. How is it that an expression can be typed, but cannot be assigned to a name? You can see the complete code at the gist [1]. [1]: https://gist.github.com/kindaro/6056f753bcf356ced96b817fee72533c/2823ec2792f...