Failure of type inference with repeated variables

[kyoDralliam]

Lax-typechecking the following snippet

let f (x y : int) (w:(b:bool & (if b then equals x y else equals y x))) =
  match w with
  | (| b, Refl |) -> ()

fails with the error

(Error) (equals (?26524 x y w b) (?26524 x y w b)) is not a subtype of the expected type (match b with
	| true  -> (equals x y)
	|_  -> (equals y x))

[kyoDralliam]

The error has changed to Expected a trivial pre-condition in current master.

Note that there is now a way to bypass the error by encapsulating the if b then equals x y else equals y x :

let t x y b = if b then x == y else y == x

let f (x y : int) (w:(b:bool & t x y b)) =
  match w with
  | (| b, Refl #int #x |) -> ()

note that the explicit annotations on the Refl are compulsory...

[kyoDralliam]

Going back to this issue, it seems strange that you need to introduce names that are not constrained nor used anywhere (in the previous code #int #x are just fresh variable names...)

[kyoDralliam]

Actually, these variables should just not be bindable in pattern since they comes from parameters (related to #65)