From 9953043a604556018ba2b1446831aae18f7e7c78 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 16 Apr 2019 20:08:41 +0200 Subject: Typecheck union constructor --- dhall/src/typecheck.rs | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 3cc67f2..c41e34c 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -644,13 +644,22 @@ fn type_last_layer( kts.insert(x, t); Ok(RetExpr(UnionType(kts))) } - Field(r, x) => ensure_matches!(r.get_type()?, - RecordType(kts) => match kts.get(&x) { - Some(e) => Ok(RetExpr(e.unroll().absurd_rec())), + Field(r, x) => match r.as_expr().as_ref() { + UnionType(kts) => match kts.get(&x) { + // Constructor has type T -> < x: T, ... > + Some(t) => { + Ok(RetExpr(Pi(x.clone(), t.clone(), r.normalize().embed()))) + } None => Err(mkerr(MissingField(x, r))), }, - mkerr(NotARecord(x, r)) - ), + _ => match r.get_type()?.unroll_ref()?.as_ref() { + RecordType(kts) => match kts.get(&x) { + Some(t) => Ok(RetExpr(t.unroll().absurd_rec())), + None => Err(mkerr(MissingField(x, r))), + }, + _ => Err(mkerr(NotARecord(x, r))), + }, + }, Const(c) => Ok(RetType(type_of_const(c))), Builtin(b) => Ok(RetExpr(type_of_builtin(b))), BoolLit(_) => Ok(RetType(simple_type_from_builtin(Bool))), @@ -1096,7 +1105,7 @@ mod spec_tests { ti_success!(ti_success_unit_True, "unit/True"); ti_success!(ti_success_unit_Type, "unit/Type"); ti_success!(ti_success_unit_TypeAnnotation, "unit/TypeAnnotation"); - // ti_success!(ti_success_unit_UnionConstructorField, "unit/UnionConstructorField"); + ti_success!(ti_success_unit_UnionConstructorField, "unit/UnionConstructorField"); ti_success!(ti_success_unit_UnionOne, "unit/UnionOne"); ti_success!(ti_success_unit_UnionTypeEmpty, "unit/UnionTypeEmpty"); ti_success!(ti_success_unit_UnionTypeKind, "unit/UnionTypeKind"); -- cgit v1.2.3