Avoid unnecessary quotation in elaboration

fathom/src/surface/elaboration.rs

@@ -645,10 +645,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
         for item in elab_order.iter().copied().map(|i| &surface_module.items[i]) {
             match item {
                 Item::Def(item) => {
-                    let (expr, type_value) =
+                    let (expr, r#type) =
                         self.synth_fun_lit(item.range, item.params, item.expr, item.r#type);
                     let expr_value = self.eval_env().eval(&expr);
-                    let r#type = self.quote_env().quote(self.scope, &type_value);
+                    let type_value = self.eval_env().eval(&r#type);
 
                     self.item_env
                         .push_definition(item.label.1, type_value, expr_value);
@@ -887,13 +887,17 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
         &mut self,
         pattern: &Pattern<ByteRange>,
         r#type: Option<&Term<'_, ByteRange>>,
-    ) -> (CheckedPattern, ArcValue<'arena>) {
+    ) -> (CheckedPattern, core::Term<'arena>, ArcValue<'arena>) {
         match r#type {
-            None => self.synth_pattern(pattern),
+            None => {
+                let (pattern, type_value) = self.synth_pattern(pattern);
+                let r#type = self.quote_env().quote(self.scope, &type_value);
+                (pattern, r#type, type_value)
+            }
             Some(r#type) => {
                 let r#type = self.check(r#type, &self.universe.clone());
                 let type_value = self.eval_env().eval(&r#type);
-                (self.check_pattern(pattern, &type_value), type_value)
+                (self.check_pattern(pattern, &type_value), r#type, type_value)
             }
         }
     }
@@ -958,9 +962,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
 
         Vec::from_iter(params.iter().map(|param| {
             let range = param.pattern.range();
-            let (pattern, type_value) =
+            let (pattern, r#type, type_value) =
                 self.synth_ann_pattern(&param.pattern, param.r#type.as_ref());
-            let r#type = self.quote_env().quote(self.scope, &type_value);
             let (name, _) = self.push_local_param(pattern, type_value);
 
             (range, param.plicity, name, r#type)
@@ -980,8 +983,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
 
         match (surface_term, expected_type.as_ref()) {
             (Term::Let(_, def_pattern, def_type, def_expr, body_expr), _) => {
-                let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
-                let def_type = self.quote_env().quote(self.scope, &def_type_value);
+                let (def_pattern, def_type, def_type_value) =
+                    self.synth_ann_pattern(def_pattern, *def_type);
                 let def_expr = self.check(def_expr, &def_type_value);
                 let def_expr_value = self.eval_env().eval(&def_expr);
 
@@ -1376,8 +1379,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
                 (ann_expr, type_value)
             }
             Term::Let(_, def_pattern, def_type, def_expr, body_expr) => {
-                let (def_pattern, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type);
-                let def_type = self.quote_env().quote(self.scope, &def_type_value);
+                let (def_pattern, def_type, def_type_value) =
+                    self.synth_ann_pattern(def_pattern, *def_type);
                 let def_expr = self.check(def_expr, &def_type_value);
                 let def_expr_value = self.eval_env().eval(&def_expr);
 
@@ -1472,7 +1475,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
                 (fun_type, self.universe.clone())
             }
             Term::FunLiteral(range, params, body_expr) => {
-                self.synth_fun_lit(*range, params, body_expr, None)
+                let (expr, r#type) = self.synth_fun_lit(*range, params, body_expr, None);
+                (expr, self.eval_env().eval(&r#type))
             }
             Term::App(range, head_expr, args) => {
                 let mut head_range = head_expr.range();
@@ -1775,7 +1779,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
                     Value::Stuck(Head::MetaVar(_), _) => {
                         let range = ByteRange::merge(param.pattern.range(), body_expr.range());
                         let (expr, r#type) = self.synth_fun_lit(range, params, body_expr, None);
-                        self.convert(range, expr, &r#type, expected_type)
+                        let type_value = self.eval_env().eval(&r#type);
+                        self.convert(range, expr, &type_value, expected_type)
                     }
                     Value::Stuck(Head::Prim(Prim::ReportedError), _) => {
                         core::Term::Prim(file_range.into(), Prim::ReportedError)
@@ -1801,7 +1806,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
         params: &[Param<'_, ByteRange>],
         body_expr: &Term<'_, ByteRange>,
         body_type: Option<&Term<'_, ByteRange>>,
-    ) -> (core::Term<'arena>, ArcValue<'arena>) {
+    ) -> (core::Term<'arena>, core::Term<'arena>) {
         self.local_env.reserve(params.len());
         let initial_local_len = self.local_env.len();
 
@@ -1843,7 +1848,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
             );
         }
 
-        (fun_lit, self.eval_env().eval(&fun_type))
+        (fun_lit, fun_type)
     }
 
     fn synth_bin_op(

formats/opentype.snap

@@ -30,28 +30,28 @@ def link_table : Pos -> {
 } -> Format -> Format =
 fun file_start table_record table_format => link (file_start + table_record.offset) (limit32 table_record.length table_format);
 def platform_id : Format = u16be;
-def encoding_id : U16 -> Format = fun platform => u16be;
+def encoding_id : Repr platform_id -> Format = fun platform => u16be;
 def empty : Format = ();
 def offset32 : Pos -> Format -> Format = fun base format => {
     offset <- u32be,
     link <- match offset { 0 => empty, _ => link (base + offset) format },
 };
 def language_id : Format = u16be;
-def cmap_language_id : U16 -> Format = fun platform => language_id;
+def cmap_language_id : Repr platform_id -> Format = fun platform => language_id;
 def small_glyph_id : Format = u8;
-def cmap_subtable_format0 : U16 -> Format = fun platform => {
+def cmap_subtable_format0 : Repr platform_id -> Format = fun platform => {
     length <- u16be,
     language <- cmap_language_id platform,
     glyph_id_array <- array16 256 small_glyph_id,
 };
-def cmap_subtable_format2 : U16 -> Format = fun platform => {
+def cmap_subtable_format2 : Repr platform_id -> Format = fun platform => {
     length <- u16be,
     language <- cmap_language_id platform,
     sub_header_keys <- array16 256 u16be,
 };
 def reserved : fun (format : Format) -> Repr format -> Format =
 fun format default => format;
-def cmap_subtable_format4 : U16 -> Format = fun platform => {
+def cmap_subtable_format4 : Repr platform_id -> Format = fun platform => {
     length <- u16be,
     language <- cmap_language_id platform,
     seg_count_x2 <- u16be,
@@ -65,45 +65,46 @@ def cmap_subtable_format4 : U16 -> Format = fun platform => {
     id_delta <- array16 seg_count s16be,
     id_range_offsets <- array16 seg_count u16be,
 };
-def cmap_subtable_format6 : U16 -> Format = fun platform => {
+def cmap_subtable_format6 : Repr platform_id -> Format = fun platform => {
     length <- u16be,
     language <- cmap_language_id platform,
     first_code <- u16be,
     entry_count <- u16be,
     glyph_id_array <- array16 entry_count u16be,
 };
 def language_id32 : Format = u32be;
-def cmap_language_id32 : U16 -> Format = fun platform => language_id32;
+def cmap_language_id32 : Repr platform_id -> Format =
+fun platform => language_id32;
 def sequential_map_group : Format = {
     start_char_code <- u32be,
     end_char_code <- u32be,
     start_glyph_id <- u32be,
 };
-def cmap_subtable_format8 : U16 -> Format = fun platform => {
+def cmap_subtable_format8 : Repr platform_id -> Format = fun platform => {
     _reserved <- reserved u16be 0,
     length <- u32be,
     language <- cmap_language_id32 platform,
     is32 <- array16 8192 u8,
     num_groups <- u32be,
     groups <- array32 num_groups sequential_map_group,
 };
-def cmap_subtable_format10 : U16 -> Format = fun platform => {
+def cmap_subtable_format10 : Repr platform_id -> Format = fun platform => {
     _reserved <- reserved u16be 0,
     length <- u32be,
     language <- cmap_language_id32 platform,
     start_char_code <- u32be,
     num_chars <- u32be,
     glyph_id_array <- array32 num_chars u16be,
 };
-def cmap_subtable_format12 : U16 -> Format = fun platform => {
+def cmap_subtable_format12 : Repr platform_id -> Format = fun platform => {
     _reserved <- reserved u16be 0,
     length <- u32be,
     language <- cmap_language_id32 platform,
     num_groups <- u32be,
     groups <- array32 num_groups sequential_map_group,
 };
 def constant_map_group : Format = sequential_map_group;
-def cmap_subtable_format13 : U16 -> Format = fun platform => {
+def cmap_subtable_format13 : Repr platform_id -> Format = fun platform => {
     _reserved <- reserved u16be 0,
     length <- u32be,
     language <- cmap_language_id32 platform,
@@ -129,14 +130,14 @@ def variation_selector : Pos -> Format = fun table_start => {
     default_uvs_offset <- offset32 table_start default_uvs_table,
     non_default_uvs_offset <- offset32 table_start non_default_uvs_table,
 };
-def cmap_subtable_format14 : U16 -> Pos -> Format =
+def cmap_subtable_format14 : Repr platform_id -> Pos -> Format =
 fun platform table_start => {
     length <- u32be,
     num_var_selector_records <- u32be,
     var_selector <- array32 num_var_selector_records (variation_selector table_start),
 };
 def unknown_table : Format = ();
-def cmap_subtable : U16 -> Format = fun platform => {
+def cmap_subtable : Repr platform_id -> Format = fun platform => {
     table_start <- stream_pos,
     format <- u16be,
     data <- match format {

tests/succeed/equality.snap

@@ -2,51 +2,40 @@ stdout = '''
 let id : fun (A : Type) -> A -> A = fun A a => a;
 let Eq : fun (A : Type) -> A -> A -> Type = fun A a0 a1 => fun (P : A ->
 Type) -> P a0 -> P a1;
-let refl : fun (A : Type) (a : A) (P : A -> Type) -> P a -> P a =
-fun A a P => id (P a);
-let fun_eta_left : fun (f : Type -> Type) (P : (Type -> Type) -> Type) -> P f ->
-P (fun x => f x) = fun f => refl (Type -> Type) f;
-let fun_eta_right : fun (f : Type -> Type) (P : (Type -> Type) -> Type) ->
-P (fun x => f x) -> P f = fun f => refl (Type -> Type) f;
-let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) ->
-Type) -> P f -> P (fun x => f x) = fun f => refl (Type -> Type -> Type) f;
-let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type)
--> Type) -> P (fun x => f x) -> P f = fun f => refl (Type -> Type -> Type) f;
-let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) ->
-Type) -> P f -> P (fun x y => f x y) = fun f => refl (Type -> Type -> Type) f;
-let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type)
--> Type) -> P (fun x y => f x y) -> P f = fun f => refl (Type -> Type ->
+let refl : fun (A : Type) (a : A) -> Eq A a a = fun A a P => id (P a);
+let fun_eta_left : fun (f : Type -> Type) -> Eq (Type ->
+Type) f (fun x => f x) = fun f => refl (Type -> Type) f;
+let fun_eta_right : fun (f : Type -> Type) -> Eq (Type ->
+Type) (fun x => f x) f = fun f => refl (Type -> Type) f;
+let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
+Type) f (fun x => f x) = fun f => refl (Type -> Type -> Type) f;
+let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
+Type) (fun x => f x) f = fun f => refl (Type -> Type -> Type) f;
+let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
+Type) f (fun x y => f x y) = fun f => refl (Type -> Type -> Type) f;
+let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
+Type) (fun x y => f x y) f = fun f => refl (Type -> Type -> Type) f;
+let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
+Type) (fun x => f x) (fun x y => f x y) = fun f => refl (Type -> Type ->
 Type) f;
-let fun_eta_left : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type) ->
-Type) -> P (fun x => f x) -> P (fun x y => f x y) = fun f => refl (Type -> Type
--> Type) f;
-let fun_eta_right : fun (f : Type -> Type -> Type) (P : (Type -> Type -> Type)
--> Type) -> P (fun x y => f x y) -> P (fun x => f x) = fun f => refl (Type ->
-Type -> Type) f;
-let record_eta_left : fun (r : { x : Type, y : Type }) (P : {
-    x : Type,
-    y : Type,
-} -> Type) -> P r -> P { x = r.x, y = r.y } = fun r => refl {
-    x : Type,
-    y : Type,
-} r;
-let record_eta_right : fun (r : { x : Type, y : Type }) (P : {
+let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type ->
+Type) (fun x y => f x y) (fun x => f x) = fun f => refl (Type -> Type ->
+Type) f;
+let record_eta_left : fun (r : { x : Type, y : Type }) -> Eq {
     x : Type,
     y : Type,
-} -> Type) -> P { x = r.x, y = r.y } -> P r = fun r => refl {
+} r { x = r.x, y = r.y } = fun r => refl { x : Type, y : Type } r;
+let record_eta_right : fun (r : { x : Type, y : Type }) -> Eq {
     x : Type,
     y : Type,
-} r;
-let four_chars : fun (P : U32 -> Type) -> P "beng" -> P 1650814567 =
-refl U32 "beng";
-let three_chars : fun (P : U32 -> Type) -> P "BEN " -> P 1111838240 =
-refl U32 "BEN ";
+} { x = r.x, y = r.y } r = fun r => refl { x : Type, y : Type } r;
+let four_chars : Eq U32 "beng" 1650814567 = refl U32 "beng";
+let three_chars : Eq U32 "BEN " 1111838240 = refl U32 "BEN ";
 let foo : U32 -> U32 = fun x => match x { 1 => 0, x => x };
-let eq_foo : fun (P : (U32 -> U32) -> Type) -> P (fun x => match x {
+let eq_foo : Eq (U32 -> U32) foo foo = refl (U32 -> U32) (fun a => match a {
     1 => 0,
     x => x,
-}) -> P (fun x => match x { 1 => 0, x => x }) = refl (U32 ->
-U32) (fun a => match a { 1 => 0, x => x });
+});
 Type : Type
 '''
 stderr = ''

tests/succeed/format-cond/simple.snap

@@ -2,7 +2,7 @@ stdout = '''
 let format : Format = {
     sfnt_version <- { version <- u32be | version == (0xffff : U32) },
 };
-let _ : { sfnt_version : U32 } -> { sfnt_version : U32 } = fun x => x;
+let _ : Repr format -> { sfnt_version : Repr u32be } = fun x => x;
 () : ()
 '''
 stderr = ''

tests/succeed/format-overlap/dependent.snap

@@ -8,10 +8,7 @@ let silly : Format = overlap {
     record0 <- record0,
     record1 <- record1 record0.length,
 };
-let _ : {
-    record0 : { length : U8 },
-    record1 : { _length : U8, data : Array8 record0.length U8 },
-} -> {
+let _ : Repr silly -> {
     record0 : { length : U8 },
     record1 : { _length : U8, data : Array8 record0.length U8 },
 } = fun silly => silly;

tests/succeed/format-overlap/field-refinements.snap

@@ -1,6 +1,6 @@
 stdout = '''
 let number : Format = overlap { u <- u32be where u >= (2 : U32), s <- s32be };
-let _ : { u : U32, s : S32 } -> { u : U32, s : S32 } = fun n => n;
+let _ : Repr number -> { u : U32, s : S32 } = fun n => n;
 () : ()
 '''
 stderr = ''

tests/succeed/format-overlap/numbers.snap

@@ -1,6 +1,6 @@
 stdout = '''
 let number : Format = overlap { u <- u32be, s <- s32be };
-let _ : { u : U32, s : S32 } -> { u : U32, s : S32 } = fun n => n;
+let _ : Repr number -> { u : U32, s : S32 } = fun n => n;
 () : ()
 '''
 stderr = ''

tests/succeed/format-record/computed-fields.snap

@@ -5,19 +5,14 @@ let format : Format = {
     start_code <- array16 seg_count u16be,
     id_delta <- array16 seg_count s16be,
 };
-let _ : {
-    seg_count_x2 : U16,
-    seg_count : U16,
-    start_code : Array16 seg_count U16,
-    id_delta : Array16 seg_count S16,
-} -> {
+let _ : Repr format -> {
     seg_count_x2 : U16,
     seg_count : U16,
     start_code : Array16 seg_count U16,
     id_delta : Array16 seg_count S16,
 } = fun x => x;
 let format : Format = { let x : U32 = 256 };
-let _ : { x : U32 } -> { x : U32 } = fun x => x;
+let _ : Repr format -> { x : U32 } = fun x => x;
 () : ()
 '''
 stderr = ''

tests/succeed/format-record/field-refinements.snap

@@ -4,11 +4,8 @@ let format : Format = {
     len <- u8 where len <= (16 : U8),
     data <- array8 len u8,
 };
-let _ : { magic : U64, len : U8, data : Array8 len U8 } -> {
-    magic : U64,
-    len : U8,
-    data : Array8 len U8,
-} = fun x => x;
+let _ : Repr format -> { magic : U64, len : U8, data : Array8 len U8 } =
+fun x => x;
 () : ()
 '''
 stderr = ''

tests/succeed/format-repr/pair-dependent.snap

@@ -1,8 +1,7 @@
 stdout = '''
 let array32 : U32 -> Format -> Format = fun len Elem => Elem;
 let pair : Format = { len <- u32be, data <- array32 len u32be };
-let test_pair : { len : U32, data : U32 } -> { len : U32, data : U32 } =
-fun p => p;
+let test_pair : Repr pair -> { len : U32, data : U32 } = fun p => p;
 pair : Format
 '''
 stderr = ''