Unable to instantiate

[michaelbjames]

data List a where
    Nil :: List a
    Cons :: x: a -> xs: List a -> List a

termination measure len :: List a -> {Int | _v >= 0} where
  Nil -> 0
  Cons x xs -> 1 + len xs

snoc ::
        (xs: List a -> x: a ->  {List a | len _v == (len xs + 1)}) ^
        (xs: {List a | _v == Nil} -> x: a ->  {List a | _v == (Cons x Nil)}) ^
        (xs: {List Int| _v == (Cons 2 Nil)} -> x: {Int | _v == 1} -> {List Int | _v == (Cons 2 (Cons 1 Nil))}) ^
        (xs: {List Int| _v == (Nil)} -> x: {Int | _v == 1} -> {List Int | _v == (Cons 1 Nil)})
snoc = \xs. \x.
    match xs with
        Nil -> Cons x Nil
        Cons y ys -> Cons y (snoc ys x)

Should the last refinement be necessary?

[michaelbjames]

This is an interesting case:

1. This comes from how Z3 now encodes those constructors. The polymorphic Nil is actually Nil_List_Var_a and the concrete one is Nil_List_Int. They're just different sorts.
2. Any user would expect not to need the concrete case. This wasn't a problem before the z3 instantiation.

I'm not sure the best way forward.