отказ в проверке типов кода с помощью Тип Families

Question

У меня есть модуль Data.FastSet, где определен этот класс типов:

{-# LANGUAGE TypeFamilies #-} 

    class HasFastSet elt where 
     type FastSet elt :: * 
     empty :: FastSet elt 
     fromList :: [elt] -> FastSet elt 
     member :: elt -> FastSet elt -> Bool 
     eq :: FastSet elt -> FastSet elt -> Bool 
     insert :: elt -> FastSet elt -> FastSet elt 
     union :: FastSet elt -> FastSet elt -> FastSet elt 
     filter :: (elt -> Bool) -> FastSet elt -> FastSet elt 

вместе с несколькими экземплярами. Тогда, в каком-то другом модуле, я пытаюсь использовать:

{-# LANGUAGE RankNTypes, TypeFamilies, ScopedTypeVariables #-} 
    import qualified Data.FastSet as FS 

    data StaticInfo elt = StaticInfo { matchesEmpty :: Bool, 
             starters :: FS.FastSet elt } 


    sequentialCompose :: forall m elt. (Monad m, FS.HasFastSet elt) => 
    m (StaticInfo elt) -> m (StaticInfo elt) -> m (StaticInfo elt) 
    sequentialCompose si1 si2 = do 
     StaticInfo me1 st1 <- si1 
     case me1 of 
     False -> si1 
     True -> do 
        StaticInfo me2 st2 <- si2 
        let together = FS.union st1 st2 :: FS.FastSet elt 
        return (StaticInfo me2 together) 

Как вы видите, я пытался использовать расширение ScopedTypeVariables сказать, что программа проверки результате объединения двух множеств имеет тот же тип, что и наборы самих себя. Когда я пытаюсь скомпилировать это, он дает мне ошибку типа (и это то же самое, независимо от моей попытки дать явный тип для together переменной:

Couldn't match expected type ‘FS.FastSet elt’ 
      with actual type ‘FS.FastSet elt1’ 
NB: ‘FS.FastSet’ is a type function, and may not be injective 
The type variable ‘elt1’ is ambiguous 
Relevant bindings include 
    together :: FS.FastSet elt 
    (bound at /home/olympia/concurrency-talk/chat-benchmark/src/Text/Parsing/StaticInfo.hs:24:20) 
    st2 :: FS.FastSet elt 
    (bound at /home/olympia/concurrency-talk/chat-benchmark/src/Text/Parsing/StaticInfo.hs:23:31) 
    st1 :: FS.FastSet elt 
    (bound at /home/olympia/concurrency-talk/chat-benchmark/src/Text/Parsing/StaticInfo.hs:19:18) 
    si2 :: m (StaticInfo elt) 
    (bound at /home/olympia/concurrency-talk/chat-benchmark/src/Text/Parsing/StaticInfo.hs:18:23) 
    si1 :: m (StaticInfo elt) 
    (bound at /home/olympia/concurrency-talk/chat-benchmark/src/Text/Parsing/StaticInfo.hs:18:19) 
    sequentialCompose :: m (StaticInfo elt) 
         -> m (StaticInfo elt) -> m (StaticInfo elt) 
    (bound at /home/olympia/concurrency-talk/chat-benchmark/src/Text/Parsing/StaticInfo.hs:18:1) 
In the expression: FS.union st1 st2 :: FS.FastSet elt 
In an equation for ‘together’: 
    together = FS.union st1 st2 :: FS.FastSet elt 

Что я делаю неправильно

Answer 1

Я подозреваю, что вы несколько злоупотребляя связанные типы это не должно быть так, что практически каждый аргумент ваших методов семейного типа

определение класса легко позволяет экземпляр, как:..

instance HasFastSet Int where 
    type FastSet Int = Bool 
    -- ... 

И вот для этого случая union :: Bool -> Bool -> Bool, которому GHC будет сложно узнать, что это экземпляра union, тем более, что, как говорится в сообщении об ошибке, у вас может быть экземпляр для Char с type FastSet Char :: Bool.

Так что происходит в вашем коде, когда вы используете union, он не знает, что использовать union. Поскольку семейства типов не являются инъективными, не имеет значения, что параметры имеют тип FastSet elt, потому что FastSet elt ~ FastSet elt1 возможен. Точно так же контекст класса также не имеет значения. При этом использование union GHC не заботится о том, какие ограничения класса для функции в целом есть, и даже если бы это было возможно, вы могли просто лишить ограничение, поэтому предоставленные вами ограничения не будут устранять проблему.

Более обычное использование связанных типов было бы скорее похожим на тип элемента, связанный с классом, параметризованным типом коллекции, что-то вроде этого, тогда вы получаете типовые экземпляры семейства, такие как type Elem [Int] = Int, и методы разрешимы без необходимости угадывать типа. Вы можете переключиться на семейства данных, но я думаю, что вам лучше было бы полностью пересмотреть ваш подход.