Quantified constraints vs. (closed) type families

Question

I am trying to use this blogpost's approach to higher-kinded data without dangling Identity functors for the trival case together with quantified-constraint deriving:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, UndecidableInstances #-}
module HKD2 where

import Control.Monad.Identity

type family HKD f a where
    HKD Identity a = a
    HKD f        a = f a

data Result f = MkResult
    { foo :: HKD f Int
    , bar :: HKD f Bool
    }

deriving instance (forall a. Show a => Show (HKD f a)) => Show (Result f)

This results in the infuriatingly self-contradicting error message:

Could not deduce Show (HKD f a) from the context: forall a. Show a => Show (HKD f a)

Is there a way to do this without being long-winded about it and doing

deriving instance (Show (HKD f Int), Show (HKD f Bool)) => Show (Result f)

?

Postulate

Ouch. I thought that (forall a. Show a => Show (HKD f a)) was disallowed when HKD is not a constructor, but I was wrong. Note that if we assume that quantified constraint, to resolve e.g. HKD f b we can't simply check Show b. Indeed if that fails, we can't report failure since it is possible that HKD f b = HKD f c holds (because of non-injectivity), and Show c is true. So, committing to a=b does not lead to a complete resolution method. – Counterwork

Again, instance C a => C (HKD f a) where is rejected by GHC, so I don't understand why the quantified constraint (forall a. C a => C (HKD f a)) is accepted. How can we provide that constraint later on? – Counterwork

The answer to this question may be buried in this wholly relevant thread: gitlab.haskell.org/ghc/ghc/issues/14860 – Prakrit

My general view has always been that the HKD trick is a Bad Idea™ because it makes the easy things easier and the hard things harder. – Ables

The core issue is independent and comes up outside of HKD. – Prakrit

Answer 1

tl;dr, gist: https://gist.github.com/Lysxia/7f955fe5f2024529ba691785a0fe4439

Boilerplate constraints

First, if the question is about avoiding repetitive code, this is mostly addressed by generics alone, without QuantifiedConstraints. The constraint (Show (HKD f Int), Show (HKD f Bool)) can be computed from the generic representation Rep (Result f). The generic-data package (disclaimer: that I wrote) implements this:

data Result f = MkResult (HKD f Int) (HKD f Bool)
  deriving Generic

-- GShow0 and gshowsPrec from Generic.Data
instance GShow0 (Rep (Result f)) => Show (Result f) where
  showsPrec = gshowsPrec

or with DerivingVia:

-- Generically and GShow0 from Generic.Data
deriving via Generically (Result f) instance GShow0 (Rep (Result f)) => Show (Result f)

Quantified constraints with type families

Nevertheless, the constraint (Show (HKD f Int), Show (HKD f Bool)) may be less than ideal for various reasons. The QuantifiedConstraints extension may seem to provide a more natural constraint forall x. Show (HKD f x):

• it would entail the tuple (Show (HKD f Int), Show (HKD f Bool));

• contrary to that tuple, it does not blow up in size when the record gets big, and does not leak the field types of Result as they may be subject to change.

Unfortunately, that constraint is actually not well-formed. The following GHC issue discusses the problem in detail: https://gitlab.haskell.org/ghc/ghc/issues/14840 I don't understand all of the reasons yet, but in brief:

• Quantified constraints won't work directly with type families for the foreseeable future, for reasons both theoretical and practical;

• But there is a workaround for most use cases.

A quantified constraint should be viewed as a sort of "local instance". The general rule then is that type families are not allowed in the head of any instance ("instance head" = the HEAD in the following instance ... => HEAD where). So forall a. Show (HKD f a) (viewed as a "local" instance Show (HKD f a)) is illegal.

Quantified constraint smuggler

The following solution is credited to Icelandjack (Source: this comment from the ticket linked earlier; thanks also to Ryan Scott for relaying it.)

We can define another class that's equivalent to Show (HKD f a):

class    Show (HKD f a) => ShowHKD f a
instance Show (HKD f a) => ShowHKD f a

Now forall x. ShowHKD f x is a legal constraint that morally expresses the intended forall x. Show (HKD f x). But it's not at all obvious how to use it. For example, the following snippet fails to type check (note: we can easily ignore the ambiguity issues):

showHKD :: forall f. (forall x. ShowHKD f x) => HKD f Int -> String
showHKD = show

-- Error:
-- Could not deduce (Show (HKD f Int)) from the context (forall x. ShowHKD f x)

This is counterintuitive, because ShowHKD f x is equivalent to Show (HKD f x) which can of course be instantiated with Show (HKD f Int). So why is that rejected? The constraint solver reasons backwards: the use of show first requires a constraint Show (HKD f Int), but the solver is immediately stuck. It sees forall x. ShowHKD f x in the context, but there is no clue for the solver to know that it should instantiate x to Int. You should imagine that at this point, the constraint solver has no idea of any relationship between Show and ShowHKD. It just wants a Show constraint, and there is none in the context.

We can help the constraint solver as follows, by annotating the body of the function with the needed instantiation(s) of ShowHKD f x, here ShowHKD f Int:

showHKD :: forall f. (forall x. ShowHKD f x) => HKD f Int -> String
showHKD = show :: ShowHKD f Int => HKD f Int -> String

This annotation provides the constraint ShowHKD f Int to the body show, which in turn makes the superclass available Show (HKD f Int) so show can be immediately satisfied. On the other side, the annotation requires the constraint ShowHKD f Int from its context, which provides forall x. ShowHKD f x. Those constraints match, and that leads the constraint solver to instantiate x appropriately.

Deriving Show with quantified constraints

With this, we can implement Show with a quantified constraint, using generics to fill out the body, and with some annotations to instantiate the quantified constraint, (ShowHKD f Int, ShowHKD f Bool):

instance (forall a. Show a => ShowHKD f a) => Show (Result f) where
  showsPrec = gshowsPrec :: (ShowHKD f Int, ShowHKD f Bool) => Int -> Result f -> ShowS

As before, those constraints can be automated with generics, so the only thing that changes in this implementation from one type to another is the name Result:

instance (forall a. Show a => ShowHKD f a) => Show (Result f) where
  showsPrec = gshowsPrec :: ShowHKDFields f (Rep (Result HKDTag)) => Int -> Result f -> ShowS

-- New definitions: ShowHKDFields and HKDTag; see gist at the end.

And with a bit more effort, we can have DerivingVia too:

deriving via GenericallyHKD Result f instance (forall a. Show a => ShowHKD f a) => Show (Result f)

-- New definition: GenericallyHKD; see gist.

---

Full gist: https://gist.github.com/Lysxia/7f955fe5f2024529ba691785a0fe4439

Prakrit

Answer 2

I don't think you can do such thing, but I could certainly be wrong. In your example you are missing an extra constraint Show (f a) in order for it to be complete:

deriving instance (forall a. (Show a, Show (f a)) => 
   Show (HKD f a)) => Show (Result f)

But that would mean that Show instance for f a cannot depend on a, which can be true for specific f, but not in general.

Edit

But at the same time it is possible to write something like that without the TypeFamilies:

data Bar f = MkBar (f Int)

deriving instance (forall a . Show a => Show (f a)) => Show (Bar f)

So, I am not sure why GHC can't figure it out.

Edit 2

Here is an interesting observation, this compiles:

type family HKD f a where
    -- HKD Identity a = a
    HKD f Int = Int
    HKD f a = f a

data Result f = MkResult
    { foo :: HKD f Int
    , bar :: HKD f Bool
    }

deriving instance (forall a. Show a => Show (f a)) => Show (Result f)

and works as expected:

λ> show $ MkResult 5 (Just True)
"MkResult {foo = 5, bar = Just True}"

So, it looks like matching on f somehow messes up the type checker.

Worth noting, that restricting to Show (HDK f a) even for the simplified example also gives the same compile time error as in the question:

deriving instance (forall a. Show a => Show (HKD f a)) => Show (Result f)

Maceio