How to put constraints on type variable of kind `Constraint`?

Question

I'm playing around with the ConstraintKinds extension of GHC. I have the following data type, which is just a box for things fulfilling some one parameter constraint c:

data Some (c :: * -> Constraint) where
    Some :: forall a. c a => a -> Some c

For example, I could construct a box with some kind of number (arguably not very useful).

x :: Some Num
x = Some (1 :: Int)

Now, as long as c includes the constraint Show, I could provide an instance of Show (Some c).

instance ??? => Show (Some c) where
    show (Some x) = show x    -- Show dictionary for type of x should be in scope here

But how do I express this requirement in the instance context (marked with ???)?

I cannot use an equality constraint (c ~ Show), because the two are not necessarily equal. c could be Num, which implies, but is not equal to, Show.

Edit

I realised that this cannot be possible in general.

If you have two values of type Some Eq, it is not possible to compare them for equality. They could be of different types that each have their own notion of equality.

What applies to Eq applies to any type class in which the type parameter appears on the right hand side of the first function arrow (like the second a in (==) :: a -> a -> Bool).

Considering that there is no way to create a constraint expressing "this type variable is not used beyond the first arrow", I don't think it is possible to write the instance I want to write.

Grau

Since Num no longer requires a Show instance it might be helpful to find a different example. – Cyma

Take a look at the constraints package. I don't think it will let you do what you want to do, but it may give you inspiration as to how you can accomplish this. – Mi

I don't think this can be done unless you use ??? = Foo c and Foo is a custom class to this purpose on the line of class Foo c where fooShow :: c a => a -> String, which needs to be instantiated manually with all the suitable cs (which I understand it's not your aim). – Patellate

@user2407038, it looks like the Class class in that package is the closest Edward Kmett was able to get to this. I would guess you'd probably need to change the type checker to go the rest of the way. – Conscription

@Mi Thank you, that pointed me in the right direction. – Grau

Answer 1

The closest we are able to get is a Class1 class that reifys the relationship between a class and a single superclass constraint as a class. It's based on the Class from constraints.

First, we'll take a short tour of the constraints package. A Dict captures the dictionary for a Constraint

data Dict :: Constraint -> * where
  Dict :: a => Dict a

:- captures that one constraint entails another. If we have a :- b, whenever we have the constraint a we can produce the dictionary for the constraint b.

newtype a :- b = Sub (a => Dict b)

We need a proof similar to :-, we need to know that forall a. h a :- b a, or h a => Dict (b a).

Single Inheritance

Actually implementing this for classes with just single inheritance requires the kitchen sink of language extensions, including OverlappingInstances.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}

import Data.Constraint

We'll define the class of constraints of kind k -> Constraint where the constraint has a single superclass.

class Class1 b h | h -> b where
    cls1 :: h a :- b a

We're now equipped to tackle our example problem. We have a class A that requires a Show instance.

 class Show a => A a
 instance A Int

Show is a superclass of A

instance Class1 Show A where
    cls1 = Sub Dict 

We want to write Show instances for Some

data Some (c :: * -> Constraint) where
    Some :: c a => a -> Some c

We can Show a Some Show.

instance Show (Some Show) where
    showsPrec x (Some a) = showsPrec x a

We can Show a Some h whenever h has a single superclass b and we could show Some b.

instance (Show (Some b), Class1 b h) => Show (Some h) where
    showsPrec x (Some (a :: a)) = 
        case cls1 :: h a :- b a of
            Sub Dict -> showsPrec x ((Some a) :: Some b)

This lets us write

x :: Some A
x = Some (1 :: Int)

main = print x

Cyma

Interesting. This doesn't work if c has other super classes than Show because of the functional dependency, right? – Grau

It does work. Multiple super classes are actually a single constraint (a product of constraints). – Bathy

So, the only downside is that you have to define that extra class A. – Grau

@AndrásKovács It would work for constraints of kind Constraint, these constraints have kind * -> Constraint; I don't think we can make a product of them without some trickery I haven't thought of yet. – Cyma

@TobiasBrandt A isn't an extra class, it's an example of an existing constraint that you would use in Some A. The extra work is defining the Class1 Show A instance for everything like A. – Cyma

@Cyma Understood, I was confused about the meaning of A. This seems to be the closest you can get to what I want. – Grau

That one you snuck in at the end, OverlappingInstances, is the only one that bothers me. Is there any way to avoid it? – Conscription

@Conscription I didn't sneak it in, OvelappingInstances was the only extension worth calling out explicitly in the text. For single inheritance it would be avoidable if you could add a constraint to Class1 so the compiler could prove that b ~ h doesn't hold. Unfortunately, there's no constraint backtracking, not even through closed type families for closed data kinds. Adding e.g. type family Equal a b :: Bool where Equal a a = True ; Equal a b = False and class (Equal b h ~ False) => Class1 b h | h -> b where cls1 :: h a :- b a doesn't help. – Cyma

For classes with multiple super classes, use class (p a, q a) => (&) (p :: k -> Constraint) (q :: k -> Constraint) (a :: k); instance (p a, q a) => (&) p q a which allows you to write instance Class1 (A & B) C. This is essentially the same as writing type (&) p q a = (p a, q a) but allows & to be partially applied. – Mi

Answer 2

The new QuantifiedConstraints extension allows this.

class (a => b) => Implies a b where
instance (a => b) => Implies a b where
instance (forall a. c a `Implies` Show a) => Show (Some c) where
  show (Some x) = show x

Within the body of the Show instance, it is as if there is a

instance forall a. Implies (c a) (Show a)

in scope. If you then have T :: Type and know c T, then the superclass of c T => Show T of the specialized Implies (c T) (Show T) instance allows you to derive Show T. It is necessary to use Implies instead of a straight forall a. c a => Show a constraint. This incorrect constraint acts like

instance forall a. c a => Show a

which overlaps with every Show instance, causing weird breakage. Forcing an indirection through the superclass of an otherwise useless constraint fixes everything.

Wrens

I still don't understand how that fixes everything. – Conscription

If you use the bad constraint and want, I don’t know, Show Int, there are two instances—the one from the quantified constraint and the global one—and GHC will pick one as it feels like it. If it picks the global one, congrats, you’ve got a time bomb; if it picks the quantified one, you get an insoluble c Int want. If you use Implies, there is only 1 Show Int and it’s fine. Meanwhile, for the type inside Some, you now have 0 Show instances. After (and only after) this failure, you can search the superclasses of the known constraints, finding the Show in the Implies. – Wrens

AFAICT it’s sanctioned as “expected behavior”. I don’t like it much, either, but it’s probably a bug if it ever doesn’t work. – Wrens

Answer 3

You cannot make Some c an instance of Show, except trivially.

You want to show the a inside Some, but that variable is existentially quantified, so we cannot depend on any knowledge of the type of a. In particular, we have no way of knowing that a is an instance of Show.

EDIT: I'll expand on my answer. Even with more machinery, and giving up on a Show instance, I still don't think what you want is possible because of the existential quantification.

First I'll rewrite Some in a more familiar form

data Dict p where
    Dict :: p a => a -> Dict p

The usual way to talk about "constraints implying constraints" is with the concept of constraint entailment.

data p :- q where
    Sub :: p a => Dict q -> p :- q

We can think about a value of type p :- q as a proof that if the constraint forall a. p a holds, then forall a. q a follows.

Now we try to write a sensible show-ish function

showD :: p :- Show -> Dict p -> String
showD (Sub (Dict a)) (Dict b) = show b

At a glance, this might work. We have brought the following constraints into scope (forgive the pseudo-exists syntax)

(0) p :: * -> Constraint
(1) exists a. p a           -- (Dict p)
(2) exists b. p b => Show b -- (p :- Show)

But now things fall apart, GHC rightfully complains:

main.hs:10:33:
    Could not deduce (Show a2) arising from a use of `show' 
    from the context (p a)
      bound by a pattern with constructor
                 Sub :: forall (p :: * -> Constraint) (q :: * -> Constraint) a.
                        (p a) => 
                        Dict q -> p :- q,
               in an equation for `showD' 
      at main.hs:10:8-19                    
    or from (Show a1) 
      bound by a pattern with constructor
                 Dict :: forall (p :: * -> Constraint) a. (p a) => a -> Dict p, 
               in an equation for `showD'
      at main.hs:10:13-18 
    or from (p a2)
      bound by a pattern with constructor
                 Dict :: forall (p :: * -> Constraint) a. (p a) => a -> Dict p,
               in an equation for `showD'
      at main.hs:10:23-28   

because it is impossible to unify the a from (1) with the b from (2).

This is the same essential idea that is used throughout the constraints package mentioned in the comments.

Callboy

The question is how to make, say, Some Num an instance of Show where Num implies Show. (It doesn't any more, but that's besides the point.) – Stour

The OP wrote that instance c ~ Show => Show (Some c) would work, but is stricter than it could be. (I did not downvote this, but this might explain who did) – Patellate

@Callboy Your assertion is correct in vanilla Haskell. However, I have made use of the GADTs extension, which means that matching on Some brings an instance of c a into scope. The problem is proving to the compiler that c a ~ Num a implies Show a. – Grau