単射型家族や制約

Question

は、我々はいくつかの既存のクラスまたは制約C、および以下の持っているとしましょう：もちろんtype D s ...の

{-# TypeFamilyDependencies #-} 

type family F t = s | s -> t 

type D s = (s ~ T t, C t) 

が原因不明の変数tのコンパイルに失敗しますが、私はどのように書くことができますD sのようなものですか？私が思う

type D s = (C (T_Inverse s)) 

は単射のT_Inverseが存在するためとして有効である必要があります：私は基本的に書きたいです。私はそれを表現する方法を知りません。

Answer 1

私が行う方法を知って最高のあなたは（おそらく部分）を形成する必要があります

type family FI a 
type D s = (s ~ F (FI s), C (FI s)) 

あるセクションFI自分は、そう私は単射型家族は本当に助けとは思いません。 Injective型の家族は、この時点では非常に限られており、不自然に思える。明らかな例を挙げると、GHCは彼らが注射薬であると受け入れることさえありません！

blah :: F a ~ F b => a :~: b 
blah = Refl 

は、タイプチェッカーに合格しません。