Skip to content

Commit 0871fcd

Browse files
sjakobimergify[bot]
authored andcommitted
Prevent "Natural/subtract 0" from causing a panic (#1208)
Previously, normalizing `Natural/subtract 0` would result in this error: ⊢ Natural/subtract 0 Error: Compiler bug An ill-typed expression was encountered during normalization. Explanation: This error message means that there is a bug in the Dhall compiler. You didn't do anything wrong, but if you would like to see this problem fixed then you should report the bug at: https://github.com/dhall-lang/dhall-haskell/issues CallStack (from HasCallStack): error, called at src/Dhall/Eval.hs:865:38 in dhall-1.25.0-FCOZ7uxqivz8dkVwuN7aED:Dhall.Eval This updates the dhall-lang submodule to include a new testcase added in dhall-lang/dhall-lang#692.
1 parent 4559a27 commit 0871fcd

File tree

2 files changed

+16
-9
lines changed

2 files changed

+16
-9
lines changed

dhall/src/Dhall/Eval.hs

+15-8
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,7 @@ data HLamInfo a
138138
| NaturalFoldCl (Val a)
139139
| ListFoldCl (Val a)
140140
| OptionalFoldCl (Val a)
141+
| NaturalSubtractZero
141142

142143
pattern VPrim :: (Val a -> Val a) -> Val a
143144
pattern VPrim f = VHLam Prim f
@@ -414,14 +415,19 @@ eval !env t =
414415
n -> VNaturalToInteger n
415416
NaturalShow -> VPrim $ \case VNaturalLit n -> VTextLit (VChunks [] (Data.Text.pack (show n)))
416417
n -> VNaturalShow n
417-
NaturalSubtract -> VPrim $ \x -> VPrim $ \y ->
418-
case (x,y) of
419-
(VNaturalLit x, VNaturalLit y)
420-
| y >= x -> VNaturalLit (subtract x y)
421-
| otherwise -> VNaturalLit 0
422-
(VNaturalLit 0, y) -> y
423-
(x, VNaturalLit 0) -> VNaturalLit 0
424-
(x, y) -> VNaturalSubtract x y
418+
NaturalSubtract -> VPrim $ \case
419+
VNaturalLit 0 ->
420+
VHLam NaturalSubtractZero id
421+
x@(VNaturalLit m) ->
422+
VPrim $ \case
423+
VNaturalLit n
424+
| n >= m -> VNaturalLit (subtract m n)
425+
| otherwise -> VNaturalLit 0
426+
y -> VNaturalSubtract x y
427+
x ->
428+
VPrim $ \case
429+
VNaturalLit 0 -> VNaturalLit 0
430+
y -> VNaturalSubtract x y
425431
NaturalPlus t u -> vNaturalPlus (evalE t) (evalE u)
426432
NaturalTimes t u -> case (evalE t, evalE u) of
427433
(VNaturalLit 1, u ) -> u
@@ -798,6 +804,7 @@ quote !env !t =
798804
NaturalFoldCl{} -> quote env (t VPrimVar)
799805
ListFoldCl{} -> quote env (t VPrimVar)
800806
OptionalFoldCl{} -> quote env (t VPrimVar)
807+
NaturalSubtractZero -> App NaturalSubtract (NaturalLit 0)
801808

802809
VPi a (freshCl -> (x, v, b)) -> Pi x (quoteE a) (quoteBind x (inst b v))
803810
VHPi (fresh -> (x, v)) a b -> Pi x (quoteE a) (quoteBind x (b v))

0 commit comments

Comments
 (0)