使 GHC 从一种类型族约束中推断出另一种类型族约束

Question

我有几个应该暗示/包含彼此的约束/类型族：

{-# 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 ()

这会导致以下编译器错误：

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
   |       ^^^

我知道编译器在一般情况下无法检查一种类型系列中的映射是否意味着另一种类型系列中的映射，但是我可以做些什么来帮助它推断出这一点吗？就像例如输入类层次结构，或使用像

MoreGeneric t = LessGeneric t ~ 'True => 'True

这样的约束？

Answer 1

我发现可以通过引入一个包含两者的附加 ConstraintKind

IsLessGeneric

并使用它来代替

LessGeneric

:

工作示例：

{-# 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                               -- Wrong, MoreGeneric t can't be deduced from LessGeneric t

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

main = print $ foo (0.0 :: Float)