Injection Type Families with GADT

Question

I tried a very simple example involving families of injective types, but I can't get it to work.

{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilyDependencies #-} type family F c = result | result -> c data G b where G :: G b -> G (F b) foo :: G (F a) -> G a foo (G a) = a 

This leads to a compilation error.

 Inject.hs:10:13: error: • Could not deduce: b ~ a from the context: F a ~ F b bound by a pattern with constructor: G :: forall b. G b -> G (F b), in an equation for 'foo' at Inject.hs:10:6-8 'b' is a rigid type variable bound by a pattern with constructor: G :: forall b. G b -> G (F b), in an equation for 'foo' at Inject.hs:10:6 'a' is a rigid type variable bound by the type signature for: foo :: forall a. G (F a) -> G a at Inject.hs:9:8 Expected type: G a Actual type: G b • In the expression: a In an equation for 'foo': foo (G a) = a • Relevant bindings include a :: G b (bound at Inject.hs:10:8) foo :: G (F a) -> G a (bound at Inject.hs:10:1) 

which is the same error I get if I use the non-injection / regular type family for F What gives?