Make GHC deduce one type family constraint from another

I have several constraints/type families that are supposed to imply/contain eachother:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind (Type)

type family MoreGeneric (t :: Type) :: Bool where
  MoreGeneric Int = 'True
  MoreGeneric Float = 'True
  MoreGeneric _ = 'False

type family LessGeneric (t :: Type) :: Bool where
  LessGeneric Float = 'True
  LessGeneric _ = 'False

foo :: LessGeneric t ~ 'True => t -> ()
foo = bar                               -- Wrong, MoreGeneric t can't be deduced from LessGeneric t

bar :: MoreGeneric t ~ 'True => t -> ()
bar = const ()

Which causes the following compiler error:

Main.hs:16:7: error: [GHC-05617]
    • Could not deduce ‘MoreGeneric t ~ True’
        arising from a use of ‘bar’
      from the context: LessGeneric t ~ True
        bound by the type signature for:
                   foo :: forall t. (LessGeneric t ~ True) => t -> ()
        at Main.hs:15:1-39
    • In the expression: bar
      In an equation for ‘foo’: foo = bar
    • Relevant bindings include foo :: t -> () (bound at Main.hs:16:1)
   |
16 | foo = bar
   |       ^^^

I understand that the compiler can not check whether a mapping in one type family implies a mapping in another type family in the general case, but is there anything I can do to help it deduce that? Like e.g. type class hierarchies, or using a constraint like MoreGeneric t = LessGeneric t ~ 'True => 'True?

Solution

I found out that it is possible by introducing an additional ConstraintKind IsLessGeneric that contains both and using that instead of LessGeneric:

Working example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind (Type)

type family MoreGeneric (t :: Type) :: Bool where
  MoreGeneric Int = 'True
  MoreGeneric Float = 'True
  MoreGeneric _ = 'False

type family LessGeneric (t :: Type) :: Bool where
  LessGeneric Float = 'True
  LessGeneric _ = 'False

type IsLessGeneric t = (MoreGeneric t ~ 'True, LessGeneric t ~ 'True)

foo :: IsLessGeneric t => t -> ()
foo = bar

bar :: MoreGeneric t ~ 'True => t -> ()
bar = const ()

main = print $ foo (0.0 :: Float)