Stefan pushed to branch master at Stefan / Typer

Commits: a7ac505a by Jean-Alexandre Barszcz at 2021-08-10T14:58:56-04:00 * src/elab.ml (elaborate): `check_inferred` when a type is given.

Previously, `check_inferred` was mainly called from `check`, but some calls to `elaborate` play the same role as `check` (if an expected type is given), so we move this logic to `elaborate`. This allows implicit arguments to be instantiated in more places. For example, calls and variables are always inferred, but without `check_inferred`, the type provided to `elaborate` would be ignored.

- - - - -

2 changed files:

- src/elab.ml - tests/elab_test.ml

Changes:

===================================== src/elab.ml ===================================== @@ -543,7 +543,7 @@ let elab_p_id ((l,name) : symbol) : vname =

(* Infer or check, as the case may be. *) let rec elaborate ctx se ot = - match se with + let (e, res_t) = match se with (* Rewrite SYM to `typer-identifier SYM`. *) | Symbol ((loc, name) as id) -> if not (name = "typer-identifier") then @@ -572,7 +572,17 @@ let rec elaborate ctx se ot = * Maybe I should only elaborate `func` above if it's a symbol * (and maybe even use `elab_varref` rather than indirecting * through `typer-identifier`)? *) - elab_call ctx ft args + elab_call ctx ft args in + match ot with + | Some t -> + (match res_t with + | Checked -> (e, res_t) + | _ -> let inferred_t = + match res_t with + | Inferred t -> t + | _ -> OL.get_type (ectx_to_lctx ctx) e in + (check_inferred ctx e inferred_t t, Checked)) + | _ -> (e, res_t)

and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with @@ -663,12 +673,7 @@ and unify_with_arrow ctx tloc lxp kind var aty | [] -> arg, body

and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = - let (e, ot) = elaborate ctx p (Some t) in - match ot with - | Checked -> e - | _ -> let inferred_t = match ot with Inferred t -> t - | _ -> OL.get_type (ectx_to_lctx ctx) e in - check_inferred ctx e inferred_t t + fst (elaborate ctx p (Some t))

and unify_or_error lctx lxp ?lxp_name expect actual = match Unif.unify expect actual lctx with

===================================== tests/elab_test.ml ===================================== @@ -231,4 +231,11 @@ type Lift (l ::: TypeLevel) (t :: Type_ l) (x : t) | mkLift; |}

+let _ = add_elab_test_decl + "Check and instantiate implicit args when a type is given" + {| +test : Int -> ?a -> ?a; +test _ = I; + |} + let _ = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/a7ac505a8249a889aa1235f6823b1c7073...