Prove that a constraint holds for a component of a product from the fact it holds for the product

Question

I have a class C with instances for one type and for tuples.

class C a

instance C Int

instance (C a, C b) => C (a, b)

Using the normal Dict GADT for capturing constraints

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}

data Dict c where
    Dict :: c => Dict c

is it possible to prove C a from C (a, b)?

fstDict :: Dict (C (a, b)) -> Dict (C a)
fstDict Dict = ???

I suspect the immediate answer is "no" since fstDict Dict = Dict isn't sufficient, and there are few other possibilities. Is there any way to change C so that constraints for components of products can be recovered from the constraint on the product?

I am, perhaps incorrectly, trying to accomplish the same thing as the most closely related question, however I have the luxury to demand a Dict from one or both ends of the category.

data DSL a b where
    DSL :: (Dict C a -> DSL' a b) -> DSL a b

data DSL' a b where
    DSL' :: (C a, C b) => ... -> DSL' a b

score 1 · Answer 1 · answered Jan 09 '15 at 02:48

One way is to store all ancestor dictionaries in your Dict type:

data CDict a where
    IntDict :: C Int => CDict Int
    PairDict :: C (a, b) => CDict a -> CDict b -> CDict (a, b)

fstCDict :: CDict (a, b) -> CDict a
fstCDict (PairDict fst snd) = fst

This has the downside that you must make the CDict type reflect the structure of your instances.

score 1 · Accepted Answer · edited May 23 '17 at 12:28

An open variant of Daniel Wagner's answer would use a TypeFamily to let each type that implements the class specify a context that it needs.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.Exts (Constraint)
import Data.Proxy

data Dict c where
    Dict :: c => Dict c

The class lets each type specify an additional constraint Ctx a that the type needs. The cdict function forces the context to follow from C and provides a way to get at underlying Ctxs without including them in the Ctx for e.g. products.

class C a where
    type Ctx a :: Constraint
    cdict :: Proxy a -> CDict a

A CDict is then a Dict that holds both the constraint C a and also whatever additional context Ctx a the type a needs

type CDict a = Dict (C a, Ctx a)

The Int instance doesn't need any extra context

instance C Int where
    type Ctx Int = ()
    cdict _ = Dict

The tuple instance needs both C a and C b

instance (C a, C b) => C (a, b) where
    type Ctx (a, b) = (C a, C b)
    cdict _ = Dict

We can write fstCDict for tuples.

fstCDict :: forall a b. CDict (a, b) -> CDict a
fstCDict Dict = case cdict (Proxy :: Proxy a) of Dict -> Dict

Incorrect instance

If we try to write an incorrect instance of C that magically summons Show instances

instance (C a) => C (Maybe a) where
    type Ctx (Maybe a) = (C a, Show a)
    cdict _ = Dict

It results in a compiler error

    Could not deduce (Show a) arising from a use of `Dict'
    from the context (C a)
      bound by the instance declaration ...
    Possible fix:
      add (Show a) to the context of the instance declaration
    In the expression: Dict
    In an equation for `cdict': cdict _ = Dict
    In the instance declaration for `C (Maybe a)'

Prove that a constraint holds for a component of a product from the fact it holds for the product

2 Answers2

Incorrect instance