[Haskell-cafe] Is UndecidableInstances unavoidable in heterogenous Show derivation?

30 Nov 2019

      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)

[Haskell-cafe] Is UndecidableInstances unavoidable in heterogenous Show derivation?

Viktor Dukhovni