I was reading: Summer School on Generic and Effectful Programming Applying Type-Level and Generic Programming in Haskell Andres Löh, Well-Typed LLP https://www.cs.ox.ac.uk/projects/utgp/school/andres.pdf and trying out the various code fragments, and was mildly surprised by the need for -XUndecidableInstances when deriving the 'Show' instance for the heterogenous N-ary product 'NP': deriving instance All (Compose Show f) xs => Show (NP f xs) Without "UndecidableInstances" I get: • Variable ‘k’ occurs more often in the constraint ‘All (Compose Show f) xs’ than in the instance head ‘Show (NP f xs)’ (Use UndecidableInstances to permit this) • In the stand-alone deriving instance for ‘All (Compose Show f) xs => Show (NP f xs)’ This is not related to automatic deriving, as a hand-crafted instance triggers the same error: instance All (Compose Show f) xs => Show (NP f xs) where show Nil = "Nil" show (x :* xs) = show x ++ " :* " ++ show xs Is there some other way of putting together the building blocks that avoids the need for 'UndecidableInstances', or is that somehow intrinsic to the type of NP construction? I guess I should also ask whether there's a way to define something equivalent to 'Compose' without 'UndecidableSuperClasses', and perhaps the two are not unrelated. [ Perhaps I should be more blasé about enabling these extensions, but I prefer to leave sanity checks enabled when possible. ] -- Viktor. {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} import GHC.Exts (Constraint) -- | Map a constraint over a list of types. type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where All _ '[] = () All c (x ': xs) = (c x, All c xs) -- | With @g@ a type constructor and @f@ a constraint, define @Compose f g@ as -- a contraint on @x@ to mean that @g x@ satisfies @f@. -- -- Requires: -- -- 'ConstraintKinds' -- 'FlexibleInstances' -- 'MultiParamTypeClasses' -- 'TypeOperators' -- 'UndecidableSuperClasses' -- class (f (g x)) => (Compose f g) x instance (f (g x)) => (Compose f g) x -- | Type-level 'const'. newtype K a b = K { unK :: a } deriving instance Show a => Show (K a b) -- | N-ary product over an index list of types @xs@ via an interpretation -- function @f@, constructed as a list of elements @f x@. -- data NP (f :: k -> *) (xs :: [k]) where Nil :: NP f '[] (:*) :: f x -> NP f xs -> NP f (x ': xs) infixr 5 :* -- | If we can 'show' each @f x@, then we can 'show' @NP f xs@. -- -- Requires: 'UndecidableInstances' -- deriving instance All (Compose Show f) xs => Show (NP f xs)