{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
# LANGUAGE FlexibleInstances      #
# LANGUAGE GADTs                  #
# LANGUAGE MultiParamTypeClasses #
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TypeOperators         #-}
# LANGUAGE UndecidableInstances   #

module DefinitionsUndecidable where

  | We define the data types and generate the TH in a separate module
-- because we want to ensure that no external names are required to be
-- imported.
--
  It 's a bit sad that these need UndecidableInstances

import GHC.Generics (Generic)
import Data.Profunctor.Product (ProductProfunctor, SumProfunctor)
import Data.Profunctor.Product.Default
  (Default, DefaultFields', DefaultConstraints, DefaultConstraints')

data MonomorphicProduct = Product Int Bool            deriving Generic
data MonomorphicSum     = A Int | B Bool              deriving Generic
data MonomorphicBoth    = Both1 Char | Both2 Int Bool deriving Generic
data PolyProduct a b c  = PolyProduct a b c           deriving Generic

instance (ProductProfunctor p, DefaultFields' p MonomorphicProduct)
         => Default p MonomorphicProduct MonomorphicProduct

instance (SumProfunctor p, DefaultFields' p MonomorphicSum)
         => Default p MonomorphicSum MonomorphicSum

instance (DefaultConstraints' p MonomorphicBoth)
         => Default p MonomorphicBoth MonomorphicBoth

instance
  ( DefaultConstraints p
      (PolyProduct a b c)
      (PolyProduct a' b' c')
  ) => Default p (PolyProduct a b c) (PolyProduct a' b' c')

  A constraint 
data Dict c where
  Dict :: c => Dict c

-- Entailment @c => d@.
data c :- d where
  Sub :: (c => Dict d) -> c :- d

-- Equivalence of constraints.
type c :<=>: d = (c :- d, d :- c)

checkDFMonomorphicProduct
  :: DefaultFields' p MonomorphicProduct :<=>:
     (Default p Int Int, Default p Bool Bool)
checkDFMonomorphicProduct = (Sub Dict, Sub Dict)

checkDFMonomorphicSum
  :: DefaultFields' p MonomorphicSum :<=>:
     (Default p Int Int, Default p Bool Bool)
checkDFMonomorphicSum = (Sub Dict, Sub Dict)

checkDCMonomorphicBoth
  :: DefaultConstraints' p MonomorphicBoth :<=>:
     (ProductProfunctor p, SumProfunctor p, Default p Int Int, Default p Bool Bool, Default p Char Char)
checkDCMonomorphicBoth = (Sub Dict, Sub Dict)

checkDCPolyProduct
  :: DefaultConstraints p (PolyProduct a b c) (PolyProduct a' b' c') :<=>:
     (ProductProfunctor p, Default p a a', Default p b b', Default p c c')
checkDCPolyProduct = (Sub Dict, Sub Dict)

# LANGUAGE ConstraintKinds       #
# LANGUAGE DataKinds             #
# LANGUAGE DeriveGeneric         #
# LANGUAGE FlexibleContexts      #
# LANGUAGE RankNTypes            #
# LANGUAGE TypeOperators         #
 because we want to ensure that no external names are required to be
 imported.

 Entailment @c => d@.
 Equivalence of constraints.
# LANGUAGE FlexibleInstances      #
# LANGUAGE GADTs                  #
# LANGUAGE MultiParamTypeClasses #
# LANGUAGE UndecidableInstances   #

module DefinitionsUndecidable where

  | We define the data types and generate the TH in a separate module
  It 's a bit sad that these need UndecidableInstances

import GHC.Generics (Generic)
import Data.Profunctor.Product (ProductProfunctor, SumProfunctor)
import Data.Profunctor.Product.Default
  (Default, DefaultFields', DefaultConstraints, DefaultConstraints')

data MonomorphicProduct = Product Int Bool            deriving Generic
data MonomorphicSum     = A Int | B Bool              deriving Generic
data MonomorphicBoth    = Both1 Char | Both2 Int Bool deriving Generic
data PolyProduct a b c  = PolyProduct a b c           deriving Generic

instance (ProductProfunctor p, DefaultFields' p MonomorphicProduct)
         => Default p MonomorphicProduct MonomorphicProduct

instance (SumProfunctor p, DefaultFields' p MonomorphicSum)
         => Default p MonomorphicSum MonomorphicSum

instance (DefaultConstraints' p MonomorphicBoth)
         => Default p MonomorphicBoth MonomorphicBoth

instance
  ( DefaultConstraints p
      (PolyProduct a b c)
      (PolyProduct a' b' c')
  ) => Default p (PolyProduct a b c) (PolyProduct a' b' c')

  A constraint 
data Dict c where
  Dict :: c => Dict c

data c :- d where
  Sub :: (c => Dict d) -> c :- d

type c :<=>: d = (c :- d, d :- c)

checkDFMonomorphicProduct
  :: DefaultFields' p MonomorphicProduct :<=>:
     (Default p Int Int, Default p Bool Bool)
checkDFMonomorphicProduct = (Sub Dict, Sub Dict)

checkDFMonomorphicSum
  :: DefaultFields' p MonomorphicSum :<=>:
     (Default p Int Int, Default p Bool Bool)
checkDFMonomorphicSum = (Sub Dict, Sub Dict)

checkDCMonomorphicBoth
  :: DefaultConstraints' p MonomorphicBoth :<=>:
     (ProductProfunctor p, SumProfunctor p, Default p Int Int, Default p Bool Bool, Default p Char Char)
checkDCMonomorphicBoth = (Sub Dict, Sub Dict)

checkDCPolyProduct
  :: DefaultConstraints p (PolyProduct a b c) (PolyProduct a' b' c') :<=>:
     (ProductProfunctor p, Default p a a', Default p b b', Default p c c')
checkDCPolyProduct = (Sub Dict, Sub Dict)
