How can I derive typeclass instances from constraint families that are in scope?

Question

edit: I have followed up with a more specific question. Thank you answerers here, and I think the followup question does a better job of explaining some confusion I introduced here.

---

TL;DR I'm struggling to get proofs of constraints into expressions, while using GADTs with existential constraints on the constructors. (that's a serious mouthful, sorry!)

---

I've distilled a problem down to the following. I have a simple GADT that represents points called X and function applications called F. The points X are constrained to be Objects.

data GADT ix a where
  X :: Object ix a => a -> GADT ix a
  F :: (a -> b) -> GADT ix a -> GADT ix b

Constrained refers to containers whose objects are constrained by something and Object is that something. (edit: my real problem involves Category and Cartesian classes from constrained-categories)

-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
  type Object ix a :: Constraint

-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for ex
instance Constrained (GADT ix) where
  type Object (GADT ix) a = (Constrained ix, Object ix a)

I would like to write an expression:

-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex0 :: GADT ix String
ex0 = F show (X (3 :: Int))

And while the obvious solution works, it quickly becomes verbose when building larger expressions:

-- Typechecks, but eventually verbose
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))

I think the correct solution should look something like this:

-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex2 :: Constrained ix => GADT ix String
ex2 = F show (X (3 :: Int))

But I still can't get that proof of Object ix Int.

I'm sure it's simpler than I'm thinking. I have tried adding constraints to the Object constraint family in the GADT class instance. I have tried offering constraints in the expression's signature. I have tried QuantifiedConstraints, although, I'm not sure I fully grasp it yet. Please help me wise ones!

---

Runnable:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}

module Test where

import Data.Kind
import Data.Functor.Identity
import Data.Functor.Const

-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
  type Object ix a :: Constraint

-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for instance
instance Constrained (GADT ix) where
  type Object (GADT ix) a = (Constrained ix, Object ix a)

-- | A demo GADT that has function application ('F'), and points ('X'). The
-- points are constrained.
data GADT ix a where
  X :: Object ix a => a -> GADT ix a
  F :: (a -> b) -> GADT ix a -> GADT ix b

-- -- Broken
-- -- error: Could not deduce: Object ix Int arising from a use of ‘X’
-- ex0 :: GADT ix String
-- ex0 = F show (X (3 :: Int))

-- Typechecks
-- but for larger programs becomes verbose, requiring many explicit constraints
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))

-- -- What I want, but, it's broken
-- ex2 :: Constrained ix => GADT ix String
-- ex2 = F show (X (3 :: Int))

Answer 1

Without more context it's hard to say what's the best solution, but here are a couple of possibilities:

Avoid constraining at all

As it stands, your GADT doesn't seem to have much reason for restricting X to Object. Maybe this is just not needed?

data GADT ix a where
  X :: a -> GADT ix a
  F :: (a -> b) -> GADT ix a -> GADT ix b

Instead, the constraint could come from the outside when it's needed.

Bite the bullet of constraint lists, but make them nicer

If you have many different types in your expression that all need to fulfill the same constraint, you can use a helper like All

ex2' :: All (Object ix) '[Int] => GADT ix String
ex2' = F show (X (3 :: Int))

where there can be more types in the list in addition to Int; and/or you can make synonym constraints such as

type StdObjs ix = (Object ix Int, Object x Bool, ...)

ex2'' :: StdObjs ix => GADT ix String
ex2'' = F show (X (3 :: Int))

Propagate the constraints backwards through the data structure itself

If you do need the constraint on the X values, it may nevertheless be possible to express this in another way in the GADT. For example, if the function is not a general function but something that is already constrained to only accept Objects, you could have it like this:

data YourFunc ix a b where
  YourFunc :: Object ix a => (a->b) -> YourFunc ix a b

show' :: Object ix Int => YourFunc ix Int String
show' = YourFunc show

This doesn't directly help with the problem you were asking about, but maybe the function is shared or something. You could even have something like

class Object ix a => InferrenceChain ix a where
  type PreElem ix a :: Type
  propInferrence :: (InferrenceChain ix (PreElem a) => r) -> r

and then

data YourFunc ix a b where
  YourFunc :: InferrenceChain ix a
                 => (PreElem a -> a) -> YourFunc (PreElem a) a

Then in the end you could proof the X constraint from just putting in Object ix String on the outside and recursing over propInferrence. But this would probably get quite fiddly.