Conflicts and failed restrictions beneath 'Choice' nodes aren't reported

[lambdageek]

Take a look at https://github.com/evincarofautumn/Ward/blob/minimal-annotations/src/Check/Permissions.hs#L655

      let conflicts = HashSet.filter conflicting $ mconcat sites
      unless (HashSet.null conflicts) $ do
        record True $ Error pos $ Text.concat $
          [ "conflicting information for permissions "
          , Text.pack $ show $ sort $ map presencePermission
            $ HashSet.toList conflicts
          , " in '"
          , name
          , "'"
          ]

this will find all conflicts in sites :: Vector [Site] and report on them. the problem is that sites comes from https://github.com/evincarofautumn/Ward/blob/minimal-annotations/src/Check/Permissions.hs#L587

      do
        sites <- liftIO $ fmap Vector.toList $ Vector.freeze $ nodeSites node
        reportCallSites restrictions (sites, nodeCalls node, name, pos)

And the nodeSites record field in Node only contains one element for each toplevel element of nodeCalls :: CallTree (Function). It does not have any sites for calls beneath conditionals.

Now I don't think this means we won't report those conflicts at all. Rather - I think we'll just report a conflict at the position of the if statement. This is... not great.

The same problem, but worse, will happen with restrictions https://github.com/evincarofautumn/Ward/blob/minimal-annotations/src/Check/Permissions.hs#L667

      for_ (zip [0 :: Int ..] sites) $ \ (index, s) -> do
        let
          position = case index of
            0 -> ["before first call"]
            _ ->
              [ "at "
              , Text.pack $ show $ callTreeIndex (index - 1) callees
              ]
        for_ restrictions $ \ restriction -> do
          unless (evalRestriction s restriction) $ do
            record True $ Error pos $ Text.concat $
              [ "restriction "
              , Text.pack $ show restriction
              , " violated in '"
              , name
              {-
              , "' with permissions '"
              , Text.pack $ show $ HashSet.toList s
              -}
              , "' "
              ]
              <> position

The issue here is worse, I think, because a restriction could be true at a Choice node, but false at a call in one of its branches.

Anyway, I think I can probably make this all go away by recomputing the site info under 'Choice' when reporting. (1. I think we can get the info in one pass no need to iterate again since the 'Call's will have the best info we have gathered. 2. This should be pretty cheap to do - I think the propagation algorithm is fairly inexpensive)

[lambdageek]

I should probably make an example that illustrates this.

[evincarofautumn]

The first problem is more of a UI issue and can be solved by augmenting a conflict (or a presence in general) with a source location.

The second problem is more worrying, and I think the situation you describe (where a restriction is violated by a substatement but not by its parent statement) is not supposed to happen, and should be ruled out by how inference works.

[lambdageek]

Well like I said, I need to build a test case to show the problem(s) first - right now this is just my reading of the code.

I think it's probably worth annotating Conflict PermissionPresences with sets of source locations - anecdotally that sort of thing greatly improves usability of error messages in other inference systems - but I don't think we should rely on it for correctness.

As for evalRestriction - I think you're probably right - anything true at a child of a Choice should be true at the Choice. (we could probably QuickCheck this once the code is a bit more modular).