I still haven't been able to get the entire library to compile, but I was doing some digging in SubType today and found a potential strategy to make Sup a type family. I reconstructed all of the code on that page by making it a type family:
type family Sup (a::k) (b::k) :: k
and then it seems to me that you could replace all past invocations of the constraint (Sup s t u) with (Sup s t ~ u). For instance, in the SubType module again, for (<:):
class (Sup s t ~ t, Sup t s ~ t) => (s::k) <: (t::k) where
embedType_ :: Embed s t
As I have said, the library in its entirety has not chosen to compile for me yet, so I'm not sure if the above solution would conflict with anything else anywhere, but it seems to work in the confinement of that file.
On another note, the problem of making Embed a type family rather than a data family seems to be quite impossible given what I know about hacking that type of thing together. It really makes no sense to me personally why it hollers about it being ambiguous, as I thought that you could only instantiate Embed s t once for each pair s, t, but the type checker is likely to know better than me.
I still haven't been able to get the entire library to compile, but I was doing some digging in SubType today and found a potential strategy to make Sup a type family. I reconstructed all of the code on that page by making it a type family:
type family Sup (a::k) (b::k) :: k
and then it seems to me that you could replace all past invocations of the constraint (Sup s t u) with (Sup s t ~ u). For instance, in the SubType module again, for (<:):
class (Sup s t ~ t, Sup t s ~ t) => (s::k) <: (t::k) where embedType_ :: Embed s t
As I have said, the library in its entirety has not chosen to compile for me yet, so I'm not sure if the above solution would conflict with anything else anywhere, but it seems to work in the confinement of that file.
On another note, the problem of making Embed a type family rather than a data family seems to be quite impossible given what I know about hacking that type of thing together. It really makes no sense to me personally why it hollers about it being ambiguous, as I thought that you could only instantiate Embed s t once for each pair s, t, but the type checker is likely to know better than me.