The problem I see here is that your List1 and List2 kinds are essentially untyped. These lists are allowed to store any types. For example, I can say `Cons1 'True (Cons1 Int Nil1)`, even though 'True and Int have different kinds. Your List3 won't allow such a construction. You're right that the kinds aren't isomorphic.
Does this help?
Richard
On Dec 9, 2014, at 6:09 PM, Gautier DI FOLCO
Hello,
In fact my problem occurs when I try to describe (Iso)morphisms: type Cons1 (e :: k1) (n :: k2) = Product e n type Nil1 = Void
type Cons2 e n = Just (Product e n) type Nil2 = Nothing
data List3 a = Nil3 | Cons3 a (List3 a)
type family List1_List2 a where List1_List2 (Cons1 a b) = Cons2 a (List1_List2 b) List1_List2 Nil1 = Nil2
type family List2_List1 a where List2_List1 (Cons2 a b) = Cons1 a (List2_List1 b) List2_List1 Nil2 = Nil1
type family List2_List3 a where List2_List3 (Cons2 a b) = Cons3 a (List2_List3 b) List2_List3 Nil2 = Nil3
type family List3_List2 a where List3_List2 (Cons3 a b) = Cons2 a (List3_List2 b) List3_List2 Nil3 = Nil2
type List1_List3 a = List2_List3 (List1_List2 a) type List3_List1 a = List2_List1 (List3_List2 a)
There is an Isomorphism between List1 and List2 (List1_List2 (List2_List1 a) == a and List2_List1 (List1_List2 a) == a) but not between List3 and the others due to it's * kind.
Thanks, Regards.