隐式建造单身人士

Question

我正在尝试隐式构建单例，然后将其传递到单身人士上的巫婆计算中。我想帮助GHC推断这种类型，但我还没有找到一种方法。

singletons [d| data Mood = Angry
                         | Sad
                         | Neutral
                         | Happy
                         | Excited deriving (Read, Eq, Ord, Show) |]

singletons [d| data Intensity = None
                              | Low
                              | Medium
                              | High
                              | Extreme deriving (Show, Read, Eq, Ord, Enum) |]


singletons [d| newtype MoodReport = MR (Mood, Intensity) deriving Show |]


moodReportToSing :: forall (a :: Mood) (b :: Intensity). (SingI a, SingI b) => MoodReport -> SMoodReport ('MR '(a,b))
moodReportToSing (MR (a,b)) = sing :: Sing ('MR '(a, b))


addSingMoodReports :: forall a a' (b :: Intensity) (c :: Intensity). SMoodReport ('MR '(a, b)) -> SMoodReport ('MR '(a, c)) -> SMoodReport ('MR '(a, b <> c))
addSingMoodReports (SMR (STuple2 a b)) (SMR (STuple2 a' c)) = SMR $ STuple2 a (b %<> c)


unsafeAddMoodReports :: MoodReport -> MoodReport -> MoodReport
unsafeAddMoodReports (MR (a, c)) (MR (b, d)) = MR (a, d <> c)

moodreeporttoming仍然是明确的，需要打字才能使用。某种程度上的问题在于它会丢失类型数据（或者如果没有类型数据，我不知道如何使用该数据），并且其中只有友好的数据，我想将其传递给addsingmoodreports 功能。无论如何，是否可以隐含地将它们推断出GHC的类型或旁路类型搜索？