Merge builtins in a single enum

5 files changed, 103 insertions, 134 deletions

diff --git a/dhall/src/core.rs b/dhall/src/core.rs
index ccaf0f5..c5b6d86 100644
--- a/dhall/src/core.rs
+++ b/dhall/src/core.rs
@@ -126,10 +126,8 @@ pub enum Expr<'i, S, A> {
     Let(&'i str, Option<Box<Expr<'i, S, A>>>, Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
     ///  `Annot x t                                ~  x : t`
     Annot(Box<Expr<'i, S, A>>, Box<Expr<'i, S, A>>),
-    /// Built-in types
-    BuiltinType(BuiltinType),
-    /// Built-in function values
-    BuiltinValue(BuiltinValue),
+    /// Built-in values
+    Builtin(Builtin),
     ///  `BoolLit b                                ~  b`
     BoolLit(bool),
     ///  `BoolAnd x y                              ~  x && y`
@@ -183,9 +181,9 @@ pub enum Expr<'i, S, A> {
     FailedParse(String, Vec<Expr<'i, S, A>>),
 }
 
-/// Built-in types
+/// Built-ins
 #[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum BuiltinType {
+pub enum Builtin {
     ///  `Bool                                     ~  Bool`
     Bool,
     ///  `Natural                                  ~  Natural`
@@ -200,11 +198,6 @@ pub enum BuiltinType {
     List,
     ///  `Optional                                 ~  Optional`
     Optional,
-}
-
-/// Built-in function values
-#[derive(Debug, Copy, Clone, PartialEq, Eq)]
-pub enum BuiltinValue {
     ///  `NaturalFold                              ~  Natural/fold`
     NaturalFold,
     ///  `NaturalBuild                             ~  Natural/build`
@@ -246,15 +239,9 @@ impl<'i, S, A> From<&'i str> for Expr<'i, S, A> {
     }
 }
 
-impl<'i, S, A> From<BuiltinType> for Expr<'i, S, A> {
-    fn from(t: BuiltinType) -> Self {
-        Expr::BuiltinType(t)
-    }
-}
-
-impl<'i, S, A> From<BuiltinValue> for Expr<'i, S, A> {
-    fn from(t: BuiltinValue) -> Self {
-        Expr::BuiltinValue(t)
+impl<'i, S, A> From<Builtin> for Expr<'i, S, A> {
+    fn from(t: Builtin) -> Self {
+        Expr::Builtin(t)
     }
 }
 
@@ -406,8 +393,7 @@ impl<'i, S, A: Display> Expr<'i, S, A> {
         match self {
             &Var(a) => a.fmt(f),
             &Const(k) => k.fmt(f),
-            &BuiltinType(t) => t.fmt(f),
-            &BuiltinValue(v) => v.fmt(f),
+            &Builtin(v) => v.fmt(f),
             &BoolLit(true) => f.write_str("True"),
             &BoolLit(false) => f.write_str("False"),
             &IntegerLit(a) => a.fmt(f),
@@ -459,29 +445,30 @@ impl Display for Const {
     }
 }
 
-impl Display for BuiltinType {
-    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        <Self as fmt::Debug>::fmt(self, f)
-    }
-}
-
-impl Display for BuiltinValue {
+impl Display for Builtin {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        use crate::BuiltinValue::*;
+        use crate::Builtin::*;
         f.write_str(match *self {
+            Bool     => "Bool",
+            Natural  => "Natural",
+            Integer  => "Integer",
+            Double   => "Double",
+            Text     => "Text",
+            List     => "List",
+            Optional => "Optional",
+            NaturalFold => "Natural/fold",
+            NaturalBuild => "Natural/build",
+            NaturalIsZero => "Natural/isZero",
+            NaturalEven => "Natural/even",
+            NaturalOdd => "Natural/odd",
+            NaturalShow => "Natural/show",
             ListBuild => "List/build",
             ListFold => "List/fold",
+            ListLength => "List/length",
             ListHead => "List/head",
-            ListIndexed => "List/indexed",
             ListLast => "List/last",
-            ListLength => "List/length",
+            ListIndexed => "List/indexed",
             ListReverse => "List/reverse",
-            NaturalBuild => "Natural/build",
-            NaturalEven => "Natural/even",
-            NaturalFold => "Natural/fold",
-            NaturalIsZero => "Natural/isZero",
-            NaturalOdd => "Natural/odd",
-            NaturalShow => "Natural/show",
             OptionalFold => "Optional/fold",
         })
     }
@@ -658,8 +645,7 @@ pub fn shift<'i, S, T, A: Clone>(d: isize, v: V, e: &Expr<'i, S, A>) -> Expr<'i,
             Let(f, mt2, bx(r2), bx(e2))
         }
         Annot(ref a, ref b) => shift_op2(Annot, d, v, a, b),
-        BuiltinType(t) => BuiltinType(t),
-        BuiltinValue(v) => BuiltinValue(v),
+        Builtin(v) => Builtin(v),
         BoolLit(a) => BoolLit(a),
         BoolAnd(ref a, ref b) => shift_op2(BoolAnd, d, v, a, b),
         BoolOr(ref a, ref b) => shift_op2(BoolOr, d, v, a, b),
@@ -756,8 +742,7 @@ pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> E
             Let(f, mt2, bx(r2), bx(b2))
         }
         Annot(ref a, ref b) => subst_op2(Annot, v, e, a, b),
-        BuiltinType(t) => BuiltinType(t),
-        BuiltinValue(v) => BuiltinValue(v),
+        Builtin(v) => Builtin(v),
         BoolLit(a) => BoolLit(a),
         BoolAnd(ref a, ref b) => subst_op2(BoolAnd, v, e, a, b),
         BoolOr(ref a, ref b) => subst_op2(BoolOr, v, e, a, b),
@@ -829,7 +814,7 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
           T: Clone + fmt::Debug,
           A: Clone + fmt::Debug,
 {
-    use crate::BuiltinValue::*;
+    use crate::Builtin::*;
     use crate::Expr::*;
     match *e {
         Const(k) => Const(k),
@@ -854,12 +839,12 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
             }
             f2 => match (f2, normalize::<S, T, A>(a)) {
                 // fold/build fusion for `List`
-                (App(box BuiltinValue(ListBuild), _), App(box App(box BuiltinValue(ListFold), _), box e2)) |
-                (App(box BuiltinValue(ListFold), _), App(box App(box BuiltinValue(ListBuild), _), box e2)) |
+                (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) |
+                (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) |
 
                 // fold/build fusion for `Natural`
-                (BuiltinValue(NaturalBuild), App(box BuiltinValue(NaturalFold), box e2)) |
-                (BuiltinValue(NaturalFold), App(box BuiltinValue(NaturalBuild), box e2)) => normalize(&e2),
+                (Builtin(NaturalBuild), App(box Builtin(NaturalFold), box e2)) |
+                (Builtin(NaturalFold), App(box Builtin(NaturalBuild), box e2)) => normalize(&e2),
 
             /*
                 App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero ->
@@ -885,14 +870,14 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
                         go (Var "Zero")          = True
                         go  _                    = False
                         */
-                (BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
-                (BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
-                (BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
-                (BuiltinValue(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
-                (App(f@box BuiltinValue(ListBuild), box t), k) => {
+                (Builtin(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0),
+                (Builtin(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0),
+                (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
+                (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
+                (App(f@box Builtin(ListBuild), box t), k) => {
                         let labeled =
                             normalize::<_, T, _>(&app(app(app(k.clone(), app(
-                                BuiltinType(self::BuiltinType::List), t.clone())), "Cons"), "Nil"));
+                                Builtin(self::Builtin::List), t.clone())), "Cons"), "Nil"));
 
                         fn list_to_vector<'i, S, A>(v: &mut Vec<Expr<'i, S, A>>, e: Expr<'i, S, A>)
                             where S: Clone, A: Clone
@@ -922,20 +907,20 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
                             app(App(f, bx(t)), k)
                         }
                     }
-                (App(box App(box App(box App(box BuiltinValue(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
+                (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => {
                     let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr
                         App(bx(App(cons.clone(), bx(y))), bx(ys))
                     );
                     normalize(&e2)
                 }
                 (App(f, x_), ListLit(t, ys)) => match *f {
-                    BuiltinValue(ListLength) =>
+                    Builtin(ListLength) =>
                         NaturalLit(ys.len()),
-                    BuiltinValue(ListHead) =>
+                    Builtin(ListHead) =>
                         normalize(&OptionalLit(t, ys.into_iter().take(1).collect())),
-                    BuiltinValue(ListLast) =>
+                    Builtin(ListLast) =>
                         normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())),
-                    BuiltinValue(ListReverse) => {
+                    Builtin(ListReverse) => {
                         let mut xs = ys;
                         xs.reverse();
                         normalize(&ListLit(t, xs))
@@ -972,8 +957,7 @@ pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A>
             normalize(&b3)
         }
         Annot(ref x, _) => normalize(x),
-        BuiltinType(t) => BuiltinType(t),
-        BuiltinValue(v) => BuiltinValue(v),
+        Builtin(v) => Builtin(v),
         BoolLit(b) => BoolLit(b),
         BoolAnd(ref x, ref y) => {
             with_binop(BoolAnd, Expr::bool_lit,
diff --git a/dhall/src/grammar.lalrpop b/dhall/src/grammar.lalrpop
index 150961f..250a45e 100644
--- a/dhall/src/grammar.lalrpop
+++ b/dhall/src/grammar.lalrpop
@@ -5,7 +5,8 @@ use std::iter::FromIterator;
 use crate::core;
 use crate::core::bx;
 use crate::core::Expr::*;
-use crate::core::BuiltinType::*;
+use crate::core::Builtin;
+use crate::core::Builtin::*;
 use crate::grammar_util::*;
 use crate::lexer::*;
 
@@ -120,9 +121,9 @@ ExprF: BoxExpr<'input> = {
     Text => bx(TextLit(<>)),
     Label => bx(Var(core::V(<>, 0))), // FIXME support var@n syntax
     Const => bx(Const(<>)),
-    List => bx(BuiltinType(List)),
-    Optional => bx(BuiltinType(Optional)),
-    Builtin => bx(builtin_expr(<>)),
+    List => bx(Builtin(List)),
+    Optional => bx(Builtin(Optional)),
+    Builtin => bx(Builtin(<>)),
     Bool => bx(BoolLit(<>)),
     Record,
     RecordLit,
diff --git a/dhall/src/grammar_util.rs b/dhall/src/grammar_util.rs
index c546a13..2250acd 100644
--- a/dhall/src/grammar_util.rs
+++ b/dhall/src/grammar_util.rs
@@ -1,14 +1,7 @@
 use crate::core::{Expr, X};
-use crate::lexer::Builtin;
 
 pub type ParsedExpr<'i> = Expr<'i, X, X>; // FIXME Parse paths and replace the second X with Path
 pub type BoxExpr<'i> = Box<ParsedExpr<'i>>;
 pub type ExprOpFn<'i> = fn(BoxExpr<'i>, BoxExpr<'i>) -> ParsedExpr<'i>;
 pub type ExprListFn<'i> = fn(BoxExpr<'i>, Vec<ParsedExpr<'i>>) -> ParsedExpr<'i>;
 
-pub fn builtin_expr<'i, S, A>(b: Builtin) -> Expr<'i, S, A> {
-    match b {
-        Builtin::Type(t)  => Expr::BuiltinType(t),
-        Builtin::Value(v) => Expr::BuiltinValue(v),
-    }
-}
diff --git a/dhall/src/lexer.rs b/dhall/src/lexer.rs
index 5b4dcaa..b5cbe6b 100644
--- a/dhall/src/lexer.rs
+++ b/dhall/src/lexer.rs
@@ -1,10 +1,8 @@
 use nom::*;
 
 use crate::core::Const;
-use crate::core::BuiltinType;
-use crate::core::BuiltinType::*;
-use crate::core::BuiltinValue;
-use crate::core::BuiltinValue::*;
+use crate::core::Builtin;
+use crate::core::Builtin::*;
 
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum Keyword {
@@ -22,12 +20,6 @@ pub enum ListLike {
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Builtin {
-    Type(BuiltinType),
-    Value(BuiltinValue),
-}
-
-#[derive(Debug, Clone, PartialEq, Eq)]
 pub enum Tok<'i> {
     Identifier(&'i str),
     Keyword(Keyword),
@@ -209,25 +201,25 @@ named!(list_like<&str, ListLike>, alt!(
 ));
 
 named!(builtin<&str, Builtin>, alt!(
-    value!(Builtin::Value(NaturalFold), ident_tag!("Natural/fold")) |
-    value!(Builtin::Value(NaturalBuild), ident_tag!("Natural/build")) |
-    value!(Builtin::Value(NaturalIsZero), ident_tag!("Natural/isZero")) |
-    value!(Builtin::Value(NaturalEven), ident_tag!("Natural/even")) |
-    value!(Builtin::Value(NaturalOdd), ident_tag!("Natural/odd")) |
-    value!(Builtin::Value(NaturalShow), ident_tag!("Natural/show")) |
-    value!(Builtin::Type(Natural), ident_tag!("Natural")) |
-    value!(Builtin::Type(Integer), ident_tag!("Integer")) |
-    value!(Builtin::Type(Double), ident_tag!("Double")) |
-    value!(Builtin::Type(Text), ident_tag!("Text")) |
-    value!(Builtin::Value(ListBuild), ident_tag!("List/build")) |
-    value!(Builtin::Value(ListFold), ident_tag!("List/fold")) |
-    value!(Builtin::Value(ListLength), ident_tag!("List/length")) |
-    value!(Builtin::Value(ListHead), ident_tag!("List/head")) |
-    value!(Builtin::Value(ListLast), ident_tag!("List/last")) |
-    value!(Builtin::Value(ListIndexed), ident_tag!("List/indexed")) |
-    value!(Builtin::Value(ListReverse), ident_tag!("List/reverse")) |
-    value!(Builtin::Value(OptionalFold), ident_tag!("Optional/fold")) |
-    value!(Builtin::Type(Bool), ident_tag!("Bool"))
+    value!(NaturalFold, ident_tag!("Natural/fold")) |
+    value!(NaturalBuild, ident_tag!("Natural/build")) |
+    value!(NaturalIsZero, ident_tag!("Natural/isZero")) |
+    value!(NaturalEven, ident_tag!("Natural/even")) |
+    value!(NaturalOdd, ident_tag!("Natural/odd")) |
+    value!(NaturalShow, ident_tag!("Natural/show")) |
+    value!(Natural, ident_tag!("Natural")) |
+    value!(Integer, ident_tag!("Integer")) |
+    value!(Double, ident_tag!("Double")) |
+    value!(Text, ident_tag!("Text")) |
+    value!(ListBuild, ident_tag!("List/build")) |
+    value!(ListFold, ident_tag!("List/fold")) |
+    value!(ListLength, ident_tag!("List/length")) |
+    value!(ListHead, ident_tag!("List/head")) |
+    value!(ListLast, ident_tag!("List/last")) |
+    value!(ListIndexed, ident_tag!("List/indexed")) |
+    value!(ListReverse, ident_tag!("List/reverse")) |
+    value!(OptionalFold, ident_tag!("Optional/fold")) |
+    value!(Bool, ident_tag!("Bool"))
 ));
 
 named!(token<&str, Tok>, alt!(
@@ -360,7 +352,7 @@ fn test_lex() {
                     ParenL,
                     Identifier("b"),
                     Ascription,
-                    Builtin(self::Builtin::Type(crate::core::BuiltinType::Bool)),
+                    Builtin(crate::core::Builtin::Bool),
                     ParenR,
                     Arrow,
                     Identifier("b"),
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 62ff7d2..51ea848 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -7,8 +7,7 @@ use crate::context::Context;
 use crate::core;
 use crate::core::{Expr, V, X, bx, normalize, shift, subst};
 use crate::core::{pi, app};
-use crate::core::BuiltinType::*;
-use crate::core::BuiltinValue::*;
+use crate::core::Builtin::*;
 use crate::core::Const::*;
 use crate::core::Expr::*;
 
@@ -71,7 +70,7 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
             }
             (&App(ref fL, ref aL), &App(ref fR, ref aR)) =>
                 if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false },
-            (&BuiltinType(a), &BuiltinType(b)) => a == b,
+            (&Builtin(a), &Builtin(b)) => a == b,
             (&Record(ref ktsL0), &Record(ref ktsR0)) => {
                 if ktsL0.len() != ktsR0.len() {
                     return false;
@@ -130,7 +129,7 @@ fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
 
 fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
                        e: &Expr<'i, S, X>,
-                       t: core::BuiltinType,
+                       t: core::Builtin,
                        ef: EF,
                        l: &Expr<'i, S, X>,
                        r: &Expr<'i, S, X>)
@@ -140,17 +139,17 @@ fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>,
 {
     let tl = normalize(&type_with(ctx, l)?);
     match tl {
-        BuiltinType(lt) if lt == t => {}
+        Builtin(lt) if lt == t => {}
         _ => return Err(TypeError::new(ctx, e, ef((*l).clone(), tl))),
     }
 
     let tr = normalize(&type_with(ctx, r)?);
     match tr {
-        BuiltinType(rt) if rt == t => {}
+        Builtin(rt) if rt == t => {}
         _ => return Err(TypeError::new(ctx, e, ef((*r).clone(), tr))),
     }
 
-    Ok(BuiltinType(t))
+    Ok(Builtin(t))
 }
 
 /// Type-check an expression and return the expression'i type if type-checking
@@ -265,11 +264,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
                 Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2)))
             }
         }
-        BuiltinType(t) => Ok(match t {
-            List | Optional => pi("_", Const(Type), Const(Type)),
-            Bool | Natural | Integer | Double | Text => Const(Type),
-        }),
-        BoolLit(_) => Ok(BuiltinType(Bool)),
+        BoolLit(_) => Ok(Builtin(Bool)),
         BoolAnd(ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r),
         BoolOr(ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r),
         BoolEQ(ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r),
@@ -277,7 +272,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
         BoolIf(ref x, ref y, ref z) => {
             let tx = normalize(&type_with(ctx, x)?);
             match tx {
-                BuiltinType(Bool) => {}
+                Builtin(Bool) => {}
                 _ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))),
             }
             let ty = normalize(&type_with(ctx, y)?);
@@ -299,26 +294,26 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
             }
             Ok(ty)
         }
-        NaturalLit(_) => Ok(BuiltinType(Natural)),
-        BuiltinValue(NaturalFold) =>
+        NaturalLit(_) => Ok(Builtin(Natural)),
+        Builtin(NaturalFold) =>
             Ok(pi("_", Natural,
                 pi("natural", Const(Type),
                     pi("succ", pi("_", "natural", "natural"),
                         pi("zero", "natural", "natural"))))),
-        BuiltinValue(NaturalBuild) =>
+        Builtin(NaturalBuild) =>
             Ok(pi("_",
                 pi("natural", Const(Type),
                     pi("succ", pi("_", "natural", "natural"),
                         pi("zero", "natural", "natural"))),
                 Natural)),
-        BuiltinValue(NaturalIsZero) |
-        BuiltinValue(NaturalEven) |
-        BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)),
+        Builtin(NaturalIsZero) |
+        Builtin(NaturalEven) |
+        Builtin(NaturalOdd) => Ok(pi("_", Natural, Bool)),
         NaturalPlus(ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r),
         NaturalTimes(ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r),
-        IntegerLit(_) => Ok(BuiltinType(Integer)),
-        DoubleLit(_) => Ok(BuiltinType(Double)),
-        TextLit(_) => Ok(BuiltinType(Text)),
+        IntegerLit(_) => Ok(Builtin(Integer)),
+        DoubleLit(_) => Ok(Builtin(Double)),
+        TextLit(_) => Ok(Builtin(Text)),
         TextAppend(ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r),
         ListLit(ref t, ref xs) => {
             let s = normalize::<_, S, _>(&type_with(ctx, t)?);
@@ -334,33 +329,33 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
                     return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) )
                 }
             }
-            Ok(App(bx(BuiltinType(List)), t.clone()))
+            Ok(App(bx(Builtin(List)), t.clone()))
         }
-        BuiltinValue(ListBuild) =>
+        Builtin(ListBuild) =>
             Ok(pi("a", Const(Type),
                 pi("_",
                     pi("list", Const(Type),
                         pi("cons", pi("_", "a", pi("_", "list", "list")),
                             pi("nil", "list", "list"))),
                     app(List, "a")))),
-        BuiltinValue(ListFold) =>
+        Builtin(ListFold) =>
             Ok(pi("a", Const(Type),
                 pi("_", app(List, "a"),
                     pi("list", Const(Type),
                         pi("cons", pi("_", "a", pi("_", "list", "list")),
                             pi("nil", "list", "list")))))),
-        BuiltinValue(ListLength) =>
+        Builtin(ListLength) =>
             Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))),
-        BuiltinValue(ListHead) |
-        BuiltinValue(ListLast) =>
+        Builtin(ListHead) |
+        Builtin(ListLast) =>
             Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))),
-        BuiltinValue(ListIndexed) => {
+        Builtin(ListIndexed) => {
             let mut m = BTreeMap::new();
-            m.insert("index", BuiltinType(Natural));
+            m.insert("index", Builtin(Natural));
             m.insert("value", Expr::from("a"));
             Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m)))))
         }
-        BuiltinValue(ListReverse) =>
+        Builtin(ListReverse) =>
             Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))),
         OptionalLit(ref t, ref xs) => {
             let s = normalize::<_, S, _>(&type_with(ctx, t)?);
@@ -380,14 +375,18 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>,
                     return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2)));
                 }
             }
-            Ok(App(bx(BuiltinType(Optional)), t.clone()))
+            Ok(App(bx(Builtin(Optional)), t.clone()))
         }
-        BuiltinValue(OptionalFold) =>
+        Builtin(OptionalFold) =>
             Ok(pi("a", Const(Type),
                 pi("_", app(Optional, "a"),
                     pi("optional", Const(Type),
                         pi("just", pi("_", "a", "optional"),
                             pi("nothing", "optional", "optional")))))),
+        Builtin(List) | Builtin(Optional) =>
+            Ok(pi("_", Const(Type), Const(Type))),
+        Builtin(Bool) | Builtin(Natural) | Builtin(Integer) | Builtin(Double) | Builtin(Text) =>
+            Ok(Const(Type)),
         Record(ref kts) => {
             for (k, t) in kts {
                 let s = normalize::<S, S, X>(&type_with(ctx, t)?);