Skip to content

Commit dd92735

Browse files
authored
α-normalize after β-normalization for integrity check (#554)
The reason you want to α-normalize last is because β-normalization can introduce new bound variables when normalizing a `constructors` expression
1 parent 54d34ec commit dd92735

File tree

4 files changed

+15
-3
lines changed

4 files changed

+15
-3
lines changed

src/Dhall/Import.hs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -488,9 +488,11 @@ exprFromImport import_@(Import {..}) = do
488488

489489
Right _ -> do
490490
let normalizedExpression =
491-
Dhall.Core.normalizeWith
492-
(getReifiedNormalizer _normalizer)
493-
(Dhall.Core.alphaNormalize resolvedExpression)
491+
Dhall.Core.alphaNormalize
492+
(Dhall.Core.normalizeWith
493+
(getReifiedNormalizer _normalizer)
494+
resolvedExpression
495+
)
494496

495497
let bytes =
496498
encodeExpression _protocolVersion normalizedExpression

tests/Import.hs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,10 @@ importTests =
5151
"a semantic integrity check if fields are reordered"
5252
"./tests/import/"
5353
"./tests/import/fieldOrderC.dhall"
54+
, shouldNotFailRelative
55+
"a semantic integrity check when importing an expression using `constructors`"
56+
"./tests/import/"
57+
"./tests/import/issue553B.dhall"
5458
]
5559
]
5660

tests/import/issue553A.dhall

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
let T = < A : {} | B : {} >
2+
3+
in let t = constructors T
4+
5+
in t

tests/import/issue553B.dhall

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
./issue553A.dhall sha256:2324a5352105b6835db60b127c7096c5d5b81027969ccd368d163edc5d9692e0

0 commit comments

Comments
 (0)