Multiple solutions found in search error

[ska80]

Steps to Reproduce

Heap.idr:

data Heap : Type -> Type where
  Empty : Ord elem => Heap elem
  Node : Ord elem => Int -> elem -> Heap elem -> Heap elem -> Heap elem

merge : Heap elem -> Heap elem -> Heap elem
merge heap Empty = heap
merge Empty heap = heap
merge h1@(Node _ elem1 left1 right1) h2@(Node _ elem2 left2 right2) =
  if elem1 <= elem2
     then makeT elem1 left1 (merge right1 h2)
     else makeT elem2 left2 (merge h1 right2)
  where
    rank : Heap elem -> Int
    rank Empty = 0
    rank (Node r _ _ _) = r

    makeT : elem -> Heap elem -> Heap elem -> Heap elem
    makeT x left right = if rank left >= rank right
                            then Node (rank right + 1) x left right
                            else Node (rank left + 1) x right left

$ idris2 --check Heap.idr

Expected Behavior

1/1: Building Heap (Heap.idr)

Observed Behavior

1/1: Building Heap (Heap.idr)
Heap.idr:19:34--20:29:While processing right hand side of Main.merge at Heap.idr:8:1--21:1:
While processing right hand side of 1148:makeT at Heap.idr:18:5--21:1:
Multiple solutions found in search. Possible correct results:
	conArg
	conArg

[edwinb]

The error message is bad, but there are definitely two possible results: one from the first Node, one from the second. There's no guarantee they'd be the same.