Getting output from class resolution

Question

We can get proof of the level of value that the [Int]Show instance has usingDict

{-# LANGUAGE ConstraintKinds, GADTs #-}
data Dict (p :: Constraint) where
  Dict :: p => Dict p

and

proof = Dict :: Dict (Show [Int])

Is there a way to get the conclusion of the value level, i.e. the whole evidence tree?

derivation = Apply@Int(Lam a.(Show a) :=> Show [a])) (Apply(() :=> Show Int)()) 

Answer 1

Unable to get the output of an arbitrary constraint as a Haskell value.

The closest thing I can think of if you want to check if the output is what you think is to look at the desugarer output.

ghc -ddump-ds -ddump-to-file A.hs

The relevant part is as follows:

-- RHS size: {terms: 2, types: 1, coercions: 0, joins: 0/0}
irred :: Show [Int]
[LclId]
irred = GHC.Show.$fShow[] @ Int GHC.Show.$fShowInt

-- RHS size: {terms: 2, types: 3, coercions: 0, joins: 0/0}
proof :: Dict (Show [Int])
[LclIdX]
proof = Cns.Dict @ (Show [Int]) irred

Another way is to write special classes used to display output, both in types and in values, but, of course, this does not apply to existing type classes.

{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, GADTs, DataKinds,
   FlexibleInstances, KindSignatures, MultiParamTypeClasses, RankNTypes,
   ScopedTypeVariables, TypeApplications, TypeOperators,
   UndecidableInstances #-}

import Data.Typeable
import Data.Kind

data (c :: [Type]) :=> (d :: Type -> Constraint)

class MyShow a d where
  myshow :: a -> String

instance (d ~ ('[] :=> MyShow Int)) => MyShow Int d where

instance (MyShow a da, d ~ ('[da] :=> MyShow [a])) => MyShow [a] d where

myshowInstance :: forall a d. (Typeable d, MyShow a d) => TypeRep
myshowInstance = typeRep @_ @d Proxy

main = print (myshowInstance @[Int])

, , TypeRep, , .

:=> (': * (:=> ('[] *) (MyShow Int)) ('[] *)) (MyShow [Int])

Answer 2

, , , , , . , GGC , , constraints.

- instance () :=> Show Int, Char. , , , .

{-# LANGUAGE ConstraintKinds #-}

import Data.Constraints

derivation :: () :- Show [Char]
derivation = trans showList showChar
    where showList :: Show a :- Show [a]
          showList = ins

          showChar :: () :- Show Char
          showChar = ins

, , "Sub Dict".

derivation TypeApplications Data.Constraint.Forall. Show a :- Forall Show ForallF Show [] :- Show [a] .