Match query type variables against concrete types (#488)

A type search for `a -> HTMLElement` previously returned no concrete
results where `_ -> HTMLElement` matched functions like
`HTMLAnchorElement -> HTMLElement`, because compareTypes had no case for
a query-side type variable against a concrete type (#395).

Query variables now match any concrete type, as wildcards do, except
that each instantiation charges a penalty of 1 - less than a single
unit of structural mismatch (10) - so results that unify with the query
directly still rank first. Each instantiation is also recorded against
the variable's name and fed through typeVarPenalty, so repeated query
variables must be instantiated consistently: for the query `a -> a`,
`Int -> Int` ranks above `Int -> String`.

Existing comparisons are unaffected: no previously-matching clause
changed, so current rankings only gain new, lower-ranked results.

Also fixes the compareTypes doc examples, which had a typo (parseType
s2 twice) and a stale expected score predating the 10x score scaling.

Based on #396 by @klntsky.

Author: thomashoneyman

CHANGELOG.md

@@ -5,6 +5,13 @@ the most up-to-date version of this file.
 
 ## Unreleased
 
+- Type search queries containing type variables now also match more concrete
+  types: `a -> HTMLElement` finds `HTMLAnchorElement -> HTMLElement` the same
+  way `_ -> HTMLElement` does (#395). Unlike a wildcard, instantiating a query
+  variable charges a small penalty, so results that unify with the query
+  directly rank first, and repeated variables must be instantiated
+  consistently (`a -> a` ranks `Int -> Int` above `Int -> String`). Based on
+  #396 by @klntsky. (@thomashoneyman)
 - The package and module badges on search results are now links to the
   package page and module docs page (#424, @joprice). Builtin modules such
   as Prim have no package page, so their package badge remains plain text.

src/SearchIndex.hs

@@ -403,26 +403,37 @@ tryStripPrefix pre s = fromMaybe s (T.stripPrefix pre s)
 -- The first argument is the query, and the second is the candidate result.
 -- This function is not symmetric; for example:
 --
--- let compare s1 s2 = compareTypes <$> parseType s2 <*> parseType s2
+-- let compare s1 s2 = compareTypes <$> parseType s1 <*> parseType s2
 --
 -- >>> compare "a" "Int"
--- Just Nothing
--- >>> compare "Int" "a"
 -- Just (Just 1)
+-- >>> compare "Int" "a"
+-- Just (Just 10)
 --
--- (The idea here being it's ok to show a more general version of the query,
--- but usually not helpful to show a more concrete version of it.)
+-- (The idea here being that a result which is more concrete than the query
+-- is a slightly worse match than one which unifies with the query directly,
+-- but a much better match than one which is more general than the query.)
 --
 compareTypes :: D.Type' -> D.Type' -> Maybe Int
 compareTypes type1 type2 =
   map calculate . runWriterT $ go type1 type2
   where
-  calculate :: (Int, [(Text, Text)]) -> Int
-  calculate (score, vars) = (10 * score) + typeVarPenalty vars
-
-  go :: D.Type' -> D.Type' -> WriterT [(Text, Text)] Maybe Int
-  go (P.TypeVar _ v1) (P.TypeVar _ v2) = tell [(v1, v2)] *> pure 0
+  -- Each instantiation of a query variable with a concrete type costs 1,
+  -- deliberately less than a single unit of structural mismatch (10), so
+  -- that results which unify with the query rank above instantiations of it.
+  calculate :: (Int, ([(Text, Text)], [(Text, Text)])) -> Int
+  calculate (score, (vars, insts)) =
+    (10 * score) + typeVarPenalty (vars ++ insts) + length insts
+
+  go :: D.Type' -> D.Type' -> WriterT ([(Text, Text)], [(Text, Text)]) Maybe Int
+  go (P.TypeVar _ v1) (P.TypeVar _ v2) = tell ([(v1, v2)], []) *> pure 0
   go t (P.TypeVar _ _) = pure (1 + typeComplexity t)
+  -- A type variable in the query matches any concrete type, like a wildcard,
+  -- except that it is charged an instantiation penalty and the pairing is
+  -- recorded, so that repeated query variables are penalised for matching
+  -- inconsistently (the rendered type acts as a result-side variable in
+  -- 'typeVarPenalty').
+  go (P.TypeVar _ v) t = tell ([], [(v, typeToText t)]) *> pure (typeComplexity t)
   go (P.TypeLevelString _ s1) (P.TypeLevelString _ s2) | s1 == s2 = pure 0
   go (P.TypeWildcard _ _) t = pure (typeComplexity t)
   go (P.TypeConstructor _ q1) (P.TypeConstructor _ q2) | compareQual q1 q2 = pure 0
@@ -448,7 +459,7 @@ compareTypes type1 type2 =
   go t1 (P.ParensInType _ t2) = go t1 t2
   go _ _ = lift Nothing
 
-  goRows :: D.Type' -> D.Type' -> WriterT [(Text, Text)] Maybe Int
+  goRows :: D.Type' -> D.Type' -> WriterT ([(Text, Text)], [(Text, Text)]) Maybe Int
   goRows r1 r2 = sum <$>
     sequence [ go t1 t2
              | P.RowListItem _ name t1 <- fst (P.rowToList r1)
@@ -459,7 +470,10 @@ compareTypes type1 type2 =
   -- Calculate a penalty based on the extent to which the type variables match.
   -- Where differences occur, those which make the result more general than the
   -- query are not penalised as harshly as those which make the result less
-  -- general than the query.
+  -- general than the query. The list may pair a query variable with a rendered
+  -- concrete type as well as with a result variable; an inconsistently
+  -- instantiated query variable is penalised in the same way as one matching
+  -- several distinct result variables.
   typeVarPenalty :: [(Text, Text)] -> Int
   typeVarPenalty list =
     penalty list + (3 * penalty (map swap list))

test/SearchSpec.hs

@@ -121,3 +121,27 @@ spec = do
       x <- shouldMatch query cand0
       y <- shouldMatch query cand1
       x `shouldBeLessThan` y
+
+    describe "with query variables against concrete types (#395)" $ do
+      it "matches concrete instantiations of the query" $ do
+        void $ shouldMatch (p "a -> Int") (p "String -> Int")
+
+      it "treats variables like wildcards, with a small penalty" $ do
+        x <- shouldMatch (p "_ -> Int") (p "String -> Int")
+        y <- shouldMatch (p "a -> Int") (p "String -> Int")
+        x `shouldBeLessThan` y
+
+      it "prefers unifying results to concrete instantiations" $ do
+        x <- shouldMatch (p "a -> a") (p "x -> x")
+        y <- shouldMatch (p "a -> a") (p "Int -> Int")
+        x `shouldBeLessThan` y
+
+      it "prefers consistent instantiations to inconsistent ones" $ do
+        x <- shouldMatch (p "a -> a") (p "Int -> Int")
+        y <- shouldMatch (p "a -> a") (p "Int -> String")
+        x `shouldBeLessThan` y
+
+      it "prefers instantiation to generalization" $ do
+        x <- shouldMatch (p "a -> Int") (p "String -> Int")
+        y <- shouldMatch (p "a -> Int") (p "x -> y")
+        x `shouldBeLessThan` y