feat: Annotate offered variables which match the required type (#1045)

primer-service/test/Tests/OpenAPI.hs

@@ -344,7 +344,7 @@ instance Arbitrary Available.InputAction where
 instance Arbitrary Available.Action where
   arbitrary = either Available.NoInput Available.Input <$> arbitrary
 instance Arbitrary Available.Option where
-  arbitrary = Available.Option <$> arbitrary <*> arbitrary
+  arbitrary = Available.Option <$> arbitrary <*> arbitrary <*> arbitrary
 instance Arbitrary Available.FreeInput where
   arbitrary = arbitraryBoundedEnum
 instance Arbitrary Available.Options where

primer-service/test/outputs/OpenAPI/openapi.json

@@ -471,12 +471,16 @@
                         "minItems": 1,
                         "type": "array"
                     },
+                    "matchesType": {
+                        "type": "boolean"
+                    },
                     "option": {
                         "type": "string"
                     }
                 },
                 "required": [
-                    "option"
+                    "option",
+                    "matchesType"
                 ],
                 "type": "object"
             },

primer/src/Primer/Action/Available.hs

@@ -31,6 +31,7 @@ import Data.Set qualified as Set
 import Data.Text qualified as T
 import Data.Tuple.Extra (fst3)
 import Optics (
+  afailing,
   to,
   (%),
   (^.),
@@ -103,6 +104,7 @@ import Primer.Typecheck (
   Cxt,
   TypeDefError (TDIHoleType),
   TypeDefInfo (TypeDefInfo),
+  eqType,
   getTypeDefInfo',
   instantiateValCons',
  )
@@ -382,6 +384,7 @@ forTypeDefConsFieldNode l Editable def con index id =
 data Option = Option
   { option :: Text
   , context :: Maybe (NonEmpty Text)
+  , matchesType :: Bool
   }
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON Option
@@ -467,13 +470,13 @@ options typeDefs defs cxt level def0 sel0 = \case
     findNode >>= \case
       ExprNode (Case _ _ brs _) ->
         let exist = mapMaybe ((\case (PatPrim (PrimInt i)) -> Just i; _ -> Nothing) . caseBranchName) brs
-         in pure $ noFree $ (\i -> Option (show i) Nothing) <$> exist
+         in pure $ noFree $ (\i -> Option (show i) Nothing False) <$> exist
       _ -> Nothing
   DeleteBranchChar ->
     findNode >>= \case
       ExprNode (Case _ _ brs _) ->
         let exist = mapMaybe ((\case (PatPrim (PrimChar c)) -> Just c; _ -> Nothing) . caseBranchName) brs
-         in pure $ noFree $ (\c -> Option (T.singleton c) Nothing) <$> exist
+         in pure $ noFree $ (\c -> Option (T.singleton c) Nothing False) <$> exist
       _ -> Nothing
   RenamePattern -> do
     CaseBindNode b <- findNode
@@ -514,17 +517,32 @@ options typeDefs defs cxt level def0 sel0 = \case
   where
     freeVar opts = Options{opts, free = FreeVarName}
     noFree opts = Options{opts, free = FreeNone}
-    localOpt = flip Option Nothing . unName
-    globalOpt n =
+    localOpt = localOpt' False
+    localOpt' matchesType x =
+      Option
+        { option = unName x
+        , context = Nothing
+        , matchesType
+        }
+    globalOpt = globalOpt' False
+    globalOpt' matchesType n =
       Option
         { option = unName $ baseName n
         , context = Just $ map unName $ unModuleName $ qualifiedModule n
+        , matchesType
         }
     varOpts = do
       (_, locals, globals) <- varsInScope
-      pure $
-        (first (localOpt . unLocalName) <$> locals)
-          <> (first globalOpt <$> globals)
+      findNode >>= \case
+        ExprNode e
+          | Just t <- (e ^? _exprMetaLens % _type % _Just % (_chkedAt `afailing` _synthed)) -> do
+              pure $
+                (locals <&> \(ln, t') -> (localOpt' (t `eqType` t') $ unLocalName ln, t'))
+                  <> (globals <&> \(gn, t') -> (globalOpt' (t `eqType` t') gn, t'))
+        _ ->
+          pure $
+            (first (localOpt . unLocalName) <$> locals)
+              <> (first globalOpt <$> globals)
     findNode = case sel0 of
       SelectionDef sel -> do
         nodeSel <- sel.node

primer/src/Primer/Typecheck.hs

@@ -58,6 +58,7 @@ module Primer.Typecheck (
   localTmVars,
   localTyVars,
   enhole,
+  eqType,
 ) where
 
 import Foreword

primer/test/Tests/Action/Available.hs

@@ -325,9 +325,9 @@ tasty_available_actions_accepted = withTests 500 $
               let opts'' =
                     opts' <> case free of
                       Available.FreeNone -> []
-                      Available.FreeVarName -> [(StudentProvided,) . flip Available.Option Nothing <$> (unName <$> genName)]
-                      Available.FreeInt -> [(StudentProvided,) . flip Available.Option Nothing <$> (show <$> genInt)]
-                      Available.FreeChar -> [(StudentProvided,) . flip Available.Option Nothing . T.singleton <$> genChar]
+                      Available.FreeVarName -> [(StudentProvided,) . (\t -> Available.Option t Nothing False) <$> (unName <$> genName)]
+                      Available.FreeInt -> [(StudentProvided,) . (\t -> Available.Option t Nothing False) <$> (show <$> genInt)]
+                      Available.FreeChar -> [(StudentProvided,) . (\t -> Available.Option t Nothing False) . T.singleton <$> genChar]
               case opts'' of
                 [] -> annotate "no options" >> success
                 options -> do
@@ -433,7 +433,7 @@ unit_sat_con_1 =
     Intermediate
     (emptyHole `ann` (tEmptyHole `tfun` tEmptyHole))
     (InExpr [Child1])
-    (Right (MakeCon, Option "Cons" $ Just $ unName <$> unModuleName builtinModuleName))
+    (Right (MakeCon, Option "Cons" (Just $ unName <$> unModuleName builtinModuleName) False))
     (hole (con cCons [emptyHole, emptyHole]) `ann` (tEmptyHole `tfun` tEmptyHole))
 
 unit_sat_con_2 :: Assertion
@@ -443,7 +443,7 @@ unit_sat_con_2 =
     Intermediate
     (emptyHole `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat)))
     (InExpr [Child1])
-    (Right (MakeCon, Option "Cons" $ Just $ unName <$> unModuleName builtinModuleName))
+    (Right (MakeCon, Option "Cons" (Just $ unName <$> unModuleName builtinModuleName) False))
     (hole (con cCons [emptyHole, emptyHole]) `ann` ((tcon tList `tapp` tcon tNat) `tfun` (tcon tList `tapp` tcon tNat)))
 
 -- The various @let@ constructs inherit the directionality of their body.
@@ -650,7 +650,7 @@ offeredNamesTest initial moves act name =
     Expert
     initial
     moves
-    (Right (act, Option name Nothing))
+    (Right (act, Option name Nothing False))
 
 -- Note that lambdas are the only form which we have interesting name info when
 -- we initially create them.