gistfile1.hs

data Range ty
  = Range Int Int
  | DummyRange

data AnyNumber = AnyNumber
data Positive
data NonZeroPos
data Nullable a
data RangeToFrom

type family RangeSubset a b where
  RangeSubset (Range a) (Range AnyNumber) = 'True
  RangeSubset (Range RangeToFrom) (Range RangeToFrom) = 'True
  RangeSubset (Range Positive) (Range Positive) = 'True
  RangeSubset (Range NonZeroPos) (Range Positive) = 'True
  RangeSubset (Range (Nullable a)) (Range (Nullable b)) = RangeSubset a b
  RangeSubset a (Range (Nullable b)) = RangeSubset a (Range b)
  RangeSubset (Range NonZeroPos) (Range NonZeroPos) = 'True
  RangeSubset a b = 'False

valueSubset :: RangeSubset a b ~ 'True => a -> b -> Bool
valueSubset (Range _fromA _toA) (Range _fromB _toB) = undefined
valueSubset _ _ = True

positive :: Range Positive
positive = DummyRange

nonZero :: Range NonZeroPos
nonZero = DummyRange

nullPositive :: Range (Nullable Positive)
nullPositive = DummyRange

range :: Int -> Int -> Range RangeToFrom
range a b = Range a b

-- • Could not deduce: a ~ Range ty0
--   from the context: RangeSubset a b ~ 'True
--     bound by the type signature for:
--                valueSubset :: forall a b.
--                               (RangeSubset a b ~ 'True) =>
--                               a -> b -> Bool
--     at src/NewRange.hs:32:1-56
--   ‘a’ is a rigid type variable bound by
--     the type signature for:
--       valueSubset :: forall a b.
--                      (RangeSubset a b ~ 'True) =>
--                      a -> b -> Bool
--     at src/NewRange.hs:32:1-56
-- • In the pattern: Range _fromA _toA
--   In an equation for ‘valueSubset’:
--       valueSubset (Range _fromA _toA) (Range _fromB _toB) = undefined
-- • Relevant bindings include
--     valueSubset :: a -> b -> Bool (bound at src/NewRange.hs:33:1)