Reflection primitive to solve instances (#7260)

* keep the problem id also for non-blocking constraints and change
noConstraints reflection primitive to fail also on unsolved non-blocking
constraints

* issue #4777: add solveInstanceConstraints primitive

* don't fail noConstraints if solveInstanceConstraints fails to solve
constraints from outside the current macro invokation

* test case for solveInstanceConstraints

* clarify interaction between noConstraints and solveInstanceConstraints

* update interaction test output

* comment for isBlockingConstraint

CHANGELOG.md

@@ -131,6 +131,16 @@ Reflection
 
 Changes to the meta-programming facilities.
 
+* Add new primitive to run instance search from reflection code:
+
+  ```agda
+    -- Try to solve open instance constraints. When wrapped in `noConstraints`,
+    -- fails if there are unsolved instance constraints left over that originate
+    -- from the current macro invokation. Outside constraints are still attempted,
+    -- but failure to solve them are ignored by `noConstraints`.
+    solveInstanceConstraints : TC ⊤
+  ```
+
 Library management
 ------------------
 

doc/user-manual/language/reflection.lagda.rst

@@ -545,6 +545,12 @@ following primitive operations::
     -- variable (it does not have to be an instance meta).
     getInstances : Meta → TC (List Term)
 
+    -- Try to solve open instance constraints. When wrapped in `noConstraints`,
+    -- fails if there are unsolved instance constraints left over that originate
+    -- from the current macro invokation. Outside constraints are still attempted,
+    -- but failure to solve them are ignored by `noConstraints`.
+    solveInstanceConstraints : TC ⊤
+
   {-# BUILTIN AGDATCMUNIFY                      unify                      #-}
   {-# BUILTIN AGDATCMTYPEERROR                  typeError                  #-}
   {-# BUILTIN AGDATCMBLOCK                      blockTC                    #-}
@@ -569,6 +575,8 @@ following primitive operations::
   {-# BUILTIN AGDATCMGETDEFINITION              getDefinition              #-}
   {-# BUILTIN AGDATCMCOMMIT                     commitTC                   #-}
   {-# BUILTIN AGDATCMISMACRO                    isMacro                    #-}
+  {-# BUILTIN AGDATCMPRAGMAFOREIGN              pragmaForeign              #-}
+  {-# BUILTIN AGDATCMPRAGMACOMPILE              pragmaCompile              #-}
   {-# BUILTIN AGDATCMWITHNORMALISATION          withNormalisation          #-}
   {-# BUILTIN AGDATCMWITHRECONSTRUCTED          withReconstructed          #-}
   {-# BUILTIN AGDATCMWITHEXPANDLAST             withExpandLast             #-}
@@ -581,6 +589,7 @@ following primitive operations::
   {-# BUILTIN AGDATCMNOCONSTRAINTS              noConstraints              #-}
   {-# BUILTIN AGDATCMRUNSPECULATIVE             runSpeculative             #-}
   {-# BUILTIN AGDATCMGETINSTANCES               getInstances               #-}
+  {-# BUILTIN AGDATCMSOLVEINSTANCES             solveInstanceConstraints   #-}
 
 Metaprogramming
 ---------------

src/data/lib/prim/Agda/Builtin/Reflection.agda

@@ -343,6 +343,12 @@ postulate
   -- variable (it does not have to be an instance meta).
   getInstances : Meta → TC (List Term)
 
+  -- Try to solve open instance constraints. When wrapped in `noConstraints`,
+  -- fails if there are unsolved instance constraints left over that originate
+  -- from the current macro invokation. Outside constraints are still attempted,
+  -- but failure to solve them are ignored by `noConstraints`.
+  solveInstanceConstraints : TC ⊤
+
 {-# BUILTIN AGDATCM                           TC                         #-}
 {-# BUILTIN AGDATCMRETURN                     returnTC                   #-}
 {-# BUILTIN AGDATCMBIND                       bindTC                     #-}
@@ -385,6 +391,7 @@ postulate
 {-# BUILTIN AGDATCMNOCONSTRAINTS              noConstraints              #-}
 {-# BUILTIN AGDATCMRUNSPECULATIVE             runSpeculative             #-}
 {-# BUILTIN AGDATCMGETINSTANCES               getInstances               #-}
+{-# BUILTIN AGDATCMSOLVEINSTANCES             solveInstanceConstraints   #-}
 
 -- All the TC primitives are compiled to functions that return
 -- undefined, rather than just undefined, in an attempt to make sure

src/full/Agda/Compiler/MAlonzo/Compiler.hs

@@ -308,6 +308,7 @@ ghcPreCompile flags = do
       , builtinAgdaTCMRunSpeculative
       , builtinAgdaTCMExec
       , builtinAgdaTCMGetInstances
+      , builtinAgdaTCMSolveInstances
       , builtinAgdaTCMPragmaForeign
       , builtinAgdaTCMPragmaCompile
       , builtinAgdaBlocker

src/full/Agda/Syntax/Builtin.hs

@@ -240,6 +240,7 @@ data BuiltinId
   | BuiltinAgdaTCMRunSpeculative
   | BuiltinAgdaTCMExec
   | BuiltinAgdaTCMGetInstances
+  | BuiltinAgdaTCMSolveInstances
   | BuiltinAgdaTCMPragmaForeign
   | BuiltinAgdaTCMPragmaCompile
   | BuiltinAgdaBlocker
@@ -459,6 +460,7 @@ instance IsBuiltin BuiltinId where
     BuiltinAgdaTCMRunSpeculative             -> "AGDATCMRUNSPECULATIVE"
     BuiltinAgdaTCMExec                       -> "AGDATCMEXEC"
     BuiltinAgdaTCMGetInstances               -> "AGDATCMGETINSTANCES"
+    BuiltinAgdaTCMSolveInstances             -> "AGDATCMSOLVEINSTANCES"
     BuiltinAgdaTCMPragmaForeign              -> "AGDATCMPRAGMAFOREIGN"
     BuiltinAgdaTCMPragmaCompile              -> "AGDATCMPRAGMACOMPILE"
     BuiltinAgdaBlocker                       -> "AGDABLOCKER"
@@ -583,6 +585,7 @@ builtinNat, builtinSuc, builtinZero, builtinNatPlus, builtinNatMinus,
   builtinAgdaTCMRunSpeculative,
   builtinAgdaTCMExec,
   builtinAgdaTCMGetInstances,
+  builtinAgdaTCMSolveInstances,
   builtinAgdaTCMPragmaForeign,
   builtinAgdaTCMPragmaCompile
   :: BuiltinId
@@ -782,6 +785,7 @@ builtinAgdaTCMNoConstraints              = BuiltinAgdaTCMNoConstraints
 builtinAgdaTCMRunSpeculative             = BuiltinAgdaTCMRunSpeculative
 builtinAgdaTCMExec                       = BuiltinAgdaTCMExec
 builtinAgdaTCMGetInstances               = BuiltinAgdaTCMGetInstances
+builtinAgdaTCMSolveInstances             = BuiltinAgdaTCMSolveInstances
 builtinAgdaTCMPragmaForeign              = BuiltinAgdaTCMPragmaForeign
 builtinAgdaTCMPragmaCompile              = BuiltinAgdaTCMPragmaCompile
 builtinAgdaBlocker                       = BuiltinAgdaBlocker

src/full/Agda/TypeChecking/Constraints.hs

@@ -143,9 +143,22 @@ stealConstraintsTCM pid = do
 noConstraints
   :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
   => m a -> m a
-noConstraints problem = do
+noConstraints = noConstraints' False
+
+-- | As noConstraints but also fail for non-blocking constraints.
+reallyNoConstraints
+  :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
+  => m a -> m a
+reallyNoConstraints = noConstraints' True
+
+noConstraints'
+  :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
+  => Bool -> m a -> m a
+noConstraints' includingNonBlocking problem = do
   (pid, x) <- newProblem problem
-  cs <- getConstraintsForProblem pid
+  let counts | includingNonBlocking = const True
+             | otherwise            = isBlockingConstraint . clValue . theConstraint
+  cs <- filter counts <$> getConstraintsForProblem pid
   unless (null cs) $ do
     withCurrentCallStack $ \loc -> do
       w <- warning'_ loc (UnsolvedConstraints cs)

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -3678,6 +3678,12 @@ data TCEnv =
           , envAssignMetas         :: Bool
             -- ^ Are we allowed to assign metas?
           , envActiveProblems      :: Set ProblemId
+          , envUnquoteProblem      :: Maybe ProblemId
+            -- ^ If inside a `runUnquoteM` call, stores the top-level problem id assigned to the
+            --   invokation. We use this to decide which instance constraints originate from the
+            --   current call and which come from the outside, for the purpose of a
+            --   `solveInstanceConstraints` inside `noConstraints` only failing for local instance
+            --   constraints.
           , envAbstractMode        :: AbstractMode
                 -- ^ When checking the typesignature of a public definition
                 --   or the body of a non-abstract definition this is true.
@@ -3817,6 +3823,7 @@ initEnv = TCEnv { envContext             = []
                 , envSolvingConstraints  = False
                 , envCheckingWhere       = False
                 , envActiveProblems      = Set.empty
+                , envUnquoteProblem      = Nothing
                 , envWorkingOnTypes      = False
                 , envAssignMetas         = True
                 , envAbstractMode        = ConcreteMode

src/full/Agda/TypeChecking/Monad/Builtin.hs

@@ -289,6 +289,7 @@ primInteger, primIntegerPos, primIntegerNegSuc,
     primAgdaTCMRunSpeculative,
     primAgdaTCMExec,
     primAgdaTCMGetInstances,
+    primAgdaTCMSolveInstances,
     primAgdaTCMPragmaForeign,
     primAgdaTCMPragmaCompile
     :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
@@ -505,6 +506,7 @@ primAgdaTCMNoConstraints              = getBuiltin builtinAgdaTCMNoConstraints
 primAgdaTCMRunSpeculative             = getBuiltin builtinAgdaTCMRunSpeculative
 primAgdaTCMExec                       = getBuiltin builtinAgdaTCMExec
 primAgdaTCMGetInstances               = getBuiltin builtinAgdaTCMGetInstances
+primAgdaTCMSolveInstances             = getBuiltin builtinAgdaTCMSolveInstances
 primAgdaTCMPragmaForeign              = getBuiltin builtinAgdaTCMPragmaForeign
 primAgdaTCMPragmaCompile              = getBuiltin builtinAgdaTCMPragmaCompile
 

src/full/Agda/TypeChecking/Monad/Constraints.hs

@@ -35,9 +35,20 @@ solvingProblems pids m = verboseBracket "tc.constr.solve" 50 ("working on proble
   return x
 
 isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
-isProblemSolved pid =
+isProblemSolved = isProblemSolved' False
+
+isProblemCompletelySolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
+isProblemCompletelySolved = isProblemSolved' True
+
+isProblemSolved' :: (MonadTCEnv m, ReadTCState m) => Bool -> ProblemId -> m Bool
+isProblemSolved' completely pid =
   and2M (not . Set.member pid <$> asksTC envActiveProblems)
-        (not . any (Set.member pid . constraintProblems) <$> getAllConstraints)
+        (not . any belongsToUs <$> getAllConstraints)
+  where
+    belongsToUs c
+      | Set.notMember pid (constraintProblems c)         = False
+      | isBlockingConstraint (clValue $ theConstraint c) = True
+      | otherwise                                        = completely -- Ignore non-blocking unless `completely`
 
 {-# SPECIALIZE getConstraintsForProblem :: ProblemId -> TCM Constraints #-}
 getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints
@@ -181,32 +192,37 @@ addAwakeConstraint' = addConstraintTo stAwakeConstraints
 
 addConstraintTo :: Lens' TCState Constraints -> Blocker -> Constraint -> TCM ()
 addConstraintTo bucket unblock c = do
-    pc <- build
+    pc <- buildConstraint unblock c
     stDirty `setTCLens` True
     bucket `modifyTCLens` (pc :)
-  where
-    build | isBlocking c = buildConstraint unblock c
-          | otherwise    = buildProblemConstraint_ unblock c
-    isBlocking = \case
-      SortCmp{}        -> False
-      LevelCmp{}       -> False
-      FindInstance{}   -> False
-      ResolveInstanceHead{} -> False
-      HasBiggerSort{}  -> False
-      HasPTSRule{}     -> False
-      CheckDataSort{}  -> False
-      ValueCmp{}       -> True
-      ValueCmpOnFace{} -> True
-      ElimCmp{}        -> True
-      UnBlock{}        -> True
-      IsEmpty{}        -> True
-      CheckSizeLtSat{} -> True
-      CheckFunDef{}    -> True
-      UnquoteTactic{}  -> True
-      CheckMetaInst{}  -> True
-      CheckType{}      -> True
-      CheckLockedVars{} -> True
-      UsableAtModality{} -> True
+
+-- | A problem is considered solved if there are no unsolved blocking constraints belonging to it.
+--   There's no really good principle for what constraints are blocking and which are not, but the
+--   general idea is that nothing bad should happen if you assume a non-blocking constraint is
+--   solvable, but it turns out it isn't. For instance, assuming an equality constraint between two
+--   types that turns out to be false can lead to ill typed terms in places where we don't expect
+--   them.
+isBlockingConstraint :: Constraint -> Bool
+isBlockingConstraint = \case
+  SortCmp{}             -> False
+  LevelCmp{}            -> False
+  FindInstance{}        -> False
+  ResolveInstanceHead{} -> False
+  HasBiggerSort{}       -> False
+  HasPTSRule{}          -> False
+  CheckDataSort{}       -> False
+  ValueCmp{}            -> True
+  ValueCmpOnFace{}      -> True
+  ElimCmp{}             -> True
+  UnBlock{}             -> True
+  IsEmpty{}             -> True
+  CheckSizeLtSat{}      -> True
+  CheckFunDef{}         -> True
+  UnquoteTactic{}       -> True
+  CheckMetaInst{}       -> True
+  CheckType{}           -> True
+  CheckLockedVars{}     -> True
+  UsableAtModality{}    -> True
 
 -- | Start solving constraints
 nowSolvingConstraints :: MonadTCEnv m => m a -> m a

src/full/Agda/TypeChecking/Rules/Builtin.hs

@@ -412,6 +412,7 @@ coreBuiltins =
                                                                           (Lam defaultArgInfo . Abs "_" <$> (primSigma <#> primLevelZero <#> primLevelZero <@> primString <@>
                                                                            (Lam defaultArgInfo . Abs "_" <$> primString)))))
   , builtinAgdaTCMGetInstances               |-> builtinPostulate (tmeta --> tTCM_ (list primAgdaTerm))
+  , builtinAgdaTCMSolveInstances             |-> builtinPostulate (tTCM_ primUnit)
   , builtinAgdaTCMPragmaForeign              |-> builtinPostulate (tstring --> tstring --> tTCM_ primUnit)
   , builtinAgdaTCMPragmaCompile              |-> builtinPostulate (tstring --> tqname --> tstring --> tTCM_ primUnit)
   ]

src/full/Agda/TypeChecking/Unquote.hs

@@ -100,7 +100,10 @@ runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
 runUnquoteM m = do
   cxt <- asksTC envContext
   s   <- getTC
-  z   <- unpackUnquoteM m cxt (Clean, s)
+  pid <- fresh  -- Create a fresh problem for the unquote call. Used in tcSolveInstances.
+  z   <- localTC (\ e -> e { envUnquoteProblem = Just pid })
+       $ solvingProblem pid
+       $ unpackUnquoteM m cxt (Clean, s)
   case z of
     Left err              -> return $ Left err
     Right ((x, _), decls) -> Right (x, decls) <$ mapM_ isDefined decls
@@ -582,6 +585,7 @@ evalTCM v = Bench.billTo [Bench.Typing, Bench.Reflection] do
              , (f `isDef` primAgdaTCMAskReconstructed, tcAskReconstructed)
              , (f `isDef` primAgdaTCMAskExpandLast,    tcAskExpandLast)
              , (f `isDef` primAgdaTCMAskReduceDefs,    tcAskReduceDefs)
+             , (f `isDef` primAgdaTCMSolveInstances,   tcSolveInstances)
              ]
              failEval
     I.Def f [u] ->
@@ -744,7 +748,7 @@ evalTCM v = Bench.billTo [Bench.Typing, Bench.Reflection] do
       primUnitUnit
 
     tcNoConstraints :: Term -> UnquoteM Term
-    tcNoConstraints m = liftU1 noConstraints (evalTCM m)
+    tcNoConstraints m = liftU1 reallyNoConstraints (evalTCM m)
 
     tcInferType :: R.Term -> TCM Term
     tcInferType v = do
@@ -1097,6 +1101,24 @@ evalTCM v = Bench.billTo [Bench.Typing, Bench.Reflection] do
       Right cands -> liftTCM $
         buildList <*> mapM (quoteTerm . candidateTerm) cands
 
+    tcSolveInstances :: UnquoteM Term
+    tcSolveInstances = liftTCM $ do
+      locallyTCState stPostponeInstanceSearch (const False) $ do
+        -- Steal instance constraints (TODO: not all!)
+        current <- asksTC envActiveProblems
+        topPid  <- fromMaybe __IMPOSSIBLE__ <$> asksTC envUnquoteProblem
+        let steal pc@(PConstr pids u c)
+              | isInstance pc
+              , Set.member topPid pids = PConstr (Set.union current pids) u c
+              | otherwise              = pc
+            isInstance c | FindInstance{} <- clValue (theConstraint c) = True
+                         | otherwise                                   = False
+        modifyAwakeConstraints    $ map steal
+        modifySleepingConstraints $ map steal
+        wakeConstraints (wakeUpWhen_ isInstance)
+        solveSomeAwakeConstraints isInstance True  -- Force solving them now!
+      primUnitUnit
+
     splitPars :: Int -> A.Expr -> ([A.TypedBinding], A.Expr)
     splitPars 0 e = ([] , e)
     splitPars npars (A.Pi _ (n :| _) e) = first (n :) (splitPars (npars - 1) e)