diff options
Diffstat (limited to 'dhall')
4 files changed, 6 insertions, 97 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 22ba72d..5422e6d 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -269,7 +269,7 @@ fn type_one_layer( let arg_nf = arg.normalize_nf(env.as_nzenv()); closure.apply(arg_nf) } - _ => return mkerr(format!("apply to not Pi: {:?}", tf_borrow)), + _ => return mkerr(format!("apply to not Pi")), } } ExprKind::BoolIf(x, y, z) => { @@ -447,12 +447,7 @@ fn type_one_layer( match &*handler_type_borrow { ValueKind::PiClosure { closure, annot, .. } => { if variant_type != annot { - // return mkerr("MergeHandlerTypeMismatch"); - return mkerr(format!( - "MergeHandlerTypeMismatch: {:#?} != {:#?}", - variant_type, - annot - )); + return mkerr("MergeHandlerTypeMismatch"); } let v = NzVar::fresh(); @@ -470,11 +465,7 @@ fn type_one_layer( None => inferred_type = Some(handler_return_type), Some(t) => { if t != &handler_return_type { - // return mkerr("MergeHandlerTypeMismatch"); - return mkerr(format!( - "MergeHandlerTypeMismatch: {:#?} != {:#?}", - t, handler_return_type, - )); + return mkerr("MergeHandlerTypeMismatch"); } } } diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index 13b0819..a72e120 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1 @@ -Type error: Unhandled error: apply to not Pi: AppliedBuiltin(Bool, [], [], NzEnv { items: [] }) +Type error: Unhandled error: apply to not Pi diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index 77fed39..8b729a4 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1,21 +1 @@ -Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF { - value: AppliedBuiltin( - Natural, - [], - [], - NzEnv { - items: [], - }, - ), - type: Type, -} != Value@WHNF { - value: AppliedBuiltin( - Bool, - [], - [], - NzEnv { - items: [], - }, - ), - type: Type, -} +Type error: Unhandled error: MergeHandlerTypeMismatch diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt index 6b3f8dc..8b729a4 100644 --- a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt @@ -1,63 +1 @@ -Type error: Unhandled error: MergeHandlerTypeMismatch: Value@WHNF { - value: AppliedBuiltin( - Bool, - [], - [], - NzEnv { - items: [ - Replaced( - Value@Unevaled { - value: Var( - Fresh( - 119, - ), - ), - type: Value@WHNF { - value: AppliedBuiltin( - Bool, - [], - [], - NzEnv { - items: [], - }, - ), - type: Type, - }, - }, - ), - ], - }, - ), - type: Type, -} != Value@WHNF { - value: AppliedBuiltin( - Natural, - [], - [], - NzEnv { - items: [ - Replaced( - Value@Unevaled { - value: Var( - Fresh( - 120, - ), - ), - type: Value@WHNF { - value: AppliedBuiltin( - Natural, - [], - [], - NzEnv { - items: [], - }, - ), - type: Type, - }, - }, - ), - ], - }, - ), - type: Type, -} +Type error: Unhandled error: MergeHandlerTypeMismatch |