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
?
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)