Idris can't solve constraint despite case split

Question

In an attempt to try to learn Idris, I've decided to try to use it to implement red-black trees. After some struggling, I've managed to get the tree itself past the typechecker, and I am now trying to define an insert function which as the name implies inserts an element into a red-black tree. In its current, rather incomplete, state the relevant parts of my code look like this:

data Color : Type where
  Red : Color
  Black : Color

mutual
    data RedBlackTree : (Ord key_type) => Nat -> Color -> (key_type : Type) -> Type -> Type where
        Empty : (impl : Ord key_type) => RedBlackTree @{impl} Z Black key_type v

        BlackNode : (impl : Ord key_type) => (k : key_type) -> value_type ->
            (left : RedBlackTree @{impl} black_height c_1 key_type value_type) ->
            (right : RedBlackTree @{impl} black_height c_2 key_type value_type) ->
            {auto left_legal : legal_child_of_key left k LT} ->
            {auto right_legal : legal_child_of_key right k GT} ->
            RedBlackTree @{impl} (S black_height) Black key_type value_type

        RedNode : (impl : Ord key_type) => (k : key_type) -> value_type ->
            (left : RedBlackTree @{impl} black_height Black key_type value_type) ->
            (right : RedBlackTree @{impl} black_height Black key_type value_type) ->
            {auto left_legal : legal_child_of_key left k LT} ->
            {auto right_legal : legal_child_of_key right k GT} ->
            RedBlackTree @{impl} black_height Red key_type value_type

    legal_child_of_key : (impl : Ord k_type) => RedBlackTree @{impl} _ _ k_type _ -> k_type -> Ordering -> Type
    legal_child_of_key Empty _ _ = Unit
    legal_child_of_key (BlackNode child_key _ _ _) parent_key ord = ord = (compare @{impl} child_key parent_key)
    legal_child_of_key (RedNode child_key _ _ _) parent_key ord = ord = (compare @{impl} child_key parent_key)

TreeMap : (Ord k) => (k : Type) -> Type -> Type
TreeMap @{impl} k v = DPair (Nat, Color) $ \case (d, c) => RedBlackTree @{impl} d c k v

insert : (impl : Ord k) => TreeMap @{impl} k v -> k -> v -> TreeMap @{impl} k v
insert (((S d), Black) ** (BlackNode @{impl} p_k p_v left right)) k v = case compare @{impl} k p_k of
    LT => case left of
        Empty => MkDPair (S d, Black) (BlackNode @{impl} p_k p_v (RedNode @{impl} k v Empty Empty) right {left_legal = ?left_legal_prf})
        real_node => ?insert_left_black

The problem I'm facing is that Idris doesn't let me fill that ?left_legal_prf hole with left_legal = Refl, claiming that it can't solve the constraint between compare k p_k and LT. This despite just having pattern matched on compare k p_k and finding it to be LT. Explicitly providing the type like the (LT = compare @{impl} key p_k) Refl doesn't seem to help either.

:t left_legal_prf outputs

Data.RedBlackTree> :t left_legal_prf
   impl : Ord k
   right : RedBlackTree 0 c_2 k v
   p_k : k
   p_v : v
   k : k
   v : v
   left : RedBlackTree 0 Black k v
   d : Nat
------------------------------
left_legal_prf : LT = compare k p_k

which I don't find very helpful for solving this particular problem.

Am I wrong when I claim that the constraint should hold? If so, what am I missing? If not, how do I convince the compiler?

michaelmesser michaelmesser · Accepted Answer · 2021-04-20T23:20:09

You can use with ... proof ... to capture the proof. Here is an example from Idris 2's test:

filterSquared p (x :: xs) with (p x) proof eq
  filterSquared p (x :: xs) | False = filterSquared p xs -- easy
  filterSquared p (x :: xs) | True
    = rewrite eq in cong (x ::) (filterSquared p xs)

Idris can't solve constraint despite case split

1 Answers