src/Idris/Core/CaseTree.hs:(701,1)-(710,51): Non-exhaustive patterns in function varRule

ChainedComparison.idr

module Control.ChainedComparison

%default total
%access export

public export
data Direction = Ascending | Descending

data ComparisonChain : Direction -> Type -> Type where
  Vacuous : ComparisonChain d ty
  Ordered : (next : ty) -> ComparisonChain d ty
  Unordered : ComparisonChain d ty


-- -- NOTE:
-- -- With this section uncommented, the error disappears.
--
-- data CompareList : Type -> Type where
--   Nil : CompareList ty
--   (::) : Lazy ty -> CompareList ty -> CompareList ty
--
-- implicit
-- singleton : ty -> CompareList ty
-- singleton x = [Delay x]


data ComparisonLink : Type -> Type where
  ListLink : Lazy (List ty) -> ComparisonLink ty
  ValueLink : Lazy ty -> ComparisonLink ty

implicit
listLink : List ty -> ComparisonLink ty
listLink xs = ListLink xs

implicit
valueLink : ty -> ComparisonLink ty
valueLink x = ValueLink x

chain : ComparisonChain d ty -> Bool
chain Vacuous = True
chain (Ordered _) = True
chain Unordered = False

implicit
fromValue : ty -> ComparisonChain d ty
fromValue x = Ordered x

implicit
fromList : Ord ty => (xs : List ty) -> ComparisonChain d ty
fromList {d = d} [] = Vacuous
fromList {d = Ascending} (x :: xs) = Ordered (foldr max x xs)
fromList {d = Descending} (x :: xs) = Ordered (foldr min x xs)

chainWith : Ord ty => (op : ty -> ty -> Bool) ->
            %static ComparisonChain d ty -> ComparisonLink ty -> ComparisonChain d ty
chainWith _ Vacuous (ValueLink y) = fromValue y
chainWith _ Vacuous (ListLink ys) = fromList ys
chainWith _ Unordered _ = Unordered
chainWith op (Ordered x) (ValueLink y) = if op x y
                                            then Ordered y
                                            else Unordered
chainWith op (Ordered x) (ListLink []) = Ordered x
chainWith op (Ordered x) (ListLink ys) = if all (op x) ys
                                            then fromList ys
                                            else Unordered

(<) : Ord ty => ComparisonChain Ascending ty -> ComparisonLink ty -> ComparisonChain Ascending ty
(<) = chainWith (<)

(<=) : Ord ty => ComparisonChain Ascending ty -> ComparisonLink ty -> ComparisonChain Ascending ty
(<=) = chainWith (<=)

(>=) : Ord ty => ComparisonChain Descending ty -> ComparisonLink ty -> ComparisonChain Descending ty
(>=) = chainWith (>=)

(>) : Ord ty => ComparisonChain Descending ty -> ComparisonLink ty -> ComparisonChain Descending ty
(>) = chainWith (>)

-- the error is due to this function
test2232 : Bool
test2232 = chain (2.0 <= [2.0, 3.0] <= 2.0)