How to implement `Constraint` reflection? [Ad-Hoc polymorphism based on available Constraints]

Question

For example, with types, you can implement AdHoc polymorphism using Typeable to define a different behavior depending on what the input type is:

foo :: forall a. Typeable a => a -> a
foo | Just HRefl <- typeRep @a `eqTypeRep` typeRep @Bool = not
    | otherwise = id

-- >>> foo 3
3
-- >>> foo True
False

I would like to do something similar to that but instead check if a type has a curtain instance of a Constraint, and implement a different behavior on that.

So far I have looked at two packages, Data.Constraint and Data.Exists. I think the solution lies with one of them but I have not been able to understand how I would go about doing this.

For context, this came about when I was thinking about what a polymorphic safe integer division function would look like

polymorphicSafeDiv :: Integral a => a -> a -> Maybe a
polymorphicSafeDiv x y = undefined

If I want this function to work for both bounded and unbounded Integrals I need to consider both, division by zero, and the overflow scenario for minBound @Int / (-1). I would imagine something like

polymorphicSafeDiv :: Integral a => a -> a -> Maybe a
polymorphicSafeDiv x y
 | y == 0    = Nothing
 | y == (-1) = case (???) of
                 Just Relf -> Nothing
                 _         -> Just $ x `div` y
 | otherwise = Just $ x `div` y

Answer 1

The idiomatic way to do this is to make a new class.

class    LowerBound a       where lowerBound :: Maybe a
instance LowerBound Int     where lowerBound = Just minBound
instance LowerBound Integer where lowerBound = Nothing

polymorphicSafeDiv :: (LowerBound a, Integral a) => a -> a -> Maybe a
polymorphicSafeDiv x = \case
    0  -> Nothing
    -1 -> case lowerBound of
        Just lb | x == lb -> Nothing
        _ -> Just (x `div` y)
    y  -> Just (x `div` y)

Actually, I'm not sure LowerBound is a great name for this. For example, Word has a lower bound, but dividing it by other things shouldn't produce Nothing. Perhaps you should make a division class directly.

class Integral a => SafeDivide a where
    safeDiv :: a -> a -> Maybe a
    default safeDiv :: Bounded a => a -> a -> Maybe a
    safeDiv x = \case
        -1 | x == minBound -> Nothing
        y -> testZeroDiv x y

testZeroDiv :: Integral a => a -> a -> Maybe a
testZeroDiv x = \case
    0 -> Nothing
    y -> Just (x `div` y)

instance SafeDivide Int
instance SafeDivide Integer where safeDiv = testZeroDiv
instance SafeDivide Word    where safeDiv = testZeroDiv

Answer 2

Using the if-instance as suggested in the comments leads to a very ergonomic way to express what I wanted, although any calling code will need the extension turned on as well

{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}

module Main where

import Data.Constraint.If ( IfSat, ifSat )

polymorphicSafeDiv :: forall a. (IfSat (Bounded a), Integral a) => a -> a -> Maybe a
polymorphicSafeDiv x y 
  | y == 0    = Nothing
  | otherwise = ifSat @(Bounded a) boundedSafeDiv optmisticDiv
  where
    optmisticDiv = Just $ x `div` y 

    boundedSafeDiv :: (Bounded a, Integral a) => Maybe a
    boundedSafeDiv
      | y == minBound `quot` maxBound = if x == minBound then Nothing else optmisticDiv
      | otherwise                     = optmisticDiv

main :: IO ()
main = do 
  print (polymorphicSafeDiv (minBound @Int ) (-1))
  print (polymorphicSafeDiv (minBound @Int ) (-2))
  print (polymorphicSafeDiv (minBound @Int ) 0   )
  print (polymorphicSafeDiv (minBound @Word) 0   )
  print (polymorphicSafeDiv (minBound @Word) maxBound)
  print (polymorphicSafeDiv (2^128)          (-1))
  print (polymorphicSafeDiv (2^128)          0   )

{-
Nothing
Just 4611686018427387904
Nothing
Nothing
Just 0
Just (-340282366920938463463374607431768211456)
Nothing
-}