Add the ability to increase instance search depth (#873)

* Store auxiliary constraints separately

* Solve constraints one by one

* Increase search depth when struggling on metas

vehicle/src/Vehicle/Backend/Agda/Compile.hs

@@ -78,7 +78,7 @@ logEntry :: (MonadAgdaCompile m) => Expr Builtin -> m ()
 logEntry e = do
   incrCallDepth
   ctx <- getNamedBoundCtx (Proxy @())
-  logDebug MaxDetail $ "compile-entry" <+> prettyFriendly (WithContext e ctx)
+  logDebug MaxDetail $ "compile-entry" <+> prettyExternal (WithContext e ctx)
 
 logExit :: (MonadAgdaCompile m) => Code -> m ()
 logExit e = do
@@ -587,9 +587,7 @@ compileBuiltin _p b args = case b of
     Quantifier q -> case reverse args of
       (ExplicitArg _ _ (Lam _ binder body)) : _ -> compileTypeLevelQuantifier q [binder] body
       _ -> unsupportedArgsError
-    FromNat dom -> case reverse args of
-      (_inst : value : _) -> compileFromNat dom <$> compileArg value
-      _ -> unsupportedArgsError
+    FromNat dom -> compileFromNat dom args
     FromRat dom -> case reverse args of
       (value : _) -> compileFromRat dom <$> compileArg value
       _ -> unsupportedArgsError
@@ -619,10 +617,11 @@ compileBuiltin _p b args = case b of
 
     unsupportedArgsError :: (MonadAgdaCompile m) => m a
     unsupportedArgsError = do
-      ctx <- getNamedBoundCtx (Proxy @())
       compilerDeveloperError $
         "compilation of"
-          <+> prettyFriendly (WithContext (normAppList (Builtin mempty b) args) ctx)
+          <+> quotePretty b
+          <+> "with args"
+          <+> prettyVerbose args
           <+> "to Agda unsupported"
 
     resolveInstance :: (MonadAgdaCompile m) => Builtin -> [Arg Builtin] -> m Code
@@ -745,11 +744,22 @@ compileNeg dom args = do
 
   annotateInfixOp1 [dependency] 8 (Just qualifier) "-" args
 
-compileFromNat :: FromNatDomain -> Code -> Code
-compileFromNat dom value = case dom of
-  FromNatToIndex -> agdaNatToFin [value]
-  FromNatToNat -> value
-  FromNatToRat -> agdaDivRat [agdaPosInt [value], "1"]
+compileFromNat :: (MonadAgdaCompile m) => FromNatDomain -> [Arg Builtin] -> m Code
+compileFromNat dom args = case (dom, args) of
+  (FromNatToNat, [value, _]) -> compileExpr $ argExpr value
+  (FromNatToRat, [value, _]) -> do
+    v <- compileExpr $ argExpr value
+    return $ agdaDivRat [agdaPosInt [v], "1"]
+  (FromNatToIndex, [_inst, value, _]) -> do
+    v <- compileExpr $ argExpr value
+    return $ agdaNatToFin [v]
+  _ -> do
+    compilerDeveloperError $
+      "compilation of"
+        <+> quotePretty (FromNat dom)
+        <+> "with args"
+        <+> prettyVerbose args
+        <+> "to Agda unsupported"
 
 compileFromRat :: FromRatDomain -> Code -> Code
 compileFromRat dom arg = case dom of

vehicle/src/Vehicle/Compile/Normalise/Builtin.hs

@@ -55,21 +55,18 @@ type Eval builtin m =
   Expr builtin ->
   m (Value builtin)
 
-evalTypeClassOp ::
+evalBuiltinFunction ::
   (MonadLogger m, BuiltinHasStandardData builtin, Show builtin) =>
   (BuiltinFunction -> EvalBuiltin (Value builtin) m) ->
   EvalApp (Value builtin) m ->
   Value builtin ->
   builtin ->
   Spine builtin ->
   m (Value builtin)
-evalTypeClassOp evalFn evalApp originalExpr b normArgs
-  | isTypeClassOp b = do
-      (inst, remainingArgs) <- findInstanceArg b normArgs
-      evalApp inst remainingArgs
-  | otherwise = case getBuiltinFunction b of
-      Nothing -> return originalExpr
-      Just f -> evalFn f evalApp originalExpr normArgs
+evalBuiltinFunction evalFn evalApp originalExpr b normArgs =
+  case getBuiltinFunction b of
+    Nothing -> return originalExpr
+    Just f -> evalFn f evalApp originalExpr normArgs
 
 findInstanceArg :: (MonadLogger m, Show op) => op -> [GenericArg a] -> m (a, [GenericArg a])
 findInstanceArg op = \case
@@ -504,7 +501,7 @@ functionBlockingArgs = \case
   Implies -> []
 
 instance NormalisableBuiltin Builtin where
-  evalBuiltinApp = evalTypeClassOp $ \b evalApp originalValue args -> case b of
+  evalBuiltinApp = evalBuiltinFunction $ \b evalApp originalValue args -> case b of
     Quantifier {} -> return originalValue
     Not -> return $ evalNot originalValue args
     And -> return $ evalAnd originalValue args
@@ -565,7 +562,7 @@ instance NormalisableBuiltin LossTensorBuiltin where
   blockingArgs = developerError "forcing not yet implemented for tensor builtins"
 
 instance NormalisableBuiltin LinearityBuiltin where
-  evalBuiltinApp = evalTypeClassOp $ \b evalApp originalValue args -> case b of
+  evalBuiltinApp = evalBuiltinFunction $ \b evalApp originalValue args -> case b of
     Quantifier {} -> return originalValue
     Not -> return $ evalNot originalValue args
     And -> return $ evalAnd originalValue args
@@ -618,7 +615,7 @@ evalLinearityFoldList evalApp originalExpr args =
     _ -> return originalExpr
 
 instance NormalisableBuiltin PolarityBuiltin where
-  evalBuiltinApp = evalTypeClassOp $ \b evalApp originalValue args -> case b of
+  evalBuiltinApp = evalBuiltinFunction $ \b evalApp originalValue args -> case b of
     Quantifier {} -> return originalValue
     Not -> return $ evalNot originalValue args
     And -> return $ evalAnd originalValue args

vehicle/src/Vehicle/Compile/Normalise/NBE.hs

@@ -21,10 +21,11 @@ import Vehicle.Compile.Context.Bound.Class (MonadBoundContext (..))
 import Vehicle.Compile.Context.Free.Class (MonadFreeContext (..), getFreeEnv)
 import Vehicle.Compile.Context.Name (MonadNameContext, addNameToContext, getBinderContext)
 import Vehicle.Compile.Error
-import Vehicle.Compile.Normalise.Builtin (NormalisableBuiltin (..), filterOutIrrelevantArgs)
+import Vehicle.Compile.Normalise.Builtin (NormalisableBuiltin (..), filterOutIrrelevantArgs, findInstanceArg)
 import Vehicle.Compile.Normalise.Quote (Quote (..))
 import Vehicle.Compile.Prelude
 import Vehicle.Compile.Print
+import Vehicle.Compile.Print.Builtin (PrintableBuiltin (..))
 import Vehicle.Data.Code.Value
 
 -- import Control.Monad (when)
@@ -179,10 +180,15 @@ evalBuiltin ::
   Spine builtin ->
   m (Value builtin)
 evalBuiltin freeEnv b args = do
-  let relArgs = filterOutIrrelevantArgs args
-  -- when (length relArgs /= length (spine <> args)) $ do
-  --   compilerDeveloperError $ "Bang" <> line <> prettyVerbose relArgs <> line <> prettyVerbose fun <> line <> prettyVerbose args <> line <> "Boom"
-  evalBuiltinApp (evalApp freeEnv) (VBuiltin b args) b relArgs
+  if isTypeClassOp b
+    then do
+      (inst, remainingArgs) <- findInstanceArg b args
+      evalApp freeEnv inst remainingArgs
+    else do
+      let relArgs = filterOutIrrelevantArgs args
+      -- when (length relArgs /= length (spine <> args)) $ do
+      --   compilerDeveloperError $ "Bang" <> line <> prettyVerbose relArgs <> line <> prettyVerbose fun <> line <> prettyVerbose args <> line <> "Boom"
+      evalBuiltinApp (evalApp freeEnv) (VBuiltin b args) b relArgs
 
 lookupIdentValueInEnv ::
   forall builtin m.

vehicle/src/Vehicle/Compile/Print.hs

@@ -11,6 +11,8 @@ module Vehicle.Compile.Print
     PrettyExternal,
     PrintableBuiltin,
     Tags (..),
+    In,
+    NoCtx,
     prettyVerbose,
     prettyFriendly,
     prettyExternal,

vehicle/src/Vehicle/Compile/Print/Builtin.hs

@@ -133,6 +133,13 @@ class (Show builtin, Pretty builtin, ConvertableBuiltin builtin Builtin) => Prin
   -- builtin type. Used for printing.
   isCoercion :: builtin -> Bool
 
+  getBuiltinTypeClassOp :: builtin -> Maybe TypeClassOp
+
+  isTypeClassOp :: builtin -> Bool
+  isTypeClassOp b = case getBuiltinTypeClassOp b of
+    Just {} -> True
+    Nothing -> False
+
 instance PrintableBuiltin Builtin where
   isCoercion = \case
     BuiltinFunction FromNat {} -> True
@@ -142,18 +149,30 @@ instance PrintableBuiltin Builtin where
     TypeClassOp FromVecTC {} -> True
     _ -> False
 
+  getBuiltinTypeClassOp = \case
+    TypeClassOp op -> Just op
+    _ -> Nothing
+
 instance PrintableBuiltin PolarityBuiltin where
   isCoercion = const False
 
+  getBuiltinTypeClassOp = const Nothing
+
 instance PrintableBuiltin LinearityBuiltin where
   isCoercion = const False
 
+  getBuiltinTypeClassOp = const Nothing
+
 instance PrintableBuiltin TensorBuiltin where
   isCoercion = const False
 
+  getBuiltinTypeClassOp = const Nothing
+
 instance PrintableBuiltin LossTensorBuiltin where
   isCoercion = const False
 
+  getBuiltinTypeClassOp = const Nothing
+
 isCoercionExpr :: (PrintableBuiltin builtin) => Expr builtin -> Bool
 isCoercionExpr = \case
   Builtin _ b -> isCoercion b

vehicle/src/Vehicle/Compile/Print/TypingError.hs

@@ -84,9 +84,8 @@ typingErrorDetails = \case
               <+> "but was unable to prove it."
           CheckingInstanceType instanceOrigin ->
             instanceOriginConstraintMessage instanceOrigin
-          CheckingAuxiliary ->
-            developerError "Auxiliary constraints should not be unsolved."
         InstanceConstraint (Resolve instanceOrigin _ _ _) -> instanceOriginConstraintMessage instanceOrigin
+        -- AuxiliaryConstraint (Auxiliary auxiliaryOrigin _ _) -> auxiliaryOriginConstraintMessage auxiliaryOrigin
         ApplicationConstraint {} ->
           "unsolved application constraint: " <+> prettyFriendly (WithContext constraint ctx)
 
@@ -206,8 +205,6 @@ failedUnificationConstraintsError (FailedUnificationConstraintsError (err :| _))
                 <+> squotes (prettyTypeClassConstraintOriginExpr ctx checkedInstanceOp checkedInstanceOpArgs)
             CheckingInstanceType (InstanceTypeRestrictionOrigin {}) ->
               ""
-            CheckingAuxiliary ->
-              developerError "Auxiliary constraints should not be unsolved."
       UserError
         { provenance = provenanceOf ctx,
           problem =