Injection families and restrictions

Question

Suppose we have some existing class or restriction Cand the following:

{-# TypeFamilyDependencies #-}

type family F t = s | s -> t

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

Of course, type D s ...it cannot be compiled due to an unknown variable t, but how can I write something like D s? I basically want to write:

type D s = (C (T_Inverse s))

I think this should be fair, because it T_Inverseexists because of injectivity . I just don’t know how to express it.

Answer 1

The best I can do is

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

(, ) FI , , . . , GHC , !

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

.