odd Subtyping check failed %[ EvalExpr.Int; ex ] << %[ t; uu___16 ] ?

[karolserkis]

This is my module that is failing on the | Comp op e1 e2 -> of eval function below, in spite of the previous | Bin op e1 e2 -> being completely ok and both take types 'int -> int ->' that are the same...

module EvalExpr

type ty =
  | Int : ty
  | Bool : ty
type binOp =
  | Add : binOp
  | Mul : binOp
type compOp =
  | Eq : compOp
  | LT : compOp

type var = string

type expr : ty -> Type =
  | Var : var -> expr Int
  | TT : expr Bool
  | FF : expr Bool
  | IntLit : int -> expr Int
  | Bin : binOp -> expr Int -> expr Int -> expr Int
  | Comp : compOp -> expr Int -> expr Int -> expr Bool

type env = var -> Tot (option int)

type value : ty -> Type =
  | IntVal : int -> value Int
  | BoolVal : bool -> value Bool

val binOpSem : binOp -> int -> int -> int
let binOpSem = function
  | Add -> (fun x y -> x + y)
  | Mul -> (fun x y -> x `op_Multiply` y)

val compOpSem : compOp -> int -> int -> bool
let compOpSem = function
  | Eq -> (fun x y -> x = y)
  | LT -> (fun x y -> x < y)

val optMap : ('a -> 'b) -> option 'a -> option 'b
let optMap f xx = match xx with
  |  (None) -> None
  |  (Some x) -> Some (f x)

val eval : env -> #t:ty -> ex:expr t -> option (value t)
let rec eval e #t = function
  | Var v -> optMap IntVal (e v)
  | TT -> Some (BoolVal true)
  | FF -> Some (BoolVal false)
  | IntLit i -> Some (IntVal i)
  | Bin op e1 e2 -> (match eval e e1 , eval e e2 with
     | Some (IntVal i1), Some (IntVal i2) -> Some (IntVal (binOpSem op i1 i2))
     |  _ -> None
     )
  | Comp op e1 e2 -> (match eval e e1 , eval e e2 with
      | Some (IntVal i1), Some (IntVal i2) -> Some (BoolVal (compOpSem op i1 i2))
      | _ -> None
      )

EvalExpr(54,35-54,37): (Error 19) Subtyping check failed; expected type (ex:EvalExpr.expr (EvalExpr.Int){ %[ EvalExpr.Int; ex ] << %[ t; uu___16 ] }); got type EvalExpr.expr (EvalExpr.Int) (see also EvalExpr(45,20-57,7))
Verified module: EvalExpr (3343 milliseconds)
1 error was reported (see above)

I am unsure what its complaining about and don't understand how to proceed here.

[aseemr]

Hi, you need to annotate the eval function to help F* prove termination:

val eval : env -> #t:ty -> ex:expr t -> Tot (option (value t)) (decreases ex)

The decreases clause tells F* that ex decreases in the recursive calls to eval.

[aseemr]

Hope this helps, you could also read more about it here (Sec. 5): https://fstar-lang.org/tutorial/.

[karolserkis]

Thanks! I understand now. The notation of the error message "%[" << and "uu___16 ] " confused me, but if I just look at the: ex:EvalExpr.expr (EvalExpr.Int) ------ vs ------ EvalExpr.Int; ex it pointed me in the right place. Thanks it worked! All verified.

[aseemr]

Great! Closing the issue.

[WolframKahl]

On Fri, Mar 23, 2018 at 01:04:32AM +0000, Karol Serkis wrote:

val eval : env -> #t:ty -> ex:expr t -> option (value t) let rec eval e #t = function [...] | Comp op e1 e2 -> (match eval e e1 , eval e e2 with | Some (IntVal i1), Some (IntVal i2) -> Some (BoolVal (compOpSem op i1 i2)) | _ -> None ) EvalExpr(54,35-54,37): (Error 19) Subtyping check failed; expected type (ex:EvalExpr.expr (EvalExpr.Int){ %[ EvalExpr.Int; ex ] << %[ t; uu___16 ] }); got type EvalExpr.expr (EvalExpr.Int) (see also EvalExpr(45,20-57,7))

The << indicates a termination check problem: You need (decreases ex).

[karolserkis]

After reading (Sec. 5) of the tutorial more carefully, I see that more clearly now! Thanks.