GHC unexpectedly reports variable as untouchable and suggests -XAmbiguousTypes after enabling constraints via associated type family under rank2 argument

Sorry for long subject, couldn't express it in a more succinct way :)

Please consider the following program. I have defined function hzygo without any issues, but after slight generalisation GHC doesn't accept hzygo1 any more. Please see the error message below the program. However, slightly more general hzygo2 is accepted.

{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE NoStarIsType        #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}

module Main (main) where

import Data.Kind
import Data.Functor.Product

hfst :: Product a b ix -> a ix
hfst (Pair a _) = a

hsnd :: Product a b ix -> b ix
hsnd (Pair _ b) = b

newtype HFix (f :: (k -> Type) -> (k -> Type)) (ix :: k) =
  HFix { unHFix :: f (HFix f) ix }


class HFunctor (f :: (k -> Type) -> (k -> Type)) where
  hmap :: (forall ix. a ix -> b ix) -> (forall ix. f a ix -> f b ix)

hcata
  :: forall f a.
     HFunctor f
  => (forall ix. f a ix -> a ix)
  -> (forall ix. HFix f ix -> a ix)
hcata alg = go
  where
    go :: forall ix. HFix f ix -> a ix
    go = alg . hmap go . unHFix

hzygo
  :: forall f a b.
     HFunctor f
  => (forall ix. f (Product a b) ix -> a ix)
  -> (forall ix. f b ix             -> b ix)
  -> (forall ix. HFix f ix          -> a ix)
hzygo alga algb = hfst . hcata alg
  where
    alg :: f (Product a b) ix -> Product a b ix
    alg x = Pair (alga x) (algb $ hmap hsnd x)

class Constrained (f :: (k1 -> k2) -> (k1 -> k2)) where
  type Constraints f :: k1 -> Constraint

class Constrained f => HFunctor' (f :: (k -> Type) -> (k -> Type)) where
  hmap'
    :: (forall ix. Constraints f ix => a ix -> b ix)
    -> (forall ix. Constraints f ix => f a ix -> f b ix)

hcata'
  :: forall f a.
     HFunctor' f
  => (forall ix. Constraints f ix => f a ix -> a ix)
  -> (forall ix. Constraints f ix => HFix f ix -> a ix)
hcata' alg = go
  where
    go :: forall ix. Constraints f ix => HFix f ix -> a ix
    go = alg . hmap' go . unHFix

hzygo2
  :: forall f a b.
     HFunctor' f
  => (forall ix. Constraints f ix => f (Product a b) ix -> a ix)
  -> (forall ix. Constraints f ix => f b ix             -> b ix)
  -> (forall ix. Constraints f ix => HFix f ix          -> Product a b ix)
hzygo2 alga algb = hcata' alg
  where
    alg :: Constraints f ix => f (Product a b) ix -> Product a b ix
    alg x = Pair (alga x) (algb $ hmap' hsnd x)

hzygo1
  :: forall f a b.
     HFunctor' f
  => (forall ix. Constraints f ix => f (Product a b) ix -> a ix)
  -> (forall ix. Constraints f ix => f b ix             -> b ix)
  -> (forall ix. Constraints f ix => HFix f ix          -> a ix)
hzygo1 alga algb = hfst . hcata' alg
  where
    alg :: Constraints f ix => f (Product a b) ix -> Product a b ix
    alg x = Pair (alga x) (algb $ hmap' hsnd x)


main :: IO ()
main =
  pure ()

$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.6.5
$ ghc -c Main.hs

Main.hs:77:6: error:
    • Couldn't match type ‘b0’ with ‘b’
        ‘b0’ is untouchable
          inside the constraints: Constraints f ix1
          bound by the type signature for:
                     hzygo' :: forall (ix1 :: k1).
                               Constraints f ix1 =>
                               f b0 ix1 -> b0 ix1
          at Main.hs:(77,6)-(81,64)
      ‘b’ is a rigid type variable bound by
        the type signature for:
          hzygo' :: forall k1 (f :: (k1 -> *) -> k1 -> *) (a :: k1
                                                                -> *) (b :: k1 -> *).
                    HFunctor f =>
                    (forall (ix1 :: k1).
                     Constraints f ix1 =>
                     f (Product a b) ix1 -> a ix1)
                    -> (forall (ix1 :: k1). Constraints f ix1 => f b ix1 -> b ix1)
                    -> forall (ix :: k1). Constraints f ix => HFix f ix -> a ix
        at Main.hs:(77,6)-(81,64)
      Expected type: f b0 ix1 -> b0 ix1
        Actual type: f b ix1 -> b ix1
    • In the ambiguity check for ‘hzygo'’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        hzygo' :: forall f a b.
                  HFunctor f =>
                  (forall ix. Constraints f ix => f (Product a b) ix -> a ix)
                  -> (forall ix. Constraints f ix => f b ix -> b ix)
                     -> (forall ix. Constraints f ix => HFix f ix -> a ix)
   |
77 |   :: forall f a b.
   |      ^^^^^^^^^^^^^...

Main.hs:77:6: error:
    • Couldn't match type ‘b0’ with ‘b’
        ‘b0’ is untouchable
          inside the constraints: Constraints f ix1
          bound by the type signature for:
                     hzygo' :: forall (ix1 :: k1).
                               Constraints f ix1 =>
                               f (Product a b0) ix1 -> a ix1
          at Main.hs:(77,6)-(81,64)
      ‘b’ is a rigid type variable bound by
        the type signature for:
          hzygo' :: forall k1 (f :: (k1 -> *) -> k1 -> *) (a :: k1
                                                                -> *) (b :: k1 -> *).
                    HFunctor f =>
                    (forall (ix1 :: k1).
                     Constraints f ix1 =>
                     f (Product a b) ix1 -> a ix1)
                    -> (forall (ix1 :: k1). Constraints f ix1 => f b ix1 -> b ix1)
                    -> forall (ix :: k1). Constraints f ix => HFix f ix -> a ix
        at Main.hs:(77,6)-(81,64)
      Expected type: f (Product a b0) ix1 -> a ix1
        Actual type: f (Product a b) ix1 -> a ix1
    • In the ambiguity check for ‘hzygo'’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        hzygo' :: forall f a b.
                  HFunctor f =>
                  (forall ix. Constraints f ix => f (Product a b) ix -> a ix)
                  -> (forall ix. Constraints f ix => f b ix -> b ix)
                     -> (forall ix. Constraints f ix => HFix f ix -> a ix)
   |
77 |   :: forall f a b.
   |      ^^^^^^^^^^^^^...