FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Cannot match implicit arg using constructor

Open mtzguido opened this issue 1 year ago • 1 comments

The second match fails with 'syntax error', but the fact that the argument is implicit should not make a difference.

noeq
type t2 = | Mk2 : _:int -> t2

let test2 (x:t2) : int =
  match x with
  | Mk2 0 -> 0
  | _ -> 1

noeq
type t1 = | Mk1 : #_:int -> t1

let test1 (x:t1) : int =
  match x with
  | Mk1 #0 -> x
  | _ -> 1

mtzguido avatar Sep 06 '24 20:09 mtzguido

To fix this, we should probably move the aqual in PatVar into the list in PatApp. Currently PatConst cannot be marked implicit.

mtzguido avatar Oct 06 '24 14:10 mtzguido