Bug in type inference.

Fixes a bug in lazy constraint expansion. When performing type inference for a field access expression (`x.f`), we generate a lazy constraint with an branch per each struct type that has a field named `n`. We expand the constraint as soon as we know the name of the struct, at which point we can prune all incorrect options. However, the code incorrectly assumed that the field type is also fully concretized at this point, which is generally not true, as type arguments may still be unknown types. The fix doesn't attempt to concretize the field completely, but instead simply substitutes what we know about type arguments at this point. Fixes vmware#1022. Signed-off-by: Leonid Ryzhyk <[email protected]>
ddlog-dev2 · Jul 21, 2021 · 90ad7c4 · 90ad7c4
1 parent 709e769
commit 90ad7c4
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -4,6 +4,12 @@ All notable changes to this project will be documented in this file.
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
+## [Unreleased]
+
+- Bug fixes
+  - Fixed a bug in type inference: #1022.
+
+
 ## [0.42.1] - Jul 16, 2021
 
 - New library functions:

diff --git a/src/Language/DifferentialDatalog/TypeInference.hs b/src/Language/DifferentialDatalog/TypeInference.hs
@@ -735,11 +735,13 @@ exprConstraints_ de@(DDExpr ctx (E e@EField{..})) = do
     let expand t' = case teDeref t' of
                          -- Type has not been sufficiently expanded yet.
                          TETVar{} -> return Nothing
-                         te@(TEUser n _) | elem n (map name candidates) -> do
-                            let t'' = fromJust $ tdefType $ getType ?d n
+                         TEUser n targs | elem n (map name candidates) -> do
+                            let tdef = getType ?d n
+                            let t'' = fromJust $ tdefType tdef
+                            let tmap = M.fromList $ zip (tdefArgs tdef) targs
                             let guarded = structFieldGuarded t'' exprField
                             check ?d (not guarded) (pos e) $ "Access to guarded field \'" ++ exprField ++ "\' (not all constructors of type '" ++ n ++ "' have this field)."
-                            let fld_type = typeToTExpr $ typ $ fromJust $ find ((==exprField) . name) $ structFields $ typ' ?d $ teToType te
+                            let fld_type = teSubstTypeArgs tmap $ typeToTExpr $ typ $ fromJust $ structLookupField t'' exprField
                             return $ Just [dv ==== fld_type]
                          _ -> err ?d (pos estruct)
                                   $ "expression '" ++ show estruct ++ "' must have a field named '" ++ exprField ++ "', but its type '" ++ show t' ++ "' doesn't"