File tree 2 files changed +14
-0
lines changed
2 files changed +14
-0
lines changed Original file line number Diff line number Diff line change @@ -1514,6 +1514,13 @@ translateNode astNode = withAstContext astNode $ case astNode of
1514
1514
1515
1515
AST_NFun node " list" _ -> throwError' $ DeprecatedList node
1516
1516
1517
+ -- rs (2023-05-10): Note, we handle the empty list as a special case (see #1182)
1518
+ -- as the element type is otherwise inferred as `Any`.
1519
+ AST_List node [] -> translateType node >>= \ case
1520
+ EType listTy -> case listTy of
1521
+ SList _ -> pure $ Some listTy $ CoreTerm $ Lit []
1522
+ _ -> throwError' $ TypeError node
1523
+
1517
1524
AST_List node elems -> do
1518
1525
elems' <- traverse translateNode elems
1519
1526
Some ty litList <- mkLiteralList elems' ?? TypeError node
Original file line number Diff line number Diff line change @@ -4565,6 +4565,13 @@ spec = describe "analyze" $ do
4565
4565
|]
4566
4566
" Vacuous property encountered!"
4567
4567
4568
+ describe " regression #1182" $ do
4569
+ expectVerified [text |
4570
+ (defun test:[string] (x: [string])
4571
+ @model [(property (= x x))]
4572
+ (let ((default-val:[string] [])) default-val)
4573
+ x)
4574
+ |]
4568
4575
describe " partial bind (regression #1173)" $ do
4569
4576
expectVerified [text |
4570
4577
(defschema ty
You can’t perform that action at this time.
0 commit comments