I'll add that Gautier's Prod has an inverse. When it's included, ghc can infer the types of x in these expressions: \x -> (Foo x :: Foo Int a) \x -> (Foo x :: Foo String a) as String and Maybe String respectively. Prod was unchanged, but the rest becomes: type family ProdInv a where ProdInv Int = String ProdInv a = Maybe a data Foo e a where Foo :: e ~ ProdInv (Prod e) => e -> Foo (Prod e) a I also thought about using a data family instead of a pair of type families. But then you still have two constructors. `class ProdFD e pe | e -> pe, pe -> e` can't work: 1. FDs don't provide coercions like TFs 2. the two ProdFD instances are rejected -- they overlap/violate FDs On Mon, Jul 4, 2016 at 5:31 PM, Gautier DI FOLCO wrote:

Hello,

I would say that type families should do the joke:

{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GADTs #-} type family Prod a where Prod String = Int Prod (Maybe a) = a

data Foo e a where

Foo :: e -> Foo (Prod e) a

Regards.

2016-07-04 22:43 GMT+02:00 Corentin Dupont :

...

Hi all, I have a data type looking like this:

data Foo e a where

Foo :: e → Foo e a

I would like to instantiate it to make it equivalent to:

data Bar a where

A :: String → Bar Int B :: Maybe a → Bar a

How can I do that? With a functional dependency? I probably need to change the definition of Foo.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.