Dependently typed iterator (i.e. induction principle) troubles

[catalin-hritcu]

I'm trying to use a dependently typed iterator (i.e. induction principle) on trees, but subtyping is not smart enough to figure this out.

type tree =
  | Leaf : tree
  | Node : n:int -> tree -> tree -> tree

val in_tree : int -> tree -> Tot bool
let rec in_tree x t =
  match t with
  | Leaf -> false
  | Node n t1 t2 -> x = n || in_tree x t1 || in_tree x t2

val ind : ta:(tree -> Type) ->
          f:(t1:tree -> t2:tree -> n:int -> ta t1 -> ta t2 -> ta (Node n t1 t2)) ->
          a:(ta Leaf) -> t:tree -> (ta t)
let rec ind ta f a t =
  match t with
  | Leaf -> a
  | Node n t1 t2 -> f t1 t2 n (ind ta f a t1) (ind ta f a t2)

#set-options "--initial_fuel 10 --max_fuel 10 --initial_ifuel 10 --max_ifuel 10"
val find' : f:(int -> Tot bool) -> t:tree -> Tot (option (x:int{f x && in_tree x t}))
let find' f = ind (fun t -> option (x:int{f x && in_tree x t}))
                  (fun t1 t2 n o1 o2 -> if f n then Some n else
                                        if Some? o1 then o1 else o2) None

(Error) Subtyping check failed; expected type (option (x#10651:int{(b2t (op_AmpAmp (f x@0) (in_tree x@0 (Node n t1 t2))))})); got type (option (x#10651:int{(b2t (op_AmpAmp (f x@0) (in_tree x@0 t2)))})) 

[catalin-hritcu]

Here is another example that works though:

val all' : p:(int -> Tot bool) -> t:tree ->
            Tot (r:bool{r <==> (forall x. in_tree x t ==> p x)})
let all' p = ind (fun t -> r:bool{r <==> (forall x. in_tree x t ==> p x)})
                 (fun t1 t2 n b1 b2 -> p n && b1 && b2) true

[kyoDralliam]

Your problem here seems come from the absence of covariance for option, ie the following code fails

let f (x:option nat) : option int = x

I don't know if the implementation of polarities by @aseemr would allow us to extend the subtyping system with it, but that might be one solution.

[catalin-hritcu]

Thanks Kenji for finding the cause (#65). Closing as duplicate.