Is there any way to open constraint dictionaries at compile-time in GHC?

Question

Consider the following Haskell code (GHC 8.2):

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Constraint

type family Head xs where
  Head (x ': xs) = x

type family Tail xs where
  Tail (x ': xs) = xs

class IsList xs where
  isList :: (xs ~ '[] => r) -> ((xs ~ (Head xs ': Tail xs), IsList (Tail xs)) => r) -> r

instance IsList '[] where isList r _ = r
instance IsList xs => IsList (x ': xs) where isList _ r = r

type family Prepend xs ys where
  Prepend '[] ys = ys
  Prepend (x ': xs) ys = x ': Prepend xs ys

prependPreservesIsList :: forall xs ys. (IsList xs, IsList ys) => Dict (IsList (Prepend xs ys))
prependPreservesIsList = isList @xs Dict (withDict (prependPreservesIsList @(Tail xs) @ys) Dict)

class IsList (Deps a) => Hard (a :: *) where
  type Deps a :: [*]

instance (Hard a, Hard b) => Hard (Either a b) where
  type Deps (Either a b) = Prepend (Deps a) (Deps b)

it fails with

Main.hs:37:10: error:
    • Could not deduce (IsList (Prepend (Deps a) (Deps b)))
        arising from the superclasses of an instance declaration
      from the context: (Hard a, Hard b)
        bound by the instance declaration at Main.hs:37:10-46
    • In the instance declaration for ‘Hard (Either a b)’
   |
37 | instance (Hard a, Hard b) => Hard (Either a b) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

What the code is trying to do is construct a class Hard that has an associated list of types Deps, where the Deps corresponding to an Either a b are supposed to be the concatenation of the Deps corresponding to a and b.

We know how to prove to GHC that this form of concatenation preserves the IsList class, as witnessed by prependPreservesIsList. If we had (Hard a, Hard b) and we needed to write normal code that required (IsList (Deps (Either a b))) we'd just withDict prependPreservesIsList and be on our way. But we need GHC to recognize this constraint "at compile time", in order to grant that the Either a b instance is legal.

Is there any way to "open a constraint dictionary" at compile-time, or to otherwise finagle this code so as to cause GHC to accept the Either a b instance?

Answer 1

Consider switching from type-level lists to type-level trees. So:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

data Tree a = Empty | Node a | Branch (Tree a) (Tree a)

class IsTree xs where
    isTree ::
        (xs ~ 'Empty => a) ->
        (forall x. xs ~ 'Node x => a) ->
        (forall l r. (xs ~ 'Branch l r, IsTree l, IsTree r) => a) ->
        a

instance IsTree 'Empty where isTree a _ _ = a
instance IsTree ('Node x) where isTree _ a _ = a
instance (IsTree l, IsTree r) => IsTree ('Branch l r) where isTree _ _ a = a

class IsTree (Deps a) => Hard a where
    type Deps a :: Tree *

instance (Hard a, Hard b) => Hard (Either a b) where
    type Deps (Either a b) = 'Branch (Deps a) (Deps b)