DynBounded.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module DynBounded where
  
import Data.Proxy
import Data.Reflection
import Data.Constraint
import Data.Constraint.Unsafe


newtype Lift (p :: * -> Constraint) (a :: *) (s :: *) =
    Lift { lower :: a }


class ReifiableConstraint p
  where
    data Def (p :: * -> Constraint) (a :: *) :: *
    reifiedIns :: Reifies s (Def p a) :- p (Lift p a s)


using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a
using d m =
    reify d $ \(_ :: Proxy s) ->
      let
        replaceProof :: Reifies s (Def p a) :- p a
        replaceProof = trans proof reifiedIns
          where
            proof = unsafeCoerceConstraint :: p (Lift p a s) :- p a
      in
        m \\ replaceProof


instance ReifiableConstraint Bounded
  where
    data Def Bounded a = Bounded { minBound_ :: a, maxBound_ :: a }
    reifiedIns = Sub Dict


instance Reifies s (Def Bounded a) => Bounded (Lift Bounded a s)
  where
    minBound = Lift $ minBound_ (reflect (Proxy :: Proxy s))
    maxBound = Lift $ maxBound_ (reflect (Proxy :: Proxy s))


example1 :: (Int, Int)
example1 =
    (minBound, maxBound)


example2 :: (Int, Int)
example2 =
    (using (Bounded 0 42) minBound, using (Bounded 0 42) maxBound)