content: {-|
  Description : Decideable equality (i.e. evidence of non-equality) on type families
  Copyright   : (c) Galois, Inc 2014-2019
  Maintainer  : Langston Barrett <langston@galois.com>
  
  This defines a class @DecidableEq@, which represents decidable equality on a
  type family.
  
  This is different from GHC's @TestEquality@ in that it provides evidence
  of non-equality. In fact, it is a superclass of @TestEquality@.
  -}
  {-# LANGUAGE CPP #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE Safe #-}
  #if __GLASGOW_HASKELL__ < 806
  {-# LANGUAGE TypeInType #-}
  #endif
  module Data.Parameterized.DecidableEq
    ( DecidableEq(..)
    ) where
  
  import Data.Void (Void)
  import Data.Type.Equality ((:~:))
  
  -- | Decidable equality.
  class DecidableEq f where
    decEq :: f a -> f b -> Either (a :~: b) ((a :~: b) -> Void)
  
  -- TODO: instances for sums, products of types with decidable equality
  
  -- import Data.Type.Equality ((:~:), TestEquality(..))
  -- instance (DecidableEq f) => TestEquality f where
  --   testEquality a b =
  --     case decEq a b of
  --       Left  prf -> Just prf
  --       Right _   -> Nothing
  