Hi, small update: I generalized the code at https://github.com/nomeata/nt-coerce/blob/9349dd3/GHC/NT/Plugin.hs a bit, it is now able to handle to create NT-values for unwarpping arbitrary newtypes and for lifting across type constructors. It does so unconditionally, i.e. does _not_ yet check whether the constructors are in scope and whether the user is allowed to cast the types occurring in the data constructors. So what works is this: NT values for newtypes without or with type arguments, and possibly recursive: newtype Age = Age Int deriving Show ageNT :: NT Age Int ageNT = deriveThisNT -- temporary syntax for deriving listNT ... newtype MyList a = MyList [a] deriving Show myListNT :: NT (MyList a) [a] myListNT = deriveThisNT newtype R a = R [R a] deriving Show rNT :: NT (R a) [R a] rNT = deriveThisNT NT values for type constructors, replacinge all or some of the type parameters: listNT :: NT a b -> NT [a] [b] listNT = deriveThisNT myListNT' :: NT a b -> NT (MyList a) (MyList b) myListNT' = deriveThisNT data F a b c = F a b c deriving Show fNT :: NT a a' -> NT (F a b c) (F a' b c) fNT = deriveThisNT What does not work is creating a NT value between a newtype and its representation if type arguments change on the way, e.g. bar :: NT (MyList Age) [Int] but the user can construct that himself: bar = myListNT' ageNT `trans` myListNT The next step would be to add the safeguards about the visibility of constructors and about the types of data constructor parameters. Especially the latter is still not clear to me: For example with data Foo a = Foo (Bar a) is it really sufficient to check whether a "barNT:: NT a b -> NT (Bar a) (Bar b)" exists? After all, I would not need barNT in the generated implementation of fooNT, so the user could “provide” this value via undefined and nobody would notice. I get the feeling that already the typing rule for TyConAppCo should expect coercions between the actual types in the data constructors rather than just between the type constructor parameters, so that the implementation barNT would actually have to use fooNT. Maybe that would simplify the two-equalities-approach. But that is just an uneducated gut feeling. BTW: Is this still on-topic on glasgow-haskell-users or should I move to ghc-dev? Greetings, Joachim -- Joachim “nomeata” Breitner mail@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org