dicts.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Constraint
import Exinst.Singletons
import Data.Singletons.Prelude hiding ((:-))

newDict
  :: forall k0 (c :: k0 -> Constraint) (f :: k1 -> k0) (g :: k2 -> k0) (h :: Either k1 k2 -> k0) (d :: Either k1 k2).
    ( Dict1 c f
    , Dict1 c g
    ) => Sing d -> Dict (c (h d))
newDict = \case
  SLeft (s1 :: Sing (a1 :: k1)) -> -- learn d ~ ('Left a1)
    case (dict1 :: _ -> Dict (c (f a1))) s1 of
      Dict -> -- learn (c (f a1))
        Dict \\ (Sub Dict :: () :- c (h ('Left a1)))
  _ -> undefined