318 files changed, 32 insertions(+), 324 deletions(-)

M lib/dhall/parser.rb
M test/test_typechecker.rb
D test/typechecker/failure/FunctionApplicationArgumentNotMatch.dhallb
D test/typechecker/failure/FunctionApplicationIsNotFunction.dhallb
D test/typechecker/failure/FunctionArgumentTypeNotAType.dhallb
D test/typechecker/failure/FunctionDependentType.dhallb
D test/typechecker/failure/FunctionDependentType2.dhallb
D test/typechecker/failure/FunctionTypeArgumentTypeNotAType.dhallb
D test/typechecker/failure/FunctionTypeKindSort.dhallb
D test/typechecker/failure/FunctionTypeTypeKind.dhallb
D test/typechecker/failure/FunctionTypeTypeSort.dhallb
D test/typechecker/failure/IfBranchesNotMatch.dhallb
D test/typechecker/failure/IfBranchesNotType.dhallb
D test/typechecker/failure/IfNotBool.dhallb
D test/typechecker/failure/LetWithWrongAnnotation.dhallb
D test/typechecker/failure/ListLiteralEmptyNoAnnotation.dhallb
D test/typechecker/failure/ListLiteralEmptyNotType.dhallb
D test/typechecker/failure/ListLiteralNotType.dhallb
D test/typechecker/failure/ListLiteralTypesNotMatch.dhallb
D test/typechecker/failure/MergeAlternativeHasNoHandler.dhallb
D test/typechecker/failure/MergeAnnotationNotType.dhallb
D test/typechecker/failure/MergeEmptyWithoutAnnotation.dhallb
D test/typechecker/failure/MergeHandlerNotFunction.dhallb
D test/typechecker/failure/MergeHandlerNotInUnion.dhallb
D test/typechecker/failure/MergeHandlerNotMatchAlternativeType.dhallb
D test/typechecker/failure/MergeHandlersWithDifferentType.dhallb
D test/typechecker/failure/MergeLhsNotRecord.dhallb
D test/typechecker/failure/MergeRhsNotUnion.dhallb
D test/typechecker/failure/MergeWithWrongAnnotation.dhallb
D test/typechecker/failure/OperatorAndNotBool.dhallb
D test/typechecker/failure/OperatorEqualNotBool.dhallb
D test/typechecker/failure/OperatorListConcatenateLhsNotList.dhallb
D test/typechecker/failure/OperatorListConcatenateListsNotMatch.dhallb
D test/typechecker/failure/OperatorListConcatenateRhsNotList.dhallb
D test/typechecker/failure/OperatorNotEqualNotBool.dhallb
D test/typechecker/failure/OperatorOrNotBool.dhallb
D test/typechecker/failure/OperatorPlusNotNatural.dhallb
D test/typechecker/failure/OperatorTextConcatenateLhsNotText.dhallb
D test/typechecker/failure/OperatorTextConcatenateRhsNotText.dhallb
D test/typechecker/failure/OperatorTimesNotNatural.dhallb
D test/typechecker/failure/RecordMixedKinds.dhallb
D test/typechecker/failure/RecordMixedKinds2.dhallb
D test/typechecker/failure/RecordMixedKinds3.dhallb
D test/typechecker/failure/RecordProjectionEmpty.dhallb
D test/typechecker/failure/RecordProjectionNotPresent.dhallb
D test/typechecker/failure/RecordProjectionNotRecord.dhallb
D test/typechecker/failure/RecordSelectionEmpty.dhallb
D test/typechecker/failure/RecordSelectionNotPresent.dhallb
D test/typechecker/failure/RecordSelectionNotRecord.dhallb
D test/typechecker/failure/RecordTypeMixedKinds.dhallb
D test/typechecker/failure/RecordTypeMixedKinds2.dhallb
D test/typechecker/failure/RecordTypeMixedKinds3.dhallb
D test/typechecker/failure/RecordTypeValueMember.dhallb
D test/typechecker/failure/RecursiveRecordMergeLhsNotRecord.dhallb
D test/typechecker/failure/RecursiveRecordMergeMixedKinds.dhallb
D test/typechecker/failure/RecursiveRecordMergeOverlapping.dhallb
D test/typechecker/failure/RecursiveRecordMergeRhsNotRecord.dhallb
D test/typechecker/failure/RecursiveRecordTypeMergeLhsNotRecordType.dhallb
D test/typechecker/failure/RecursiveRecordTypeMergeOverlapping.dhallb
D test/typechecker/failure/RecursiveRecordTypeMergeRhsNotRecordType.dhallb
D test/typechecker/failure/RightBiasedRecordMergeLhsNotRecord.dhallb
D test/typechecker/failure/RightBiasedRecordMergeMixedKinds.dhallb
D test/typechecker/failure/RightBiasedRecordMergeMixedKinds2.dhallb
D test/typechecker/failure/RightBiasedRecordMergeMixedKinds3.dhallb
D test/typechecker/failure/RightBiasedRecordMergeRhsNotRecord.dhallb
D test/typechecker/failure/SomeNotType.dhallb
D test/typechecker/failure/Sort.dhallb
D test/typechecker/failure/TextLiteralInterpolateNotText.dhallb
D test/typechecker/failure/TypeAnnotationWrong.dhallb
D test/typechecker/failure/UnionConstructorFieldNotPresent.dhallb
D test/typechecker/failure/UnionTypeMixedKinds.dhallb
D test/typechecker/failure/UnionTypeMixedKinds2.dhallb
D test/typechecker/failure/UnionTypeMixedKinds3.dhallb
D test/typechecker/failure/UnionTypeNotType.dhallb
D test/typechecker/failure/VariableFree.dhallb
D test/typechecker/gen
D test/typechecker/success/BoolA.dhallb
D test/typechecker/success/BoolB.dhallb
D test/typechecker/success/DoubleA.dhallb
D test/typechecker/success/DoubleB.dhallb
D test/typechecker/success/DoubleLiteralA.dhallb
D test/typechecker/success/DoubleLiteralB.dhallb
D test/typechecker/success/DoubleShowA.dhallb
D test/typechecker/success/DoubleShowB.dhallb
D test/typechecker/success/FalseA.dhallb
D test/typechecker/success/FalseB.dhallb
D test/typechecker/success/FunctionA.dhallb
D test/typechecker/success/FunctionApplicationA.dhallb
D test/typechecker/success/FunctionApplicationB.dhallb
D test/typechecker/success/FunctionB.dhallb
D test/typechecker/success/FunctionNamedArgA.dhallb
D test/typechecker/success/FunctionNamedArgB.dhallb
D test/typechecker/success/FunctionTypeKindKindA.dhallb
D test/typechecker/success/FunctionTypeKindKindB.dhallb
D test/typechecker/success/FunctionTypeKindTermA.dhallb
D test/typechecker/success/FunctionTypeKindTermB.dhallb
D test/typechecker/success/FunctionTypeKindTypeA.dhallb
D test/typechecker/success/FunctionTypeKindTypeB.dhallb
D test/typechecker/success/FunctionTypeTermTermA.dhallb
D test/typechecker/success/FunctionTypeTermTermB.dhallb
D test/typechecker/success/FunctionTypeTypeTermA.dhallb
D test/typechecker/success/FunctionTypeTypeTermB.dhallb
D test/typechecker/success/FunctionTypeTypeTypeA.dhallb
D test/typechecker/success/FunctionTypeTypeTypeB.dhallb
D test/typechecker/success/FunctionTypeUsingArgumentA.dhallb
D test/typechecker/success/FunctionTypeUsingArgumentB.dhallb
D test/typechecker/success/IfA.dhallb
D test/typechecker/success/IfB.dhallb
D test/typechecker/success/IfNormalizeArgumentsA.dhallb
D test/typechecker/success/IfNormalizeArgumentsB.dhallb
D test/typechecker/success/IntegerA.dhallb
D test/typechecker/success/IntegerB.dhallb
D test/typechecker/success/IntegerLiteralA.dhallb
D test/typechecker/success/IntegerLiteralB.dhallb
D test/typechecker/success/IntegerShowA.dhallb
D test/typechecker/success/IntegerShowB.dhallb
D test/typechecker/success/IntegerToDoubleA.dhallb
D test/typechecker/success/IntegerToDoubleB.dhallb
D test/typechecker/success/KindA.dhallb
D test/typechecker/success/KindB.dhallb
D test/typechecker/success/LetA.dhallb
D test/typechecker/success/LetB.dhallb
D test/typechecker/success/LetNestedTypeSynonymA.dhallb
D test/typechecker/success/LetNestedTypeSynonymB.dhallb
D test/typechecker/success/LetTypeSynonymA.dhallb
D test/typechecker/success/LetTypeSynonymB.dhallb
D test/typechecker/success/LetWithAnnotationA.dhallb
D test/typechecker/success/LetWithAnnotationB.dhallb
D test/typechecker/success/ListA.dhallb
D test/typechecker/success/ListB.dhallb
D test/typechecker/success/ListBuildA.dhallb
D test/typechecker/success/ListBuildB.dhallb
D test/typechecker/success/ListFoldA.dhallb
D test/typechecker/success/ListFoldB.dhallb
D test/typechecker/success/ListHeadA.dhallb
D test/typechecker/success/ListHeadB.dhallb
D test/typechecker/success/ListIndexedA.dhallb
D test/typechecker/success/ListIndexedB.dhallb
D test/typechecker/success/ListLastA.dhallb
D test/typechecker/success/ListLastB.dhallb
D test/typechecker/success/ListLengthA.dhallb
D test/typechecker/success/ListLengthB.dhallb
D test/typechecker/success/ListLiteralEmptyA.dhallb
D test/typechecker/success/ListLiteralEmptyB.dhallb
D test/typechecker/success/ListLiteralNormalizeArgumentsA.dhallb
D test/typechecker/success/ListLiteralNormalizeArgumentsB.dhallb
D test/typechecker/success/ListLiteralOneA.dhallb
D test/typechecker/success/ListLiteralOneB.dhallb
D test/typechecker/success/ListReverseA.dhallb
D test/typechecker/success/ListReverseB.dhallb
D test/typechecker/success/MergeEmptyUnionA.dhallb
D test/typechecker/success/MergeEmptyUnionB.dhallb
D test/typechecker/success/MergeOneA.dhallb
D test/typechecker/success/MergeOneB.dhallb
D test/typechecker/success/MergeOneWithAnnotationA.dhallb
D test/typechecker/success/MergeOneWithAnnotationB.dhallb
D test/typechecker/success/NaturalA.dhallb
D test/typechecker/success/NaturalB.dhallb
D test/typechecker/success/NaturalBuildA.dhallb
D test/typechecker/success/NaturalBuildB.dhallb
D test/typechecker/success/NaturalEvenA.dhallb
D test/typechecker/success/NaturalEvenB.dhallb
D test/typechecker/success/NaturalFoldA.dhallb
D test/typechecker/success/NaturalFoldB.dhallb
D test/typechecker/success/NaturalIsZeroA.dhallb
D test/typechecker/success/NaturalIsZeroB.dhallb
D test/typechecker/success/NaturalLiteralA.dhallb
D test/typechecker/success/NaturalLiteralB.dhallb
D test/typechecker/success/NaturalOddA.dhallb
D test/typechecker/success/NaturalOddB.dhallb
D test/typechecker/success/NaturalShowA.dhallb
D test/typechecker/success/NaturalShowB.dhallb
D test/typechecker/success/NaturalToIntegerA.dhallb
D test/typechecker/success/NaturalToIntegerB.dhallb
D test/typechecker/success/NoneA.dhallb
D test/typechecker/success/NoneB.dhallb
D test/typechecker/success/OldOptionalNoneA.dhallb
D test/typechecker/success/OldOptionalNoneB.dhallb
D test/typechecker/success/OldOptionalTrueA.dhallb
D test/typechecker/success/OldOptionalTrueB.dhallb
D test/typechecker/success/OperatorAndA.dhallb
D test/typechecker/success/OperatorAndB.dhallb
D test/typechecker/success/OperatorAndNormalizeArgumentsA.dhallb
D test/typechecker/success/OperatorAndNormalizeArgumentsB.dhallb
D test/typechecker/success/OperatorEqualA.dhallb
D test/typechecker/success/OperatorEqualB.dhallb
D test/typechecker/success/OperatorEqualNormalizeArgumentsA.dhallb
D test/typechecker/success/OperatorEqualNormalizeArgumentsB.dhallb
D test/typechecker/success/OperatorListConcatenateA.dhallb
D test/typechecker/success/OperatorListConcatenateB.dhallb
D test/typechecker/success/OperatorListConcatenateNormalizeArgumentsA.dhallb
D test/typechecker/success/OperatorListConcatenateNormalizeArgumentsB.dhallb
D test/typechecker/success/OperatorNotEqualA.dhallb
D test/typechecker/success/OperatorNotEqualB.dhallb
D test/typechecker/success/OperatorNotEqualNormalizeArgumentsA.dhallb
D test/typechecker/success/OperatorNotEqualNormalizeArgumentsB.dhallb
D test/typechecker/success/OperatorOrA.dhallb
D test/typechecker/success/OperatorOrB.dhallb
D test/typechecker/success/OperatorOrNormalizeArgumentsA.dhallb
D test/typechecker/success/OperatorOrNormalizeArgumentsB.dhallb
D test/typechecker/success/OperatorPlusA.dhallb
D test/typechecker/success/OperatorPlusB.dhallb
D test/typechecker/success/OperatorPlusNormalizeArgumentsA.dhallb
D test/typechecker/success/OperatorPlusNormalizeArgumentsB.dhallb
D test/typechecker/success/OperatorTextConcatenateA.dhallb
D test/typechecker/success/OperatorTextConcatenateB.dhallb
D test/typechecker/success/OperatorTextConcatenateNormalizeArgumentsA.dhallb
D test/typechecker/success/OperatorTextConcatenateNormalizeArgumentsB.dhallb
D test/typechecker/success/OperatorTimesA.dhallb
D test/typechecker/success/OperatorTimesB.dhallb
D test/typechecker/success/OperatorTimesNormalizeArgumentsA.dhallb
D test/typechecker/success/OperatorTimesNormalizeArgumentsB.dhallb
D test/typechecker/success/OptionalA.dhallb
D test/typechecker/success/OptionalB.dhallb
D test/typechecker/success/OptionalBuildA.dhallb
D test/typechecker/success/OptionalBuildB.dhallb
D test/typechecker/success/OptionalFoldA.dhallb
D test/typechecker/success/OptionalFoldB.dhallb
D test/typechecker/success/RecordEmptyA.dhallb
D test/typechecker/success/RecordEmptyB.dhallb
D test/typechecker/success/RecordOneKindA.dhallb
D test/typechecker/success/RecordOneKindB.dhallb
D test/typechecker/success/RecordOneTypeA.dhallb
D test/typechecker/success/RecordOneTypeB.dhallb
D test/typechecker/success/RecordOneValueA.dhallb
D test/typechecker/success/RecordOneValueB.dhallb
D test/typechecker/success/RecordProjectionEmptyA.dhallb
D test/typechecker/success/RecordProjectionEmptyB.dhallb
D test/typechecker/success/RecordProjectionKindA.dhallb
D test/typechecker/success/RecordProjectionKindB.dhallb
D test/typechecker/success/RecordProjectionTypeA.dhallb
D test/typechecker/success/RecordProjectionTypeB.dhallb
D test/typechecker/success/RecordProjectionValueA.dhallb
D test/typechecker/success/RecordProjectionValueB.dhallb
D test/typechecker/success/RecordSelectionKindA.dhallb
D test/typechecker/success/RecordSelectionKindB.dhallb
D test/typechecker/success/RecordSelectionTypeA.dhallb
D test/typechecker/success/RecordSelectionTypeB.dhallb
D test/typechecker/success/RecordSelectionValueA.dhallb
D test/typechecker/success/RecordSelectionValueB.dhallb
D test/typechecker/success/RecordTypeA.dhallb
D test/typechecker/success/RecordTypeB.dhallb
D test/typechecker/success/RecordTypeEmptyA.dhallb
D test/typechecker/success/RecordTypeEmptyB.dhallb
D test/typechecker/success/RecordTypeKindA.dhallb
D test/typechecker/success/RecordTypeKindB.dhallb
D test/typechecker/success/RecordTypeTypeA.dhallb
D test/typechecker/success/RecordTypeTypeB.dhallb
D test/typechecker/success/RecursiveRecordMergeLhsEmptyA.dhallb
D test/typechecker/success/RecursiveRecordMergeLhsEmptyB.dhallb
D test/typechecker/success/RecursiveRecordMergeRecursivelyA.dhallb
D test/typechecker/success/RecursiveRecordMergeRecursivelyB.dhallb
D test/typechecker/success/RecursiveRecordMergeRecursivelyKindsA.dhallb
D test/typechecker/success/RecursiveRecordMergeRecursivelyKindsB.dhallb
D test/typechecker/success/RecursiveRecordMergeRecursivelyTypesA.dhallb
D test/typechecker/success/RecursiveRecordMergeRecursivelyTypesB.dhallb
D test/typechecker/success/RecursiveRecordMergeRhsEmptyA.dhallb
D test/typechecker/success/RecursiveRecordMergeRhsEmptyB.dhallb
D test/typechecker/success/RecursiveRecordMergeTwoA.dhallb
D test/typechecker/success/RecursiveRecordMergeTwoB.dhallb
D test/typechecker/success/RecursiveRecordMergeTwoKindsA.dhallb
D test/typechecker/success/RecursiveRecordMergeTwoKindsB.dhallb
D test/typechecker/success/RecursiveRecordMergeTwoTypesA.dhallb
D test/typechecker/success/RecursiveRecordMergeTwoTypesB.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeRecursivelyA.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeRecursivelyB.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsA.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeRecursivelyKindsB.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesA.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeRecursivelyTypesB.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyA.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeRhsEmptyB.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeTwoA.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeTwoB.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeTwoKindsA.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeTwoKindsB.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeTwoTypesA.dhallb
D test/typechecker/success/RecursiveRecordTypeMergeTwoTypesB.dhallb
D test/typechecker/success/RightBiasedRecordMergeRhsEmptyA.dhallb
D test/typechecker/success/RightBiasedRecordMergeRhsEmptyB.dhallb
D test/typechecker/success/RightBiasedRecordMergeTwoA.dhallb
D test/typechecker/success/RightBiasedRecordMergeTwoB.dhallb
D test/typechecker/success/RightBiasedRecordMergeTwoDifferentA.dhallb
D test/typechecker/success/RightBiasedRecordMergeTwoDifferentB.dhallb
D test/typechecker/success/RightBiasedRecordMergeTwoKindsA.dhallb
D test/typechecker/success/RightBiasedRecordMergeTwoKindsB.dhallb
D test/typechecker/success/RightBiasedRecordMergeTwoTypesA.dhallb
D test/typechecker/success/RightBiasedRecordMergeTwoTypesB.dhallb
D test/typechecker/success/SomeTrueA.dhallb
D test/typechecker/success/SomeTrueB.dhallb
D test/typechecker/success/TextA.dhallb
D test/typechecker/success/TextB.dhallb
D test/typechecker/success/TextLiteralA.dhallb
D test/typechecker/success/TextLiteralB.dhallb
D test/typechecker/success/TextLiteralNormalizeArgumentsA.dhallb
D test/typechecker/success/TextLiteralNormalizeArgumentsB.dhallb
D test/typechecker/success/TextLiteralWithInterpolationA.dhallb
D test/typechecker/success/TextLiteralWithInterpolationB.dhallb
D test/typechecker/success/TextShowA.dhallb
D test/typechecker/success/TextShowB.dhallb
D test/typechecker/success/TrueA.dhallb
D test/typechecker/success/TrueB.dhallb
D test/typechecker/success/TypeA.dhallb
D test/typechecker/success/TypeAnnotationA.dhallb
D test/typechecker/success/TypeAnnotationB.dhallb
D test/typechecker/success/TypeB.dhallb
D test/typechecker/success/UnionConstructorFieldA.dhallb
D test/typechecker/success/UnionConstructorFieldB.dhallb
D test/typechecker/success/UnionOneA.dhallb
D test/typechecker/success/UnionOneB.dhallb
D test/typechecker/success/UnionTypeEmptyA.dhallb
D test/typechecker/success/UnionTypeEmptyB.dhallb
D test/typechecker/success/UnionTypeKindA.dhallb
D test/typechecker/success/UnionTypeKindB.dhallb
D test/typechecker/success/UnionTypeOneA.dhallb
D test/typechecker/success/UnionTypeOneB.dhallb
D test/typechecker/success/UnionTypeTypeA.dhallb
D test/typechecker/success/UnionTypeTypeB.dhallb

@@ 120,13 120,13 @@ module Dhall
 		module SelectorExpression
 			def value
 				record = capture(:primitive_expression).value
-				selectors = captures(:selector).map(&:value).map(&method(:Array))
+				selectors = captures(:selector).map(&:value)
 				selectors.reduce(record) do |rec, sels|
-					if sels.length == 1
-						RecordSelection.new(record: rec, selector: sels.first)
-					else
+					if sels.is_a?(Array)
 						return EmptyRecordProjection.new(record: rec) if sels.empty?
 						RecordProjection.new(record: rec, selectors: sels)
+					else
+						RecordSelection.new(record: rec, selector: sels)
 					end
 				end
 			end


@@ 394,9 394,10 @@ module Dhall
 			def value(first_key)
 				Record.new(
 					record: captures(:record_literal_entry).map(&:value).reduce(
-						{ first_key => capture(:expression).value },
-						&:merge
-					)
+						first_key => capture(:expression).value
+					) do |final, rec|
+						final.merge(rec) { raise TypeError, "duplicate field" }
+					end
 				)
 			end
 		end

@@ 4,22 4,22 @@ require "minitest/autorun"
 require "pathname"
 
 require "dhall/typecheck"
-require "dhall/binary"
+require "dhall/parser"
 
 class TestTypechecker < Minitest::Test
 	DIRPATH = Pathname.new(File.dirname(__FILE__))
-	TESTS = DIRPATH + "typechecker/"
+	TESTS = DIRPATH + "../dhall-lang/tests/typecheck/"
 
-	Pathname.glob(TESTS + "success/**/*A.dhallb").each do |path|
-		test = path.relative_path_from(TESTS).to_s.sub(/A\.dhallb$/, "")
+	Pathname.glob(TESTS + "success/**/*A.dhall").each do |path|
+		test = path.relative_path_from(TESTS).to_s.sub(/A\.dhall$/, "")
 		next if test =~ /prelude/
 
 		define_method("test_#{test}") do
 			assert_respond_to(
 				Dhall::TypeChecker.for(
 					Dhall::TypeAnnotation.new(
-						value: Dhall.from_binary(path.binread),
-						type:  Dhall.from_binary((TESTS + "#{test}B.dhallb").binread)
+						value: Dhall::Parser.parse_file(path).value,
+						type:  Dhall::Parser.parse_file(TESTS + "#{test}B.dhall").value
 					)
 				).annotate(Dhall::TypeChecker::Context.new),
 				:type


@@ 27,19 27,33 @@ class TestTypechecker < Minitest::Test
 		end
 	end
 
-	Pathname.glob(TESTS + "failure/**/*.dhallb").each do |path|
-		test = path.relative_path_from(TESTS).to_s.sub(/.dhallb$/, "")
+	Pathname.glob(TESTS + "failure/**/*.dhall").each do |path|
+		test = path.relative_path_from(TESTS).to_s.sub(/.dhall$/, "")
 
 		define_method("test_#{test}") do
 			assert_raises TypeError do
-				expr = Dhall.from_binary(path.binread)
 				Dhall::TypeChecker.for(
-					expr
+					Dhall::Parser.parse_file(path).value
 				).annotate(Dhall::TypeChecker::Context.new)
 			end
 		end
 	end
 
+	ITESTS = DIRPATH + "../dhall-lang/tests/type-inference/"
+
+	Pathname.glob(ITESTS + "success/**/*A.dhall").each do |path|
+		test = path.relative_path_from(TESTS).to_s.sub(/A\.dhall$/, "")
+
+		define_method("test_#{test}") do
+			assert_equal(
+				Dhall::Parser.parse_file(ITESTS + "#{test}B.dhall").value,
+				Dhall::TypeChecker.for(
+					Dhall::Parser.parse_file(path).value
+				).annotate(Dhall::TypeChecker::Context.new).type
+			)
+		end
+	end
+
 	def forall(var, type)
 		Dhall::Forall.new(var: var, type: type, body: Dhall::Variable["UNKNOWN"])
 	end

@@ 1,1 0,0 @@
-�axdBooldBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�axdBooldType>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dKinddSort>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dTypedKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dTypedSort>
\ No newline at end of file

@@ 1,1 0,0 @@
-����`>
\ No newline at end of file

@@ 1,1 0,0 @@
-��dTypedType>
\ No newline at end of file

@@ 1,1 0,0 @@
-����>
\ No newline at end of file

@@ 1,1 0,0 @@
-�axgNatural��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-����>
\ No newline at end of file

@@ 1,1 0,0 @@
-����ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-�����dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-�����>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax��ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-����>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-�����>
\ No newline at end of file

@@ 1,1 0,0 @@
-�������>
\ No newline at end of file

@@ 1,1 0,0 @@
-�����>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-���`>
\ No newline at end of file

@@ 1,1 0,0 @@
-��`�>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��aydBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdTypeay��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdTypeaydKind>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��ax>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��ay��ax>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-�ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ay��ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	�ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBoolaydType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKindaydType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKindaydBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax�>
\ No newline at end of file

@@ 1,1 0,0 @@
-����>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax���aydBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax���ax�>
\ No newline at end of file

@@ 1,1 0,0 @@
-����>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-dBool��>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��axdBool��axgNatural>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	���>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ax����axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��axdBool��axdKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ax����axdKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	���>
\ No newline at end of file

@@ 1,1 0,0 @@
-��dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dSort>
\ No newline at end of file

@@ 1,1 0,0 @@
-�`�`>
\ No newline at end of file

@@ 1,1 0,0 @@
-��dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��axdBoolay>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBoolaydType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKindaydType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKindaydBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax�>
\ No newline at end of file

@@ 1,1 0,0 @@
-ax>
\ No newline at end of file

@@ 1,10 0,0 @@
-#!/bin/sh
-
-cp -r "$(git root)"/dhall-lang/tests/typecheck/success "$(git root)"/test/typechecker/success/standard
-cp -r "$(git root)"/dhall-lang/tests/typecheck/failure "$(git root)"/test/typechecker/failure/standard
-
-cd "$(git root)"/test/typechecker/success/standard
-find . -name '*.dhall' -exec "$(git root)"/test/normalization/dhall-encode '{}' \;
-
-cd "$(git root)"/test/typechecker/failure/standard
-find . -name '*.dhall' -exec "$(git root)"/test/normalization/dhall-encode '{}' \;

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-fDouble>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-fDouble>
\ No newline at end of file

@@ 1,1 0,0 @@
-kDouble/show>
\ No newline at end of file

@@ 1,1 0,0 @@
-�fDoubledText>
\ No newline at end of file

@@ 1,1 0,0 @@
-�>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dBooldBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�axdBoolax>
\ No newline at end of file

@@ 1,1 0,0 @@
-�axdBooldBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dKinddKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-dSort>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dKinddBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dKinddType>
\ No newline at end of file

@@ 1,1 0,0 @@
-dSort>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dBooldBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dTypedBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dTypedType>
\ No newline at end of file

@@ 1,1 0,0 @@
-dKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-����>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�������������>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-gInteger>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-�>
\ No newline at end of file

@@ 1,1 0,0 @@
-gInteger>
\ No newline at end of file

@@ 1,1 0,0 @@
-lInteger/show>
\ No newline at end of file

@@ 1,1 0,0 @@
-�gIntegerdText>
\ No newline at end of file

@@ 1,1 0,0 @@
-pInteger/toDouble>
\ No newline at end of file

@@ 1,1 0,0 @@
-�gIntegerfDouble>
\ No newline at end of file

@@ 1,1 0,0 @@
-dKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-dSort>
\ No newline at end of file

@@ 1,1 0,0 @@
-�ax��ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�ax�dBoolayax�ay>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�ax�dBool��ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�axdBool�ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dList>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dTypedType>
\ No newline at end of file

@@ 1,1 0,0 @@
-jList/build>
\ No newline at end of file

@@ 1,1 0,0 @@
-iList/fold>
\ No newline at end of file

@@ 1,1 0,0 @@
-iList/head>
\ No newline at end of file

@@ 1,1 0,0 @@
-lList/indexed>
\ No newline at end of file

@@ 1,1 0,0 @@
-iList/last>
\ No newline at end of file

@@ 1,1 0,0 @@
-kList/length>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-������>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-lList/reverse>
\ No newline at end of file

@@ 1,1 0,0 @@
-�ax�����axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�ax��dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-gNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-mNatural/build>
\ No newline at end of file

@@ 1,1 0,0 @@
-��gnaturaldType�dsucc�gnaturalgnatural�dzerognaturalgnaturalgNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-lNatural/even>
\ No newline at end of file

@@ 1,1 0,0 @@
-�gNaturaldBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-lNatural/fold>
\ No newline at end of file

@@ 1,1 0,0 @@
-�gNatural�gnaturaldType�dsucc�gnaturalgnatural�dzerognaturalgnatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-nNatural/isZero>
\ No newline at end of file

@@ 1,1 0,0 @@
-�gNaturaldBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�>
\ No newline at end of file

@@ 1,1 0,0 @@
-gNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-kNatural/odd>
\ No newline at end of file

@@ 1,1 0,0 @@
-�gNaturaldBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-lNatural/show>
\ No newline at end of file

@@ 1,1 0,0 @@
-�gNaturaldText>
\ No newline at end of file

@@ 1,1 0,0 @@
-qNatural/toInteger>
\ No newline at end of file

@@ 1,1 0,0 @@
-�gNaturalgInteger>
\ No newline at end of file

@@ 1,1 0,0 @@
-dNone>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dBool�>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�����>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�����>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�������>
\ No newline at end of file

@@ 1,1 0,0 @@
-����������������>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�����>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-gNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-�������>
\ No newline at end of file

@@ 1,1 0,0 @@
-gNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-��aa�ab>
\ No newline at end of file

@@ 1,1 0,0 @@
-dText>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax�aa��ay�ab>
\ No newline at end of file

@@ 1,1 0,0 @@
-dText>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-gNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-�������>
\ No newline at end of file

@@ 1,1 0,0 @@
-gNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-hOptional>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dTypedType>
\ No newline at end of file

@@ 1,1 0,0 @@
-nOptional/build>
\ No newline at end of file

@@ 1,1 0,0 @@
-mOptional/fold>
\ No newline at end of file

@@ 1,1 0,0 @@
-��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��axdTypeaydTypeax>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKind>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��axdBoolaygNaturalax>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdType>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��ax��ay��ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��axdTypeax>
\ No newline at end of file

@@ 1,1 0,0 @@
-dKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ax��ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ax��ax>
\ No newline at end of file

@@ 1,1 0,0 @@
-��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-dSort>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-dKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-�����ax�>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax��aa���ax��ab�>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��aadBoolabdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax��aadType��ax��abdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��aadKindabdKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax��aadBool��ax��abgNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��aadTypeabdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax���>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-���ax���ay�>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBoolaydBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-���axdType��aydType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKindaydKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-���axdBool��aygNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdTypeaydType>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��ax��aadBool��ay��abdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��ax��aadKind��ay��abdKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-dSort>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��ax��aadType��ay��abdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-dKind>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��axdBool��>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��axdBool��aydBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��axdKind��aydKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-dSort>
\ No newline at end of file

@@ 1,2 0,0 @@
-�
-��axdType��aydType>
\ No newline at end of file

@@ 1,1 0,0 @@
-dKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ax����>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ax����ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��ax����ax�>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��axdType��axdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��axdBool��axgNatural>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-���>
\ No newline at end of file

@@ 1,1 0,0 @@
-dText>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-�aa>
\ No newline at end of file

@@ 1,1 0,0 @@
-dText>
\ No newline at end of file

@@ 1,1 0,0 @@
-�aa���aa�ab`>
\ No newline at end of file

@@ 1,1 0,0 @@
-dText>
\ No newline at end of file

@@ 1,1 0,0 @@
-�aa�ab`>
\ No newline at end of file

@@ 1,1 0,0 @@
-dText>
\ No newline at end of file

@@ 1,1 0,0 @@
-iText/show>
\ No newline at end of file

@@ 1,1 0,0 @@
-�dTextdText>
\ No newline at end of file

@@ 1,1 0,0 @@
-�>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-�	��axdBoolax>
\ No newline at end of file

@@ 1,1 0,0 @@
-�axdBool��axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-�ax��>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-��>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdKind>
\ No newline at end of file

@@ 1,1 0,0 @@
-dSort>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdBool>
\ No newline at end of file

@@ 1,1 0,0 @@
-dType>
\ No newline at end of file

@@ 1,1 0,0 @@
-��axdType>
\ No newline at end of file

@@ 1,1 0,0 @@
-dKind>
\ No newline at end of file