| I also noticed a problem with my logic for creating the NT-lifting | function. Suppose | data C a = MkC (Foo a) | Just having the constructors of C in scope is not sufficient | to safely provide | NT a b -> NT (C a) (C b) | as the parameters of the constructor might wrap a in another type | constructor, eg | data Foo a = Foo (Set a) | | then we certainly don’t want the user to be able to write | deriving fooNT :: NT a b -> NT (Foo a) (Foo b) Dually, suppose Foo was an *abstract* type, where we can't see the constructors of Foo. But the programmer as exported fooNT :: NT a b -> NT (Foo a) (Foo b). Then we *do* want to be able to derive cNT :: NT a b -> NT (C a) (C b) Instead maybe we say deriving cNT :: NT a b -> NT (C a) (C b) using( fooNT ) listing the imported witnesses that we use. Or maybe we say simply deriving cNT :: NT a b -> NT (C a) (C b) and magically use any NT-typed things that are in scope. This clearly deserves treatment on the wiki page. The criterion "could you write it by hand?" remains a good one. Simon