ConstraintUnion.hs

{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, KindSignatures #-}
{-# LANGUAGE LiberalTypeSynonyms, RankNTypes, ScopedTypeVariables           #-}
{-# LANGUAGE TypeFamilies, TypeOperators, TypeSynonymInstances              #-}
module ConstraintUnion where
import Data.Kind
import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.Prelude.Ord
import Data.Type.Equality
import GHC.TypeNats

type family PerfectWitness (p :: Bool) a where
  PerfectWitness 'False a = ()
  PerfectWitness 'True  a = a -> a

class KnownNat (Chara k) => Field k where
  type Chara k :: Nat

class (Field k) => PerfectField k where
  witness :: proxy k -> PerfectWitness (2 :<= Chara k) k

instance Field Rational where
  type Chara Rational = 0

instance PerfectField Rational where
  witness _ = ()

instance Field Bool where
  type Chara Bool = 2

instance PerfectField Bool where
  witness _ = id

invFrob :: forall k. PerfectField k => k -> Maybe k
invFrob i =
  case (sing :: Sing 2) %:<= (sing :: Sing (Chara k)) of
    SFalse -> Nothing
    STrue  -> Just $ witness (Proxy :: Proxy k) i

WithGADTs.hs

data Perfectness k where
  CharZero :: Chara k ~ 0 => Perfectness k
  CharPos  :: (2 <= Chara k) => (k -> k) -> Perfectness k

class Field k => PerfectField' k where
  pWit :: Perfectness k

instance PerfectField' Rational where
  pWit = CharZero

instance PerfectField' Bool where
  pWit = CharPos id

invFrob' :: forall k. PerfectField' k => k -> Maybe k
invFrob' =
  case pWit @k of
    CharZero  -> const Nothing
    CharPos f -> Just . f