haskellconstraintstype-families

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)