Dependent pattern match on pairs doesn't work; need to use nested pattern-match instead

[msprotz]

The following snippet doesn't work:

module JH

type vec (a: Type): nat -> Type =
  | Nil: vec a 0
  | Cons: hd:a -> n:nat -> tl:vec a n -> vec a (n + 1)

val map2:
  n:nat ->
  f:('a -> 'b -> Tot 'c) ->
  l1:vec 'a n ->
  l2:vec 'b n ->
  Tot (vec 'c n)
let rec map2 n f l1 l2 =
  match l1, l2 with
  | Cons hd1 n1 tl1, Cons hd2 n2 tl2 ->
      Cons (f hd1 hd2) n1 (map2 n1 f tl1 tl2)
  | Nil, Nil ->
      Nil

The following snippet does:

module JH

type vec (a: Type): nat -> Type =
  | Nil: vec a 0
  | Cons: hd:a -> n:nat -> tl:vec a n -> vec a (n + 1)

val map2:
  n:nat ->
  f:('a -> 'b -> Tot 'c) ->
  l1:vec 'a n ->
  l2:vec 'b n ->
  Tot (vec 'c n)
let rec map2 n f l1 l2 =
  match l1 with
  | Cons hd1 n1 tl1 ->
      begin match l2 with
      | Cons hd2 n2 tl2 ->
          Cons (f hd1 hd2) n2 (map2 n2 f tl1 tl2)
      end
  | Nil ->
      begin match l2 with
      | Nil ->
          Nil
      end

I made a quick note of it at https://github.com/FStarLang/FStar/wiki/Early-stumbling-blocks%2C-FAQ#error-pairs because I remember a discussion we had a while ago while I was playing with union-find, and @nikswamy was telling me that nested pattern-matches were better.

If I hallucinated / this is no longer the case / this bug can be fixed easily, then I'll make sure I remove the note in the wiki.

Thanks,

Jonathan

[catalin-hritcu]

The error message for this is

./bug682.fst(17,4-17,8) : (Error) (?41694 'a 'b 'c n f l1 l2) is not equal to the expected type (Bug682.vec (?41538 'a 'b 'c n f l1 l2) (Prims.op_Addition n1 1))

Looks a bit like #291, but not sure whether there is any relation.

[nikswamy]

With @aseemr today, we were revisiting this (also in the context of PR #2473)

It turns out the problem appears because F* has not yet fully inferred the type of the scrutinee when inferring the type of the pattern.

E.g., this works:

let rec map2 (#a #b #c:Type) (n:nat) (f: a -> b -> c) (l1:vec a n) (l2:vec b n)
  : vec c n
  = match l1, l2 <: (vec a n & vec b n) with
    | Cons hd1 n1 tl1, Cons hd2 n2 tl2 ->
           Cons (f hd1 hd2) n1 (map2 n1 f tl1 tl2)
    | Nil, Nil ->
           Nil

We are considering at least adding an error message in this case asking the user to annotate the scrutinee when its type is not informative enough to typecheck the pattern.

In this case, it seems obvious that the type of the scrutinee should be vec a n & vec b n, but due to subtyping, F* defers solving the type of l1, l2, inferring only ?u1 & ?u2 for its type

[aseemr]

Another example from #419, without the annotation on the scrutinee, path_same_repr fails.

module Test

type relation (v: Type) = v → v → Type
noeq
type path (v: Type) (r: v → v → Type): v → v → Type =
  | Refl: x:v → path v r x x
  | Step: x:v → y:v → z:v → r x y → path v r y z → path v r x z

type is_root (v: Type) (f: relation v) (x: v) =
  ∀ y. ¬(f x y)
type is_repr (v: Type) (f: relation v) (x: v) (r: v) =
  path v f x r ∧ is_root v f r

type confined (v: eqtype) (d: Set.set v) (f: relation v) =
  ∀ (x: v) (y: v). path v f x y ⟹ Set.mem x d ∧ Set.mem y d
type functional (v: eqtype) (f: relation v) =
  ∀ (x: v) (y: v) (z: v). f x z ∧ f y z ⟹ x = y
type defined (v: Type) (rel: relation v) =
  ∀ (x: v). ∃ (r: v). rel x r

type is_dsf (v: eqtype) (d: Set.set v) (f: relation v) =
  confined v d f ∧ functional v f ∧ defined v (is_repr v f)

val path_same_repr:
  v:eqtype → d:Set.set v → f:relation v →
  x:v → r:v → z:v → p_1:path v f x z → p_2:path v f x r → Lemma
    (requires (is_dsf v d f ∧ is_root v f r))
    (ensures (is_repr v f z r))
    (decreases %[p_1, p_2])
let rec path_same_repr (v: eqtype) d (f: relation v) x r z p_1 p_2 =
  match (p_1, p_2) <: (path v f x z & path v f x r) with 
  | Refl _, Refl _ →
    admit ()
  | _ → admit ()