And ordering in refinement type preventing type checking, PR 3004.

[briangmilnes]

Folks, A Seq length = n constraint in a conjunctive refinement type is order dependent. (*

This demonstrates a type checking problem in which a sequence is used before it's length is specified in the next conjunct and an error occurs. Flip the and it passes.

*)

module AndOrderBug

open FStar.Seq

type seqN n = (s: seq int{length s = n}) let seqprop n (s0: seqN n) (sp: seqN n) (s1: seqN n) = True

let seqswapgood (s0: seqN 1) (sp: seqN 1) (s1: seq int{length s1 = 1 /\ seqprop 1 s0 sp s1 }) : Tot unit = ()

// And ordering here prevents type checking in PR 3004.

let seqswapbad (s0: seqN 1) (sp: seqN 1) (s1: seq int{seqprop 1 s0 sp s1 /\ length s1 = 1}) : Tot unit = ()