diff --git a/vehicle/src/Vehicle/Backend/Agda/Compile.hs b/vehicle/src/Vehicle/Backend/Agda/Compile.hs
index 52d0f1945..d9bdcc119 100644
--- a/vehicle/src/Vehicle/Backend/Agda/Compile.hs
+++ b/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
diff --git a/vehicle/src/Vehicle/Compile/Normalise/Builtin.hs b/vehicle/src/Vehicle/Compile/Normalise/Builtin.hs
index 289d4395f..2f98a34a7 100644
--- a/vehicle/src/Vehicle/Compile/Normalise/Builtin.hs
+++ b/vehicle/src/Vehicle/Compile/Normalise/Builtin.hs
@@ -55,7 +55,7 @@ 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 ->
@@ -63,13 +63,10 @@ evalTypeClassOp ::
   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
diff --git a/vehicle/src/Vehicle/Compile/Normalise/NBE.hs b/vehicle/src/Vehicle/Compile/Normalise/NBE.hs
index e6538ddc5..7c6d51d23 100644
--- a/vehicle/src/Vehicle/Compile/Normalise/NBE.hs
+++ b/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.
diff --git a/vehicle/src/Vehicle/Compile/Print.hs b/vehicle/src/Vehicle/Compile/Print.hs
index 687222fd1..0ce65a761 100644
--- a/vehicle/src/Vehicle/Compile/Print.hs
+++ b/vehicle/src/Vehicle/Compile/Print.hs
@@ -11,6 +11,8 @@ module Vehicle.Compile.Print
     PrettyExternal,
     PrintableBuiltin,
     Tags (..),
+    In,
+    NoCtx,
     prettyVerbose,
     prettyFriendly,
     prettyExternal,
diff --git a/vehicle/src/Vehicle/Compile/Print/Builtin.hs b/vehicle/src/Vehicle/Compile/Print/Builtin.hs
index d585a34c7..b98643408 100644
--- a/vehicle/src/Vehicle/Compile/Print/Builtin.hs
+++ b/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
diff --git a/vehicle/src/Vehicle/Compile/Print/TypingError.hs b/vehicle/src/Vehicle/Compile/Print/TypingError.hs
index c0648f8aa..004aaedea 100644
--- a/vehicle/src/Vehicle/Compile/Print/TypingError.hs
+++ 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 =
diff --git a/vehicle/src/Vehicle/Compile/Type.hs b/vehicle/src/Vehicle/Compile/Type.hs
index c58d85920..c70e0b089 100644
--- a/vehicle/src/Vehicle/Compile/Type.hs
+++ b/vehicle/src/Vehicle/Compile/Type.hs
@@ -17,10 +17,11 @@ import Vehicle.Compile.Print
 import Vehicle.Compile.Type.Bidirectional
 import Vehicle.Compile.Type.Constraint.ApplicationSolver (runApplicationSolver)
 import Vehicle.Compile.Type.Constraint.Core (runConstraintSolver)
+import Vehicle.Compile.Type.Constraint.InstanceDefaultSolver (addNewInstanceConstraintUsingDefaults)
+import Vehicle.Compile.Type.Constraint.InstanceSolver (runInstanceSolver)
 import Vehicle.Compile.Type.Constraint.UnificationSolver
 import Vehicle.Compile.Type.Core
 import Vehicle.Compile.Type.Generalise
-import Vehicle.Compile.Type.Meta
 import Vehicle.Compile.Type.Meta.Set qualified as MetaSet
 import Vehicle.Compile.Type.Monad
 import Vehicle.Compile.Type.Monad.Class
@@ -110,7 +111,7 @@ typeCheckAbstractDef p ident defSort uncheckedType = do
 
   let substDecl = DefAbstract p ident defSort substCheckedType
 
-  logUnsolvedUnknowns (Just substDecl) Nothing
+  logUnsolvedUnknowns (Just substDecl)
 
   finalDecl <- generaliseOverUnsolvedMetaVariables substDecl
   return finalDecl
@@ -152,7 +153,7 @@ typeCheckFunction p ident anns typ body = do
         if isUserIdent ident
           then addAuxiliaryInputOutputConstraints substDecl
           else return substDecl
-      logUnsolvedUnknowns (Just substDecl) Nothing
+      logUnsolvedUnknowns (Just substDecl)
 
       checkedDecl2 <- generaliseOverUnsolvedConstraints checkedDecl1
       checkedDecl3 <- generaliseOverUnsolvedMetaVariables checkedDecl2
@@ -187,60 +188,79 @@ restrictAbstractDefType resource decl@(ident, _) defType = do
 -- occur in the type or not.
 solveConstraints :: forall builtin m. (TCM builtin m) => Maybe (Decl builtin) -> m ()
 solveConstraints d = logCompilerPass MidDetail "constraint solving" $ do
-  loopOverConstraints mempty 1 d
+  loopOverConstraints 1 d
   where
-    loopOverConstraints :: (TCM builtin m) => MetaSet -> Int -> Maybe (Decl builtin) -> m ()
-    loopOverConstraints recentlySolvedMetas loopNumber decl = do
+    loopOverConstraints :: (TCM builtin m) => Int -> Maybe (Decl builtin) -> m ()
+    loopOverConstraints loopNumber decl = do
       unsolvedConstraints <- getActiveConstraints @builtin
 
       updatedDecl <- traverse substMetas decl
-      logUnsolvedUnknowns updatedDecl (Just recentlySolvedMetas)
+      logUnsolvedUnknowns updatedDecl
 
       unless (null unsolvedConstraints) $ do
-        let allConstraintsBlocked = all (constraintIsBlocked recentlySolvedMetas) unsolvedConstraints
+        isUnblocked <- getIsUnblockedFn
 
-        if allConstraintsBlocked
+        if any isUnblocked unsolvedConstraints
           then do
+            -- If we have unblocked constraints then start a new pass
+            let passDoc = "constraint solving pass" <+> pretty loopNumber
+            logCompilerPass MaxDetail passDoc $
+              runSolvers updatedDecl
+            loopOverConstraints (loopNumber + 1) updatedDecl
+          else do
             -- If no constraints are unblocked then try generating new constraints using defaults.
-            instanceCandidates <- getInstanceCandidates
-            successfullyGeneratedDefault <- generateDefaultConstraint instanceCandidates decl
-            when successfullyGeneratedDefault $
+            logDebug MaxDetail $ "Temporarily stuck" <> line
+            success <- tryToUnstick updatedDecl
+            when success $
               -- If new constraints generated then continue solving.
-              loopOverConstraints mempty loopNumber decl
-          else do
-            -- If we have made useful progress then start a new pass
-            let passDoc = "constraint solving pass" <+> pretty loopNumber
-            newMetasSolved <- logCompilerPass MaxDetail passDoc $ do
-              metasSolvedDuringApplications <-
-                trackSolvedMetas (Proxy @builtin) $
-                  runApplicationSolver (Proxy @builtin) recentlySolvedMetas
+              loopOverConstraints loopNumber decl
+
+    runSolvers :: (TCM builtin m) => Maybe (Decl builtin) -> m ()
+    runSolvers maybeDecl = do
+      let proxy = Proxy @builtin
+
+      logUnsolvedUnknowns maybeDecl
+      runApplicationSolver proxy
+
+      logUnsolvedUnknowns maybeDecl
+      runUnificationSolver proxy
 
-              metasSolvedDuringUnification <-
-                trackSolvedMetas (Proxy @builtin) $
-                  runUnificationSolver (Proxy @builtin) (metasSolvedDuringApplications <> recentlySolvedMetas)
+      logUnsolvedUnknowns maybeDecl
+      runInstanceSolver proxy 0
 
-              logUnsolvedUnknowns updatedDecl (Just recentlySolvedMetas)
+      logUnsolvedUnknowns maybeDecl
+      runAuxiliarySolver proxy
 
-              metasSolvedDuringInstanceResolution <-
-                trackSolvedMetas (Proxy @builtin) $
-                  runInstanceSolver (Proxy @builtin) (metasSolvedDuringUnification <> metasSolvedDuringApplications)
+    tryToUnstick :: (TCM builtin m) => Maybe (Decl builtin) -> m Bool
+    tryToUnstick decl = do
+      -- First try to increase the depth limit for instance search
+      solvedMetas <- logCompilerPass MidDetail "trying to increase the depth for instance search" $ do
+        trackSolvedMetas (Proxy @builtin) $ runInstanceSolver (Proxy @builtin) 1
 
-              return (metasSolvedDuringInstanceResolution <> metasSolvedDuringUnification)
+      if not (MetaSet.null solvedMetas)
+        then return True
+        else do
+          -- Then if that fails try to use default instances
+          success <- logCompilerPass MidDetail "trying to generate a new constraint using instance defaults" $ do
+            addNewInstanceConstraintUsingDefaults decl
 
-            loopOverConstraints newMetasSolved (loopNumber + 1) updatedDecl
+          if success
+            then return True
+            else logCompilerPass MidDetail "trying to generate a new constraint using instance defaults" $ do
+              -- Then if that fails try to use default auxiliary instances
+              generateDefaultAuxiliaryConstraint decl
 
 -- | Attempts to solve as many type-class constraints as possible. Takes in
 -- the set of meta-variables solved since the solver was last run and outputs
 -- the set of meta-variables solved during this run.
-runInstanceSolver :: forall builtin m. (TCM builtin m) => Proxy builtin -> MetaSet -> m ()
-runInstanceSolver _ metasSolved = do
-  instanceCandidates <- getInstanceCandidates
-  logCompilerPass MaxDetail ("instance solver run" <> line) $
+runAuxiliarySolver :: forall builtin m. (TCM builtin m) => Proxy builtin -> m ()
+runAuxiliarySolver proxy = do
+  logCompilerPass MaxDetail ("auxiliary solver run" <> line) $
     runConstraintSolver @builtin
-      getActiveInstanceConstraints
-      setInstanceConstraints
-      (solveInstance instanceCandidates)
-      metasSolved
+      proxy
+      getActiveAuxiliaryInstanceConstraints
+      setAuxiliaryInstanceConstraints
+      solveAuxiliaryInstanceConstraint
 
 -------------------------------------------------------------------------------
 -- Unsolved constraint checks
@@ -279,8 +299,8 @@ checkAllMetasSolved proxy = do
           )
       throwError $ TypingError $ UnsolvedMetas proxy metasAndOrigins
 
-logUnsolvedUnknowns :: forall builtin m. (TCM builtin m) => Maybe (Decl builtin) -> Maybe MetaSet -> m ()
-logUnsolvedUnknowns maybeDecl maybeSolvedMetas = do
+logUnsolvedUnknowns :: forall builtin m. (TCM builtin m) => Maybe (Decl builtin) -> m ()
+logUnsolvedUnknowns maybeDecl = do
   logDebugM MaxDetail $ do
     newSubstitution <- getMetaSubstitution (Proxy @builtin)
     updatedSubst <- substMetas newSubstitution
@@ -289,23 +309,17 @@ logUnsolvedUnknowns maybeDecl maybeSolvedMetas = do
     unsolvedMetasDoc <- prettyMetas (Proxy @builtin) unsolvedMetas
     unsolvedConstraints <- getActiveConstraints @builtin
 
-    let constraintsDoc = case maybeSolvedMetas of
-          Nothing ->
-            "unsolved-constraints:"
-              <> line
-              <> indent 2 (prettyVerbose unsolvedConstraints)
-              <> line
-          Just solvedMetas -> do
-            let isUnblocked = not . constraintIsBlocked solvedMetas
-            let (unblockedConstraints, blockedConstraints) = partition isUnblocked unsolvedConstraints
-            "unsolved-blocked-constraints:"
-              <> line
-              <> indent 2 (prettyBlockedConstraints blockedConstraints)
-              <> line
-              <> "unsolved-unblocked-constraints:"
-              <> line
-              <> indent 2 (prettyVerbose unblockedConstraints)
-              <> line
+    isUnblocked <- getIsUnblockedFn
+    let (unblockedConstraints, blockedConstraints) = partition isUnblocked unsolvedConstraints
+    let constraintsDoc =
+          "unsolved-blocked-constraints:"
+            <> line
+            <> indent 2 (prettyBlockedConstraints blockedConstraints)
+            <> line
+            <> "unsolved-unblocked-constraints:"
+            <> line
+            <> indent 2 (prettyVerbose unblockedConstraints)
+            <> line
 
     let declDoc = case maybeDecl of
           Nothing -> ""
diff --git a/vehicle/src/Vehicle/Compile/Type/Bidirectional.hs b/vehicle/src/Vehicle/Compile/Type/Bidirectional.hs
index c6a7dd0ca..90741d60e 100644
--- a/vehicle/src/Vehicle/Compile/Type/Bidirectional.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Bidirectional.hs
@@ -23,6 +23,7 @@ import Vehicle.Compile.Type.Force (forceHead)
 import Vehicle.Compile.Type.Meta (MetaSet)
 import Vehicle.Compile.Type.Meta.Set qualified as MetaSet
 import Vehicle.Compile.Type.Monad
+import Vehicle.Compile.Type.System (HasTypeSystem (..), TCM)
 import Vehicle.Data.Code.Value
 import Vehicle.Data.Universe (UniverseLevel (..))
 import Prelude hiding (pi)
@@ -37,7 +38,7 @@ import Prelude hiding (pi)
 -- | Type checking monad with additional bound context for the bidirectional
 -- type-checking pass.
 type MonadBidirectional builtin m =
-  ( MonadTypeChecker builtin m,
+  ( TCM builtin m,
     MonadBoundContext (Type builtin) m,
     MonadReader Relevance m
   )
@@ -60,7 +61,7 @@ runMonadBidirectional ctx relevance x =
 -- version of the expression with the necessary implicit and instance arguments
 -- inserted.
 checkExprType ::
-  (MonadTypeChecker builtin m) =>
+  (TCM builtin m) =>
   BoundCtx (Type builtin) ->
   Relevance ->
   Type builtin ->
@@ -144,7 +145,7 @@ viaInfer expectedType expr = do
 -- Inference
 
 inferExprType ::
-  (MonadTypeChecker builtin m) =>
+  (TCM builtin m) =>
   BoundCtx (Type builtin) ->
   Relevance ->
   Expr builtin ->
@@ -310,7 +311,7 @@ type ArgInsertionProblemSolution builtin =
 
 -- | Deals with insertion of missing implicits and instance arguments
 solveArgInsertionProblem ::
-  (MonadTypeChecker builtin m) =>
+  (TCM builtin m) =>
   BoundCtx (Type builtin) ->
   ArgInsertionProblem builtin ->
   m (ArgInsertionProblemSolution builtin)
@@ -353,7 +354,7 @@ forceApplicationHeadType ctx typ = do
   return (quote (provenanceOf typ) (boundCtxLv ctx) forcedType, blockingMetas)
 
 checkArgsAgainstPiType ::
-  (MonadTypeChecker builtin m) =>
+  (TCM builtin m) =>
   BoundCtx (Type builtin) ->
   ArgInsertionProblem builtin ->
   Binder builtin ->
@@ -406,7 +407,7 @@ argInsertionProblemSolved problem@ArgInsertionProblem {..} =
   return $ Right (solutionSoFar problem, currentExpectedType)
 
 instantiateArgForNonExplicitBinder ::
-  (MonadTypeChecker builtin m) =>
+  (TCM builtin m) =>
   BoundCtx (Type builtin) ->
   Provenance ->
   (Expr builtin, [Arg builtin], Type builtin) ->
@@ -426,7 +427,7 @@ instantiateArgForNonExplicitBinder boundCtx p (fun, funArgs, funType) binder = d
                   checkedInstanceOpType = funType,
                   checkedInstanceType = binderType
                 }
-      createFreshInstanceConstraint boundCtx (provenanceOf fun) origin (relevanceOf binder) binderType
+      createFreshInstanceConstraint (isAuxiliaryConstraint binderType) boundCtx (provenanceOf fun) origin (relevanceOf binder) binderType
   return $ Arg p (markInserted $ visibilityOf binder) (relevanceOf binder) checkedExpr
 
 --------------------------------------------------------------------------------
diff --git a/vehicle/src/Vehicle/Compile/Type/Constraint/ApplicationSolver.hs b/vehicle/src/Vehicle/Compile/Type/Constraint/ApplicationSolver.hs
index fd017dade..577ce3813 100644
--- a/vehicle/src/Vehicle/Compile/Type/Constraint/ApplicationSolver.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Constraint/ApplicationSolver.hs
@@ -8,21 +8,20 @@ import Vehicle.Compile.Prelude
 import Vehicle.Compile.Type.Bidirectional (solveArgInsertionProblem)
 import Vehicle.Compile.Type.Constraint.Core
 import Vehicle.Compile.Type.Core
-import Vehicle.Compile.Type.Meta (MetaSet)
 import Vehicle.Compile.Type.Monad.Class
 import Vehicle.Compile.Type.System
 
 -- | Attempts to solve as many type-class constraints as possible. Takes in
 -- the set of meta-variables solved since the solver was last run and outputs
 -- the set of meta-variables solved during this run.
-runApplicationSolver :: forall builtin m. (TCM builtin m) => Proxy builtin -> MetaSet -> m ()
-runApplicationSolver _ metasSolved = do
+runApplicationSolver :: (TCM builtin m) => Proxy builtin -> m ()
+runApplicationSolver proxy = do
   logCompilerPass MaxDetail ("application solver run" <> line) $
-    runConstraintSolver @builtin
+    runConstraintSolver
+      proxy
       getActiveApplicationConstraints
       setApplicationConstraints
       solveApplicationConstraint
-      metasSolved
 
 solveApplicationConstraint ::
   (TCM builtin m) =>
diff --git a/vehicle/src/Vehicle/Compile/Type/Constraint/Core.hs b/vehicle/src/Vehicle/Compile/Type/Constraint/Core.hs
index a8e2333a8..2bdbb0d15 100644
--- a/vehicle/src/Vehicle/Compile/Type/Constraint/Core.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Constraint/Core.hs
@@ -8,12 +8,11 @@ module Vehicle.Compile.Type.Constraint.Core
     createInstanceUnification,
     createSubInstance,
     mkCandidate,
+    AuxiliaryConstraintProgress (..),
   )
 where
 
-import Control.Monad (forM_)
 import Data.Data (Proxy (..))
-import Data.List (partition)
 import Vehicle.Compile.Error
 import Vehicle.Compile.Normalise.Quote (Quote (..))
 import Vehicle.Compile.Prelude
@@ -21,7 +20,8 @@ import Vehicle.Compile.Print
 import Vehicle.Compile.Type.Core
 import Vehicle.Compile.Type.Meta (MetaSet)
 import Vehicle.Compile.Type.Meta.Set qualified as MetaSet
-import Vehicle.Compile.Type.Monad (MonadTypeChecker, copyContext, freshMetaIdAndExpr, trackSolvedMetas)
+import Vehicle.Compile.Type.Monad (MonadTypeChecker, copyContext, freshMetaIdAndExpr)
+import Vehicle.Compile.Type.Monad.Class (getIsUnblockedFn)
 import Vehicle.Data.Code.Value
 import Vehicle.Data.DSL
 
@@ -31,44 +31,67 @@ import Vehicle.Data.DSL
 runConstraintSolver ::
   forall builtin m constraint.
   (MonadTypeChecker builtin m, PrettyExternal (Contextualised constraint (ConstraintContext builtin))) =>
+  Proxy builtin ->
   m [Contextualised constraint (ConstraintContext builtin)] ->
   ([Contextualised constraint (ConstraintContext builtin)] -> m ()) ->
   (Contextualised constraint (ConstraintContext builtin) -> m ()) ->
-  MetaSet ->
   m ()
-runConstraintSolver getConstraints setConstraints attemptToSolveConstraint = loop 0
+runConstraintSolver _ getConstraints setConstraints attemptToSolveConstraint = loop 0
   where
-    loop :: Int -> MetaSet -> m ()
-    loop loopNumber recentMetasSolved = do
+    loop :: Int -> m ()
+    loop loopNumber = do
       unsolvedConstraints <- getConstraints
 
       if null unsolvedConstraints
         then return mempty
         else do
-          let isUnblocked = not . constraintIsBlocked recentMetasSolved
-          let (unblockedConstraints, blockedConstraints) = partition isUnblocked unsolvedConstraints
+          isUnblocked <- getIsUnblockedFn
 
-          if null unblockedConstraints
-            then return mempty
-            else do
+          case findFirstConstraint isUnblocked unsolvedConstraints of
+            Nothing -> return mempty
+            Just (unblockedConstraint, remainingConstraints) -> do
               -- We have made useful progress so start a new pass
-              setConstraints blockedConstraints
+              setConstraints remainingConstraints
 
-              solvedMetas <- trackSolvedMetas (Proxy @builtin) $ do
-                forM_ unblockedConstraints $ \constraint -> do
-                  logCompilerSection MaxDetail ("trying:" <+> prettyExternal constraint) $ do
-                    attemptToSolveConstraint constraint
+              logCompilerSection MaxDetail ("trying:" <+> prettyExternal unblockedConstraint) $
+                attemptToSolveConstraint unblockedConstraint
 
-              loop (loopNumber + 1) solvedMetas
+              loop (loopNumber + 1)
 
-blockOn :: (MonadCompile m) => [MetaID] -> Maybe (m (ConstraintProgress builtin))
+-- | Find the first constraint satisfying `p` appending all the constraints that don't satisfy it to
+-- the end of the list, so we don't search through them again immediately next time.
+findFirstConstraint :: forall a. (a -> Bool) -> [a] -> Maybe (a, [a])
+findFirstConstraint p xs = (\(found, seen, unseen) -> (found, unseen <> seen)) <$> go xs
+  where
+    go :: [a] -> Maybe (a, [a], [a])
+    go = \case
+      [] -> Nothing
+      c : cs
+        | p c -> Just (c, [], cs)
+        | otherwise -> fmap (\(found, seen, unseen) -> (found, c : seen, unseen)) (go cs)
+
+data AuxiliaryConstraintProgress builtin
+  = Stuck MetaSet
+  | Progress [WithContext (UnificationConstraint builtin)] [WithContext (InstanceConstraint builtin)]
+  deriving (Show)
+
+instance Semigroup (AuxiliaryConstraintProgress builtin) where
+  Stuck m1 <> Stuck m2 = Stuck (m1 <> m2)
+  Stuck {} <> x@Progress {} = x
+  x@Progress {} <> Stuck {} = x
+  Progress u1 r1 <> Progress u2 r2 = Progress (u1 <> u2) (r1 <> r2)
+
+blockOn :: (MonadCompile m) => [MetaID] -> Maybe (m (AuxiliaryConstraintProgress builtin))
 blockOn metas = Just $ do
   logDebug MaxDetail $ "stuck-on metas" <+> pretty metas
   return $ Stuck $ MetaSet.fromList metas
 
-malformedConstraintError :: (PrintableBuiltin builtin, MonadCompile m) => WithContext (InstanceConstraint builtin) -> m a
+malformedConstraintError ::
+  (PrintableBuiltin builtin, MonadCompile m) =>
+  WithContext (InstanceConstraint builtin) ->
+  m a
 malformedConstraintError c =
-  compilerDeveloperError $ "Malformed type-class constraint:" <+> prettyVerbose c
+  compilerDeveloperError $ "Malformed auxiliary constraint:" <+> prettyVerbose c
 
 -- | Create a new unification constraint as a subgoal of an existing instance constraint.
 createInstanceUnification ::
diff --git a/vehicle/src/Vehicle/Compile/Type/Constraint/IndexSolver.hs b/vehicle/src/Vehicle/Compile/Type/Constraint/IndexSolver.hs
index 3f2260bca..303b583d0 100644
--- a/vehicle/src/Vehicle/Compile/Type/Constraint/IndexSolver.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Constraint/IndexSolver.hs
@@ -39,7 +39,7 @@ solveIndexConstraint constraint = do
           solveMeta meta solution (boundContext ctx)
         Just metas -> do
           let blockedConstraint = blockConstraintOn normConstraint metas
-          addInstanceConstraints [blockedConstraint]
+          addAuxiliaryInstanceConstraints [blockedConstraint]
     _ -> compilerDeveloperError $ "Malformed instance goal" <+> prettyFriendly normConstraint
 
 -- | Function signature for constraints solved by type class resolution.
@@ -116,15 +116,14 @@ solveDefaultIndexConstraint ::
   (MonadTypeChecker Builtin m) =>
   WithContext (InstanceConstraint Builtin) ->
   m Bool
-solveDefaultIndexConstraint constraint = do
-  let goal = parseInstanceGoal constraint
-  case (goalHead goal, goalSpine goal) of
-    (NatInDomainConstraint, [n, argExpr -> IIndexType _ size]) -> do
+solveDefaultIndexConstraint (WithContext constraint ctx) = do
+  case instanceGoal constraint of
+    (VBuiltin NatInDomainConstraint [n, argExpr -> IIndexType _ size]) -> do
       let succN = case argExpr n of
             INatLiteral p x -> INatLiteral p (x + 1)
             n' -> IAdd AddNat n' (INatLiteral mempty 1)
 
-      let constraintInfo = (contextOf constraint, instanceOrigin $ objectIn constraint)
+      let constraintInfo = (ctx, instanceOrigin constraint)
       newSizeConstraint <- createInstanceUnification constraintInfo size succN
       addUnificationConstraints [newSizeConstraint]
       return True
diff --git a/vehicle/src/Vehicle/Compile/Type/Constraint/InstanceDefaultSolver.hs b/vehicle/src/Vehicle/Compile/Type/Constraint/InstanceDefaultSolver.hs
index 6e5424127..25a8ce93a 100644
--- a/vehicle/src/Vehicle/Compile/Type/Constraint/InstanceDefaultSolver.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Constraint/InstanceDefaultSolver.hs
@@ -1,5 +1,6 @@
 module Vehicle.Compile.Type.Constraint.InstanceDefaultSolver
-  ( addNewConstraintUsingDefaults,
+  ( addNewInstanceConstraintUsingDefaults,
+    getDefaultableConstraints,
   )
 where
 
@@ -7,9 +8,8 @@ import Control.Monad (filterM)
 import Data.Hashable (Hashable)
 import Data.Maybe (mapMaybe)
 import Data.Proxy (Proxy (..))
-import Vehicle.Compile.Error (MonadCompile)
 import Vehicle.Compile.Prelude
-import Vehicle.Compile.Print (PrintableBuiltin, prettyVerbose)
+import Vehicle.Compile.Print (In, NoCtx, PrettyVerbose, PrintableBuiltin, prettyVerbose)
 import Vehicle.Compile.Type.Constraint.Core (parseInstanceGoal)
 import Vehicle.Compile.Type.Constraint.InstanceSolver (acceptCandidate)
 import Vehicle.Compile.Type.Core
@@ -32,44 +32,29 @@ instance (PrintableBuiltin builtin) => Pretty (DefaultCandidate builtin) where
   pretty (DefaultCandidate (constraint, _, candidate)) =
     prettyVerbose constraint <+> "~" <+> prettyVerbose (candidateExpr candidate)
 
--- | Tries to add new unification constraints using default values.
-addNewConstraintUsingDefaults ::
+addNewInstanceConstraintUsingDefaults ::
+  forall builtin m.
   (MonadTypeChecker builtin m, Hashable builtin) =>
-  ([WithContext (InstanceConstraint builtin)] -> m Bool) ->
-  InstanceDatabase builtin ->
   Maybe (Decl builtin) ->
   m Bool
-addNewConstraintUsingDefaults handleNonStandardConstraints instanceDatabase maybeDecl = do
-  logDebug MaxDetail $ "Temporarily stuck" <> line
-
-  logCompilerPass
-    MidDetail
-    "trying to generate a new constraint using instance defaults"
-    $ do
-      -- Calculate the set of candidate constraints
-      defaultableConstraints <- getDefaultableConstraints maybeDecl
-      logDebug MaxDetail $
-        "Suitable instance constraints:"
-          <> line
-          <> indent 2 (prettyVerbose defaultableConstraints)
-          <> line
-
-      result <- chooseDefaultConstraint instanceDatabase defaultableConstraints
-      case result of
-        Just candidate -> do
-          acceptDefaultCandidate candidate
-          return True
-        Nothing ->
-          handleNonStandardConstraints defaultableConstraints
+addNewInstanceConstraintUsingDefaults maybeDecl = do
+  instanceConstraints <- getActiveInstanceConstraints @builtin
+  defaultableConstraints <- getDefaultableConstraints maybeDecl instanceConstraints
+  result <- chooseDefaultConstraint defaultableConstraints
+  case result of
+    Just candidate -> do
+      acceptDefaultCandidate candidate
+      return True
+    Nothing -> return False
 
 getDefaultableConstraints ::
-  forall builtin m.
-  (MonadInstanceDefault builtin m) =>
+  forall constraint ctx builtin m.
+  (MonadInstanceDefault builtin m, HasMetas constraint, PrettyVerbose (Contextualised constraint ctx `In` NoCtx)) =>
   Maybe (Decl builtin) ->
-  m [WithContext (InstanceConstraint builtin)]
-getDefaultableConstraints maybeDecl = do
-  instanceConstraints <- getActiveInstanceConstraints
-  case maybeDecl of
+  [Contextualised constraint ctx] ->
+  m [Contextualised constraint ctx]
+getDefaultableConstraints maybeDecl possibleConstraints = do
+  result <- case maybeDecl of
     Just decl | not (isAbstractDecl decl) -> do
       -- We only want to generate default solutions for constraints
       -- that *don't* appear in the type of the declaration, as those will be
@@ -83,18 +68,26 @@ getDefaultableConstraints maybeDecl = do
         unsolvedMetasInTypeDoc <- prettyMetas (Proxy @builtin) typeMetas
         return $ "Metas transitively related to type-signature:" <+> unsolvedMetasInTypeDoc
 
-      flip filterM instanceConstraints $ \tc -> do
+      flip filterM possibleConstraints $ \tc -> do
         constraintMetas <- metasIn (objectIn tc)
         return $ MetaSet.disjoint constraintMetas typeMetas
-    _ -> return instanceConstraints
+    _ -> return possibleConstraints
+
+  logDebug MaxDetail $
+    "Suitable defaultable constraints:"
+      <> line
+      <> indent 2 (prettyVerbose result)
+      <> line
+
+  return result
 
 chooseDefaultConstraint ::
   forall builtin m.
-  (MonadCompile m, PrintableBuiltin builtin, Hashable builtin) =>
-  InstanceDatabase builtin ->
+  (MonadTypeChecker builtin m) =>
   [WithContext (InstanceConstraint builtin)] ->
   m (Maybe (DefaultCandidate builtin))
-chooseDefaultConstraint instanceDatabase constraints = do
+chooseDefaultConstraint constraints = do
+  instanceDatabase <- getInstanceCandidates
   let defaults = mapMaybe (findDefault instanceDatabase) constraints
   case defaults of
     [] -> do
diff --git a/vehicle/src/Vehicle/Compile/Type/Constraint/InstanceSolver.hs b/vehicle/src/Vehicle/Compile/Type/Constraint/InstanceSolver.hs
index 0d46d4d55..b0c172de4 100644
--- a/vehicle/src/Vehicle/Compile/Type/Constraint/InstanceSolver.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Constraint/InstanceSolver.hs
@@ -1,5 +1,5 @@
 module Vehicle.Compile.Type.Constraint.InstanceSolver
-  ( solveInstanceConstraint,
+  ( runInstanceSolver,
     acceptCandidate,
   )
 where
@@ -26,19 +26,21 @@ import Vehicle.Data.DeBruijn (dbLevelToIndex)
 --------------------------------------------------------------------------------
 -- Public interface
 
-solveInstanceConstraint ::
-  forall builtin m.
-  (Hashable builtin, MonadInstance builtin m) =>
-  InstanceDatabase builtin ->
-  WithContext (InstanceConstraint builtin) ->
+-- | Attempts to solve as many type-class constraints as possible. Takes in
+-- the set of meta-variables solved since the solver was last run and outputs
+-- the set of meta-variables solved during this run.
+runInstanceSolver ::
+  (MonadInstance builtin m) =>
+  Proxy builtin ->
+  InstanceSearchDepth ->
   m ()
-solveInstanceConstraint database constraint = do
-  normConstraint <- substMetas constraint
-  logDebug MaxDetail $ "Forced:" <+> prettyFriendly normConstraint
-
-  let goal = parseInstanceGoal normConstraint
-  let candidates = lookupInstances database goal
-  solveInstanceGoal normConstraint candidates goal
+runInstanceSolver proxy depth = do
+  logCompilerPass MaxDetail ("instance solver run" <> line) $
+    runConstraintSolver
+      proxy
+      getActiveInstanceConstraints
+      setInstanceConstraints
+      (solveInstanceConstraint depth)
 
 --------------------------------------------------------------------------------
 -- Algorithm
@@ -51,14 +53,30 @@ type MonadInstance builtin m =
 -- The algorithm for this is taken from
 -- https://agda.readthedocs.io/en/v2.6.2.2/language/instance-arguments.html#instance-resolution
 
+solveInstanceConstraint ::
+  forall builtin m.
+  (Hashable builtin, MonadInstance builtin m) =>
+  InstanceSearchDepth ->
+  WithContext (InstanceConstraint builtin) ->
+  m ()
+solveInstanceConstraint depth constraint = do
+  normConstraint <- substMetas constraint
+  logDebug MaxDetail $ "Forced:" <+> prettyFriendly normConstraint
+
+  let goal = parseInstanceGoal normConstraint
+  database <- getInstanceCandidates
+  let candidates = lookupInstances database goal
+  solveInstanceGoal depth normConstraint candidates goal
+
 solveInstanceGoal ::
   forall builtin m.
   (MonadInstance builtin m) =>
+  InstanceSearchDepth ->
   WithContext (InstanceConstraint builtin) ->
   [InstanceCandidate builtin] ->
   InstanceGoal builtin ->
   m ()
-solveInstanceGoal constraint rawBuiltinCandidates goal = do
+solveInstanceGoal depth constraint rawBuiltinCandidates goal = do
   let boundCtx = boundContext $ contextOf constraint
   candidatesInBoundCtx <- findCandidatesInBoundCtx goal boundCtx
   -- The previously declared candidates have access to the entire bound context
@@ -75,10 +93,11 @@ solveInstanceGoal constraint rawBuiltinCandidates goal = do
       <> line
       <> indent 2 (list (fmap prettyCandidate candidatesInBoundCtx))
       <> line
+      <> "Depth:" <+> pretty depth
 
   -- Try all candidates
   (unsuccessfulCandidates, successfulCandidates) <-
-    partitionEithers <$> traverse (checkCandidate constraint goal) allCandidates
+    partitionEithers <$> traverse (checkCandidate depth constraint goal) allCandidates
 
   case successfulCandidates of
     -- If there is a single valid candidate then we adopt the resulting state
@@ -131,17 +150,24 @@ findCandidatesInBoundCtx goal ctx = go ctx
 checkCandidate ::
   forall builtin m.
   (MonadInstance builtin m) =>
+  InstanceSearchDepth ->
   WithContext (InstanceConstraint builtin) ->
   InstanceGoal builtin ->
   WithContext (InstanceCandidate builtin) ->
   m (Either (WithContext (InstanceCandidate builtin), UnAnnDoc) (WithContext (InstanceCandidate builtin), TypeCheckerState builtin))
-checkCandidate constraint goal candidate = do
+checkCandidate depth constraint goal candidate = do
   let candidateDoc = squotes (prettyCandidate candidate)
   logCompilerPass MaxDetail ("trying candidate instance" <+> candidateDoc) $ do
     result <- runTypeCheckerTHypothetically $ do
       logCompilerSection MaxDetail "hypothetically accepting candidate" $
         acceptCandidate constraint goal candidate
-      runUnificationSolver (Proxy @builtin) mempty
+
+      -- Run the solvers to check for conflicts
+      let proxy = Proxy @builtin
+      runUnificationSolver proxy
+      if depth == 0
+        then return mempty
+        else runInstanceSolver proxy (depth - 1)
 
     case result of
       Left err -> do
diff --git a/vehicle/src/Vehicle/Compile/Type/Constraint/LinearitySolver.hs b/vehicle/src/Vehicle/Compile/Type/Constraint/LinearitySolver.hs
index 97d6fd743..dda3edfc9 100644
--- a/vehicle/src/Vehicle/Compile/Type/Constraint/LinearitySolver.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Constraint/LinearitySolver.hs
@@ -11,7 +11,7 @@ import Vehicle.Compile.Print (prettyFriendly)
 import Vehicle.Compile.Type.Constraint.Core
 import Vehicle.Compile.Type.Core
 import Vehicle.Compile.Type.Monad (MonadTypeChecker, addUnificationConstraints)
-import Vehicle.Compile.Type.Monad.Class (addInstanceConstraints, solveMeta, substMetas)
+import Vehicle.Compile.Type.Monad.Class (addAuxiliaryInstanceConstraints, solveMeta, substMetas)
 import Vehicle.Data.Builtin.Core
 import Vehicle.Data.Builtin.Linearity
 import Vehicle.Data.Code.Interface
@@ -19,10 +19,9 @@ import Vehicle.Data.Code.Value
 
 solveLinearityConstraint ::
   (MonadLinearitySolver m) =>
-  InstanceDatabase LinearityBuiltin ->
   WithContext (InstanceConstraint LinearityBuiltin) ->
   m ()
-solveLinearityConstraint _ (WithContext constraint ctx) = do
+solveLinearityConstraint (WithContext constraint ctx) = do
   normConstraint@(Resolve origin _ _ expr) <- substMetas constraint
   logDebug MaxDetail $ "Forced:" <+> prettyFriendly (WithContext normConstraint ctx)
 
@@ -45,7 +44,7 @@ type LinearitySolver =
   (MonadLinearitySolver m) =>
   InstanceConstraintInfo LinearityBuiltin ->
   [VType LinearityBuiltin] ->
-  Maybe (m (ConstraintProgress LinearityBuiltin))
+  Maybe (m (AuxiliaryConstraintProgress LinearityBuiltin))
 
 solve :: LinearityRelation -> LinearitySolver
 solve = \case
@@ -147,14 +146,14 @@ powLinearityOp p l1 l2 = case (l1, l2) of
 handleConstraintProgress ::
   (MonadTypeChecker LinearityBuiltin m) =>
   WithContext (InstanceConstraint LinearityBuiltin) ->
-  ConstraintProgress LinearityBuiltin ->
+  AuxiliaryConstraintProgress LinearityBuiltin ->
   m ()
 handleConstraintProgress originalConstraint@(WithContext (Resolve _ m _ _) ctx) = \case
-  Stuck metas -> addInstanceConstraints [blockConstraintOn originalConstraint metas]
-  Progress newUnificationConstraints newInstanceConstraints -> do
+  Stuck metas -> addAuxiliaryInstanceConstraints [blockConstraintOn originalConstraint metas]
+  Progress newUnificationConstraints newAuxiliaryConstraints -> do
     solveMeta m (IUnitLiteral (provenanceOf ctx)) (boundContext ctx)
     addUnificationConstraints newUnificationConstraints
-    addInstanceConstraints newInstanceConstraints
+    addAuxiliaryInstanceConstraints newAuxiliaryConstraints
 
 getTypeClass :: (MonadCompile m) => Value LinearityBuiltin -> m (LinearityRelation, Spine LinearityBuiltin)
 getTypeClass = \case
diff --git a/vehicle/src/Vehicle/Compile/Type/Constraint/PolaritySolver.hs b/vehicle/src/Vehicle/Compile/Type/Constraint/PolaritySolver.hs
index 1130cf79e..21e9a3e00 100644
--- a/vehicle/src/Vehicle/Compile/Type/Constraint/PolaritySolver.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Constraint/PolaritySolver.hs
@@ -12,7 +12,7 @@ import Vehicle.Compile.Print (prettyFriendly)
 import Vehicle.Compile.Type.Constraint.Core
 import Vehicle.Compile.Type.Core
 import Vehicle.Compile.Type.Monad
-import Vehicle.Compile.Type.Monad.Class (addInstanceConstraints)
+import Vehicle.Compile.Type.Monad.Class (addAuxiliaryInstanceConstraints)
 import Vehicle.Data.Builtin.Core
 import Vehicle.Data.Builtin.Polarity
 import Vehicle.Data.Code.Interface
@@ -20,10 +20,9 @@ import Vehicle.Data.Code.Value
 
 solvePolarityConstraint ::
   (MonadPolaritySolver m) =>
-  InstanceDatabase PolarityBuiltin ->
   WithContext (InstanceConstraint PolarityBuiltin) ->
   m ()
-solvePolarityConstraint _ (WithContext constraint ctx) = do
+solvePolarityConstraint (WithContext constraint ctx) = do
   normConstraint@(Resolve origin _ _ expr) <- substMetas constraint
   logDebug MaxDetail $ "Forced:" <+> prettyFriendly (WithContext normConstraint ctx)
 
@@ -44,7 +43,7 @@ type PolaritySolver =
   (MonadPolaritySolver m) =>
   InstanceConstraintInfo PolarityBuiltin ->
   [VType PolarityBuiltin] ->
-  Maybe (m (ConstraintProgress PolarityBuiltin))
+  Maybe (m (AuxiliaryConstraintProgress PolarityBuiltin))
 
 solve :: PolarityRelation -> PolaritySolver
 solve = \case
@@ -232,14 +231,14 @@ implPolarityOp p pol1 pol2 =
 handleConstraintProgress ::
   (MonadTypeChecker PolarityBuiltin m) =>
   WithContext (InstanceConstraint PolarityBuiltin) ->
-  ConstraintProgress PolarityBuiltin ->
+  AuxiliaryConstraintProgress PolarityBuiltin ->
   m ()
 handleConstraintProgress originalConstraint@(WithContext (Resolve _ m _ _) ctx) = \case
-  Stuck metas -> addInstanceConstraints [blockConstraintOn originalConstraint metas]
-  Progress newUnificationConstraints newInstanceConstraints -> do
+  Stuck metas -> addAuxiliaryInstanceConstraints [blockConstraintOn originalConstraint metas]
+  Progress newUnificationConstraints newAuxiliaryConstraints -> do
     solveMeta m (IUnitLiteral (provenanceOf ctx)) (boundContext ctx)
     addUnificationConstraints newUnificationConstraints
-    addInstanceConstraints newInstanceConstraints
+    addAuxiliaryInstanceConstraints newAuxiliaryConstraints
 
 getTypeClass :: (MonadCompile m) => Value PolarityBuiltin -> m (PolarityRelation, Spine PolarityBuiltin)
 getTypeClass = \case
diff --git a/vehicle/src/Vehicle/Compile/Type/Constraint/UnificationSolver.hs b/vehicle/src/Vehicle/Compile/Type/Constraint/UnificationSolver.hs
index a20653e3e..0796a5702 100644
--- a/vehicle/src/Vehicle/Compile/Type/Constraint/UnificationSolver.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Constraint/UnificationSolver.hs
@@ -40,14 +40,14 @@ import Vehicle.Data.DeBruijn
 -- | Attempts to solve as many unification constraints as possible. Takes in
 -- the set of meta-variables solved since unification was last run and outputs
 -- the set of meta-variables solved during this run.
-runUnificationSolver :: forall builtin m. (MonadTypeChecker builtin m) => Proxy builtin -> MetaSet -> m ()
-runUnificationSolver _ metasSolved =
+runUnificationSolver :: (MonadTypeChecker builtin m) => Proxy builtin -> m ()
+runUnificationSolver proxy =
   logCompilerPass MaxDetail "unification solver run" $
-    runConstraintSolver @builtin
+    runConstraintSolver
+      proxy
       getActiveUnificationConstraints
       setUnificationConstraints
       solveUnificationConstraint
-      metasSolved
 
 --------------------------------------------------------------------------------
 -- Unification algorithm
diff --git a/vehicle/src/Vehicle/Compile/Type/Core.hs b/vehicle/src/Vehicle/Compile/Type/Core.hs
index a1ff05976..092353bd9 100644
--- a/vehicle/src/Vehicle/Compile/Type/Core.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Core.hs
@@ -183,6 +183,8 @@ type InstanceConstraintInfo builtin =
     InstanceConstraintOrigin builtin
   )
 
+type InstanceSearchDepth = Int
+
 -- | Stores the list of instance candidates currently in scope.
 -- We use a HashMap rather than an ordinary Map as not all builtins may be
 -- totally ordered (e.g. PolarityBuiltin and LinearityBuiltin)
@@ -221,7 +223,6 @@ data UnificationConstraintOrigin builtin
   = CheckingExprType (CheckingExprType builtin)
   | CheckingBinderType (CheckingBinderType builtin)
   | CheckingInstanceType (InstanceConstraintOrigin builtin)
-  | CheckingAuxiliary
   deriving (Show)
 
 -- | A constraint representing that a pair of expressions should be equal
@@ -244,7 +245,7 @@ data Constraint builtin
     UnificationConstraint (UnificationConstraint builtin)
   | -- | Represents that the provided type must have the required functionality
     InstanceConstraint (InstanceConstraint builtin)
-  | -- | Represents that
+  | -- | Represents an implicit/instance application argument insertion problem
     ApplicationConstraint (ApplicationConstraint builtin)
   deriving (Show)
 
@@ -252,11 +253,6 @@ type instance
   WithContext (Constraint builtin) =
     Contextualised (Constraint builtin) (ConstraintContext builtin)
 
-getTypeClassConstraint :: WithContext (Constraint builtin) -> Maybe (WithContext (InstanceConstraint builtin))
-getTypeClassConstraint (WithContext constraint ctx) = case constraint of
-  InstanceConstraint tc -> Just (WithContext tc ctx)
-  _ -> Nothing
-
 blockConstraintOn ::
   Contextualised c (ConstraintContext builtin) ->
   MetaSet ->
@@ -269,20 +265,6 @@ isBlocked solvedMetas ctx = isStillBlocked solvedMetas (blockedBy ctx)
 constraintIsBlocked :: MetaSet -> Contextualised c (ConstraintContext builtin) -> Bool
 constraintIsBlocked solvedMetas c = isBlocked solvedMetas (contextOf c)
 
---------------------------------------------------------------------------------
--- Progress in solving meta-variable constraints
-
-data ConstraintProgress builtin
-  = Stuck MetaSet
-  | Progress [WithContext (UnificationConstraint builtin)] [WithContext (InstanceConstraint builtin)]
-  deriving (Show)
-
-instance Semigroup (ConstraintProgress builtin) where
-  Stuck m1 <> Stuck m2 = Stuck (m1 <> m2)
-  Stuck {} <> x@Progress {} = x
-  x@Progress {} <> Stuck {} = x
-  Progress u1 r1 <> Progress u2 r2 = Progress (u1 <> u2) (r1 <> r2)
-
 --------------------------------------------------------------------------------
 -- Restrictions on decl types
 --------------------------------------------------------------------------------
diff --git a/vehicle/src/Vehicle/Compile/Type/Generalise.hs b/vehicle/src/Vehicle/Compile/Type/Generalise.hs
index ca11fd4df..c4fe896cc 100644
--- a/vehicle/src/Vehicle/Compile/Type/Generalise.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Generalise.hs
@@ -5,8 +5,9 @@ module Vehicle.Compile.Type.Generalise
 where
 
 import Control.Monad (foldM, forM)
+import Control.Monad.Except (MonadError (..))
 import Data.Data (Proxy (..))
-import Data.List.NonEmpty ((<|))
+import Data.List.NonEmpty (NonEmpty (..), (<|))
 import Data.Maybe (fromMaybe)
 import Vehicle.Compile.Context.Bound
 import Vehicle.Compile.Error
@@ -17,6 +18,7 @@ import Vehicle.Compile.Type.Core
 import Vehicle.Compile.Type.Meta
 import Vehicle.Compile.Type.Meta.Set qualified as MetaSet
 import Vehicle.Compile.Type.Monad
+import Vehicle.Compile.Type.Monad.Class (getActiveAuxiliaryInstanceConstraints, setAuxiliaryInstanceConstraints)
 import Vehicle.Data.DeBruijn
 
 --------------------------------------------------------------------------------
@@ -26,18 +28,29 @@ import Vehicle.Data.DeBruijn
 -- metas that occur in the type of the declaration. It then appends these
 -- constraints as instance arguments to the declaration.
 generaliseOverUnsolvedConstraints ::
+  forall builtin m.
   (MonadTypeChecker builtin m) =>
   Decl builtin ->
   m (Decl builtin)
 generaliseOverUnsolvedConstraints decl =
   logCompilerPass MidDetail "generalisation over unsolved type-class constraints" $ do
-    unsolvedTypeClassConstraints <- traverse substMetas =<< getActiveInstanceConstraints
-    unsolvedConstraints <- traverse substMetas =<< getActiveConstraints
+    unsolvedInstanceConstraints <- getActiveInstanceConstraints
+    unsolvedAuxiliaryConstraints <- getActiveAuxiliaryInstanceConstraints
 
-    (generalisedDecl, rejectedTypeClassConstraints) <-
-      foldM (generaliseOverConstraint unsolvedConstraints) (decl, []) unsolvedTypeClassConstraints
-    setInstanceConstraints rejectedTypeClassConstraints
-    return generalisedDecl
+    unsolvedConstraints <- traverse substMetas =<< getActiveConstraints
+    generalisableConstraints <- traverse substMetas (unsolvedInstanceConstraints <> unsolvedAuxiliaryConstraints)
+
+    (generalisedDecl, rejectedGeneralisableConstraints) <-
+      foldM (generaliseOverConstraint unsolvedConstraints) (decl, []) generalisableConstraints
+
+    case rejectedGeneralisableConstraints of
+      (c : cs) -> do
+        let ungeneralisableConstraints = fmap (mapObject InstanceConstraint) (c :| cs)
+        throwError $ TypingError $ UnsolvedConstraints ungeneralisableConstraints
+      [] -> do
+        setInstanceConstraints @builtin mempty
+        setAuxiliaryInstanceConstraints @builtin mempty
+        return generalisedDecl
 
 generaliseOverConstraint ::
   (MonadTypeChecker builtin m) =>
diff --git a/vehicle/src/Vehicle/Compile/Type/Meta/Substitution.hs b/vehicle/src/Vehicle/Compile/Type/Meta/Substitution.hs
index d5549a7a5..1132444e7 100644
--- a/vehicle/src/Vehicle/Compile/Type/Meta/Substitution.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Meta/Substitution.hs
@@ -171,7 +171,6 @@ instance MetaSubstitutable m builtin (UnificationConstraintOrigin builtin) where
     CheckingExprType c -> CheckingExprType <$> subst s c
     CheckingBinderType c -> CheckingBinderType <$> subst s c
     CheckingInstanceType c -> CheckingInstanceType <$> subst s c
-    CheckingAuxiliary -> return CheckingAuxiliary
 
 instance MetaSubstitutable m builtin (CheckingExprType builtin) where
   subst s (CheckingExpr e t1 t2) = CheckingExpr <$> subst s e <*> subst s t1 <*> subst s t2
diff --git a/vehicle/src/Vehicle/Compile/Type/Monad.hs b/vehicle/src/Vehicle/Compile/Type/Monad.hs
index 731d36051..f68bacb1f 100644
--- a/vehicle/src/Vehicle/Compile/Type/Monad.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Monad.hs
@@ -44,6 +44,7 @@ import Vehicle.Compile.Context.Free
 import Vehicle.Compile.Error (CompileError (..))
 import Vehicle.Compile.Normalise.NBE
 import Vehicle.Compile.Prelude
+import Vehicle.Compile.Print (prettyVerbose)
 import Vehicle.Compile.Type.Builtin (TypableBuiltin (..))
 import Vehicle.Compile.Type.Core
 import Vehicle.Compile.Type.Meta (MetaSet)
@@ -121,6 +122,8 @@ createFreshUnificationConstraint p ctx origin expectedType actualType = do
   let env = boundContextToEnv ctx
   normExpectedType <- normaliseInEnv env expectedType
   normActualType <- normaliseInEnv env actualType
+  logDebug MaxDetail $ "Hit1" <+> prettyVerbose normExpectedType
+  logDebug MaxDetail $ "Hit2" <+> prettyVerbose normActualType
   context <- createFreshConstraintCtx p p ctx
   let unification = Unify origin normExpectedType normActualType
   let constraint = WithContext unification context
@@ -151,18 +154,19 @@ createFreshApplicationConstraint ctx problem blockingMetas = do
   addApplicationConstraint blockedConstraint
   return (unnormalised finalExpr, unnormalised finalType)
 
--- | Adds an entirely new type-class constraint (as opposed to one
+-- | Adds an entirely new instance constraint (as opposed to one
 -- derived from another constraint).
 createFreshInstanceConstraint ::
   forall builtin m.
   (MonadTypeChecker builtin m) =>
+  Bool ->
   BoundCtx (Type builtin) ->
   Provenance ->
   InstanceConstraintOrigin builtin ->
   Relevance ->
   Type builtin ->
   m (GluedExpr builtin)
-createFreshInstanceConstraint boundCtx p origin relevance tcExpr = do
+createFreshInstanceConstraint auxiliaryConstraint boundCtx p origin relevance tcExpr = do
   let env = boundContextToEnv boundCtx
   (meta, metaExpr) <- freshMetaIdAndExpr p tcExpr boundCtx
 
@@ -171,6 +175,8 @@ createFreshInstanceConstraint boundCtx p origin relevance tcExpr = do
   nTCExpr <- normaliseInEnv env tcExpr
   let constraint = WithContext (Resolve origin meta relevance nTCExpr) context
 
-  addInstanceConstraints [constraint]
+  if auxiliaryConstraint
+    then addAuxiliaryInstanceConstraints [constraint]
+    else addInstanceConstraints [constraint]
 
   return metaExpr
diff --git a/vehicle/src/Vehicle/Compile/Type/Monad/Class.hs b/vehicle/src/Vehicle/Compile/Type/Monad/Class.hs
index 9b9ed7ca9..55ca9a9a3 100644
--- a/vehicle/src/Vehicle/Compile/Type/Monad/Class.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Monad/Class.hs
@@ -5,6 +5,7 @@ import Control.Monad.Reader (ReaderT (..))
 import Control.Monad.State (StateT (..))
 import Control.Monad.Trans.Class (lift)
 import Control.Monad.Writer (WriterT (..))
+import Data.Hashable (Hashable)
 import Data.Maybe (fromMaybe)
 import Data.Proxy (Proxy (..))
 import Prettyprinter (fill)
@@ -73,6 +74,8 @@ data TypeCheckerState builtin = TypeCheckerState
     applicationConstraints :: [WithContext (ApplicationConstraint builtin)],
     unificationConstraints :: [WithContext (UnificationConstraint builtin)],
     instanceConstraints :: [WithContext (InstanceConstraint builtin)],
+    -- | Instance constraints not solvable by instance class resolution
+    auxiliaryInstanceConstraints :: [WithContext (InstanceConstraint builtin)],
     freshNameState :: FreshNameState,
     solvedMetaState :: SolvedMetaState,
     nextConstraintID :: ConstraintID
@@ -86,6 +89,7 @@ emptyTypeCheckerState =
       applicationConstraints = mempty,
       unificationConstraints = mempty,
       instanceConstraints = mempty,
+      auxiliaryInstanceConstraints = mempty,
       freshNameState = 0,
       solvedMetaState = SolvedMetaState mempty,
       nextConstraintID = 0
@@ -95,7 +99,7 @@ emptyTypeCheckerState =
 -- The type-checking monad class
 
 -- | The type-checking monad.
-class (MonadCompile m, MonadFreeContext builtin m, NormalisableBuiltin builtin, Eq builtin, TypableBuiltin builtin) => MonadTypeChecker builtin m where
+class (MonadCompile m, MonadFreeContext builtin m, NormalisableBuiltin builtin, Eq builtin, Hashable builtin, TypableBuiltin builtin) => MonadTypeChecker builtin m where
   getMetaState :: m (TypeCheckerState builtin)
   modifyMetaCtx :: (TypeCheckerState builtin -> TypeCheckerState builtin) -> m ()
   getFreshName :: Type builtin -> m Name
@@ -166,6 +170,15 @@ getMetaSubstitution ::
   m (MetaSubstitution builtin)
 getMetaSubstitution _ = currentSubstitution <$> getMetaState
 
+getIsUnblockedFn ::
+  forall builtin m constraint.
+  (MonadTypeChecker builtin m) =>
+  m (Contextualised constraint (ConstraintContext builtin) -> Bool)
+getIsUnblockedFn = do
+  metasSolved <- MetaMap.keys <$> getMetaSubstitution (Proxy @builtin)
+  let isUnblocked = not . constraintIsBlocked metasSolved
+  return isUnblocked
+
 substMetas ::
   forall builtin m a.
   (MonadTypeChecker builtin m, MetaSubstitutable m builtin a) =>
@@ -413,9 +426,10 @@ createFreshConstraintCtx originalProvenance creationProvenance ctx = do
 getActiveConstraints :: (MonadTypeChecker builtin m) => m [WithContext (Constraint builtin)]
 getActiveConstraints = do
   us <- fmap (mapObject UnificationConstraint) <$> getActiveUnificationConstraints
-  ts <- fmap (mapObject InstanceConstraint) <$> getActiveInstanceConstraints
   as <- fmap (mapObject ApplicationConstraint) <$> getActiveApplicationConstraints
-  return $ us <> ts <> as
+  ts <- fmap (mapObject InstanceConstraint) <$> getActiveInstanceConstraints
+  xs <- fmap (mapObject InstanceConstraint) <$> getActiveAuxiliaryInstanceConstraints
+  return $ us <> ts <> as <> xs
 
 getActiveUnificationConstraints :: (MonadTypeChecker builtin m) => m [WithContext (UnificationConstraint builtin)]
 getActiveUnificationConstraints = getsMetaCtx unificationConstraints
@@ -426,6 +440,9 @@ getActiveInstanceConstraints = getsMetaCtx instanceConstraints
 getActiveApplicationConstraints :: (MonadTypeChecker builtin m) => m [WithContext (ApplicationConstraint builtin)]
 getActiveApplicationConstraints = getsMetaCtx applicationConstraints
 
+getActiveAuxiliaryInstanceConstraints :: (MonadTypeChecker builtin m) => m [WithContext (InstanceConstraint builtin)]
+getActiveAuxiliaryInstanceConstraints = getsMetaCtx auxiliaryInstanceConstraints
+
 setInstanceConstraints :: (MonadTypeChecker builtin m) => [WithContext (InstanceConstraint builtin)] -> m ()
 setInstanceConstraints newConstraints = modifyMetaCtx $ \TypeCheckerState {..} ->
   TypeCheckerState {instanceConstraints = newConstraints, ..}
@@ -434,16 +451,14 @@ setApplicationConstraints :: (MonadTypeChecker builtin m) => [WithContext (Appli
 setApplicationConstraints newConstraints = modifyMetaCtx $ \TypeCheckerState {..} ->
   TypeCheckerState {applicationConstraints = newConstraints, ..}
 
-removeInstanceConstraint :: forall builtin m. (MonadTypeChecker builtin m) => WithContext (InstanceConstraint builtin) -> m ()
-removeInstanceConstraint constraint = modifyMetaCtx @builtin $ \TypeCheckerState {..} -> do
-  let idOf = constraintID . contextOf
-  let newConstraints = filter (\c -> idOf constraint /= idOf c) instanceConstraints
-  TypeCheckerState {instanceConstraints = newConstraints, ..}
-
 setUnificationConstraints :: (MonadTypeChecker builtin m) => [WithContext (UnificationConstraint builtin)] -> m ()
 setUnificationConstraints newConstraints = modifyMetaCtx $ \TypeCheckerState {..} ->
   TypeCheckerState {unificationConstraints = newConstraints, ..}
 
+setAuxiliaryInstanceConstraints :: (MonadTypeChecker builtin m) => [WithContext (InstanceConstraint builtin)] -> m ()
+setAuxiliaryInstanceConstraints newConstraints = modifyMetaCtx $ \TypeCheckerState {..} ->
+  TypeCheckerState {auxiliaryInstanceConstraints = newConstraints, ..}
+
 addUnificationConstraints :: (MonadTypeChecker builtin m) => [WithContext (UnificationConstraint builtin)] -> m ()
 addUnificationConstraints constraints = do
   unless (null constraints) $ do
@@ -467,6 +482,19 @@ addApplicationConstraint constraint = do
   modifyMetaCtx $ \TypeCheckerState {..} ->
     TypeCheckerState {applicationConstraints = applicationConstraints ++ [constraint], ..}
 
+addAuxiliaryInstanceConstraints :: (MonadTypeChecker builtin m) => [WithContext (InstanceConstraint builtin)] -> m ()
+addAuxiliaryInstanceConstraints constraints = do
+  logDebug MaxDetail ("add-constraints:" <> line <> indent 2 (vcat (fmap prettyExternal constraints)))
+
+  modifyMetaCtx $ \TypeCheckerState {..} ->
+    TypeCheckerState {auxiliaryInstanceConstraints = auxiliaryInstanceConstraints ++ constraints, ..}
+
+removeInstanceConstraint :: forall builtin m. (MonadTypeChecker builtin m) => WithContext (InstanceConstraint builtin) -> m ()
+removeInstanceConstraint constraint = modifyMetaCtx @builtin $ \TypeCheckerState {..} -> do
+  let idOf = constraintID . contextOf
+  let newConstraints = filter (\c -> idOf constraint /= idOf c) instanceConstraints
+  TypeCheckerState {instanceConstraints = newConstraints, ..}
+
 -- | Create a new fresh copy of the context for a new constraint
 copyContext :: forall builtin m. (MonadTypeChecker builtin m) => ConstraintContext builtin -> m (ConstraintContext builtin)
 copyContext (ConstraintContext _cid originProv creationProv _blockingStatus ctx) = do
diff --git a/vehicle/src/Vehicle/Compile/Type/Monad/Instance.hs b/vehicle/src/Vehicle/Compile/Type/Monad/Instance.hs
index ae1a599a0..62666a057 100644
--- a/vehicle/src/Vehicle/Compile/Type/Monad/Instance.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Monad/Instance.hs
@@ -17,6 +17,7 @@ import Control.Monad.State
   )
 import Control.Monad.Trans (MonadTrans)
 import Control.Monad.Trans.Class (lift)
+import Data.Hashable (Hashable)
 import Vehicle.Compile.Context.Free
 import Vehicle.Compile.Error
 import Vehicle.Compile.Normalise.Builtin (NormalisableBuiltin)
@@ -80,7 +81,7 @@ instance (PrintableBuiltin builtin, MonadCompile m) => MonadFreeContext builtin
   hideStdLibDecls p f = TypeCheckerT . hideStdLibDecls p f . unTypeCheckerT
   getHiddenStdLibDecl p = TypeCheckerT . getHiddenStdLibDecl p
 
-instance (Eq builtin, PrintableBuiltin builtin, NormalisableBuiltin builtin, TypableBuiltin builtin, MonadCompile m) => MonadTypeChecker builtin (TypeCheckerT builtin m) where
+instance (Eq builtin, Hashable builtin, PrintableBuiltin builtin, NormalisableBuiltin builtin, TypableBuiltin builtin, MonadCompile m) => MonadTypeChecker builtin (TypeCheckerT builtin m) where
   getMetaState = TypeCheckerT get
   modifyMetaCtx f = TypeCheckerT $ modify f
   getFreshName typ = TypeCheckerT $ getFreshNameInternal typ
diff --git a/vehicle/src/Vehicle/Compile/Type/Subsystem.hs b/vehicle/src/Vehicle/Compile/Type/Subsystem.hs
index c54ad3950..3d994f3e8 100644
--- a/vehicle/src/Vehicle/Compile/Type/Subsystem.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Subsystem.hs
@@ -11,11 +11,11 @@ import Vehicle.Compile.Monomorphisation (monomorphise, removeLiteralCoercions)
 import Vehicle.Compile.Normalise.Builtin (NormalisableBuiltin, findInstanceArg)
 import Vehicle.Compile.Prelude
 import Vehicle.Compile.Print (PrintableBuiltin, prettyExternal)
+import Vehicle.Compile.Print.Builtin (PrintableBuiltin (..))
 import Vehicle.Compile.Type (typeCheckProg)
 import Vehicle.Compile.Type.Core (InstanceDatabase)
 import Vehicle.Compile.Type.Irrelevance (removeIrrelevantCodeFromProg)
 import Vehicle.Compile.Type.System
-import Vehicle.Data.Builtin.Interface
 import Vehicle.Data.Builtin.Standard
 
 typeCheckWithSubsystem ::
@@ -39,7 +39,7 @@ typeCheckWithSubsystem instanceCandidates errorHandler prog = do
 
 resolveInstanceArguments ::
   forall m builtin.
-  (MonadCompile m, BuiltinHasStandardData builtin, Show builtin) =>
+  (MonadCompile m, PrintableBuiltin builtin, Show builtin) =>
   Prog builtin ->
   m (Prog builtin)
 resolveInstanceArguments prog =
diff --git a/vehicle/src/Vehicle/Compile/Type/Subsystem/InputOutputInsertion.hs b/vehicle/src/Vehicle/Compile/Type/Subsystem/InputOutputInsertion.hs
index 6cf456169..b83d8ef21 100644
--- a/vehicle/src/Vehicle/Compile/Type/Subsystem/InputOutputInsertion.hs
+++ b/vehicle/src/Vehicle/Compile/Type/Subsystem/InputOutputInsertion.hs
@@ -85,6 +85,6 @@ addFunctionConstraint constraint declProv@(_, declP) position existingExpr = do
   freeEnv <- getFreeEnv
   let declSort = developerError "function IO constraints should never fail"
   let origin = InstanceTypeRestrictionOrigin $ TypeRestrictionOrigin freeEnv declProv declSort existingExpr
-  _ <- createFreshInstanceConstraint mempty declP origin Irrelevant tcExpr
+  _ <- createFreshInstanceConstraint True mempty declP origin Irrelevant tcExpr
 
   return newExpr
diff --git a/vehicle/src/Vehicle/Compile/Type/System.hs b/vehicle/src/Vehicle/Compile/Type/System.hs
index f5092204b..ccbfb11c1 100644
--- a/vehicle/src/Vehicle/Compile/Type/System.hs
+++ b/vehicle/src/Vehicle/Compile/Type/System.hs
@@ -1,20 +1,19 @@
 module Vehicle.Compile.Type.System where
 
+import Data.Hashable (Hashable)
 import Vehicle.Compile.Context.Free (MonadFreeContext, getFreeEnv)
 import Vehicle.Compile.Error
 import Vehicle.Compile.Normalise.Builtin (NormalisableBuiltin)
 import Vehicle.Compile.Prelude
 import Vehicle.Compile.Print (prettyVerbose)
 import Vehicle.Compile.Type.Builtin (TypableBuiltin)
-import Vehicle.Compile.Type.Constraint.Core
 import Vehicle.Compile.Type.Constraint.IndexSolver (solveDefaultIndexConstraints, solveIndexConstraint)
-import Vehicle.Compile.Type.Constraint.InstanceDefaultSolver (addNewConstraintUsingDefaults)
-import Vehicle.Compile.Type.Constraint.InstanceSolver
+import Vehicle.Compile.Type.Constraint.InstanceDefaultSolver (getDefaultableConstraints)
 import Vehicle.Compile.Type.Constraint.LinearitySolver
 import Vehicle.Compile.Type.Constraint.PolaritySolver
 import Vehicle.Compile.Type.Core
 import Vehicle.Compile.Type.Monad (createFreshInstanceConstraint, createFreshUnificationConstraint, freshMetaExpr)
-import Vehicle.Compile.Type.Monad.Class (MonadTypeChecker)
+import Vehicle.Compile.Type.Monad.Class (MonadTypeChecker, getActiveAuxiliaryInstanceConstraints)
 import Vehicle.Compile.Type.Subsystem.InputOutputInsertion (addFunctionAuxiliaryInputOutputConstraints)
 import Vehicle.Data.Builtin.Linearity
 import Vehicle.Data.Builtin.Polarity
@@ -28,7 +27,7 @@ type TCM builtin m =
   )
 
 -- | A class that provides an abstract interface for a set of builtins.
-class (Eq builtin, NormalisableBuiltin builtin, TypableBuiltin builtin) => HasTypeSystem builtin where
+class (Eq builtin, Hashable builtin, NormalisableBuiltin builtin, TypableBuiltin builtin) => HasTypeSystem builtin where
   convertFromStandardBuiltins ::
     (MonadTypeChecker builtin m) =>
     BuiltinUpdate m Builtin builtin
@@ -43,16 +42,18 @@ class (Eq builtin, NormalisableBuiltin builtin, TypableBuiltin builtin) => HasTy
   addAuxiliaryInputOutputConstraints ::
     (MonadTypeChecker builtin m) => Decl builtin -> m (Decl builtin)
 
-  generateDefaultConstraint ::
+  generateDefaultAuxiliaryConstraint ::
     (MonadTypeChecker builtin m) =>
-    InstanceDatabase builtin ->
     Maybe (Decl builtin) ->
     m Bool
 
-  -- | Solves a type-class constraint
-  solveInstance ::
+  isAuxiliaryConstraint ::
+    Expr builtin -> Bool
+
+  -- | Solves an auxiliary instance constraint (i.e. a constraint that is
+  -- not solvable by the default instance mechanism)
+  solveAuxiliaryInstanceConstraint ::
     (MonadTypeChecker builtin m, MonadFreeContext builtin m) =>
-    InstanceDatabase builtin ->
     WithContext (InstanceConstraint builtin) ->
     m ()
 
@@ -63,24 +64,16 @@ class (Eq builtin, NormalisableBuiltin builtin, TypableBuiltin builtin) => HasTy
 instance HasTypeSystem Builtin where
   convertFromStandardBuiltins = convertToTypingBuiltins
   restrictDeclType = restrictStandardDeclType
-  solveInstance = solveStandardInstanceConstraint
+  isAuxiliaryConstraint e = case e of
+    App (Builtin _ NatInDomainConstraint) _ -> True
+    _ -> False
+  solveAuxiliaryInstanceConstraint = solveIndexConstraint
   addAuxiliaryInputOutputConstraints = return
-  generateDefaultConstraint = addNewConstraintUsingDefaults solveDefaultIndexConstraints
+  generateDefaultAuxiliaryConstraint = addNewStandardAuxiliaryConstraintUsingDefaults
 
 convertToTypingBuiltins :: (MonadCompile m) => BuiltinUpdate m Builtin Builtin
 convertToTypingBuiltins p t args = return $ normAppList (Builtin p t) args
 
-solveStandardInstanceConstraint ::
-  (MonadTypeChecker Builtin m) =>
-  InstanceDatabase Builtin ->
-  WithContext (InstanceConstraint Builtin) ->
-  m ()
-solveStandardInstanceConstraint database constraint = do
-  case instanceGoal (objectIn constraint) of
-    VBuiltin NatInDomainConstraint _ -> solveIndexConstraint constraint
-    VBuiltin {} -> solveInstanceConstraint database constraint
-    _ -> malformedConstraintError constraint
-
 restrictStandardDeclType ::
   forall m.
   (MonadTypeChecker Builtin m) =>
@@ -98,22 +91,30 @@ restrictStandardDeclType declSort (ident, p) typ = do
 
   let expr = BuiltinExpr p (TypeClass tc) [explicit typ]
   let origin = InstanceTypeRestrictionOrigin $ TypeRestrictionOrigin env (ident, provenanceOf typ) declSort typ
-  _ <- createFreshInstanceConstraint mempty p origin Irrelevant expr
+  _ <- createFreshInstanceConstraint False mempty p origin Irrelevant expr
   return typ
 
+-- | Tries to add new unification constraints using default values.
+addNewStandardAuxiliaryConstraintUsingDefaults ::
+  (MonadTypeChecker Builtin m) =>
+  Maybe (Decl Builtin) ->
+  m Bool
+addNewStandardAuxiliaryConstraintUsingDefaults maybeDecl = do
+  -- Calculate the set of candidate constraints
+  auxiliaryConstraints <- getActiveAuxiliaryInstanceConstraints
+  defaultableConstraints <- getDefaultableConstraints maybeDecl auxiliaryConstraints
+  solveDefaultIndexConstraints defaultableConstraints
+
 -------------------------------------------------------------------------------
 -- Linearity
 
 instance HasTypeSystem LinearityBuiltin where
   convertFromStandardBuiltins = convertToLinearityTypes
-  restrictDeclType = \case
-    RestrictedNetwork -> restrictLinearityNetworkType
-    RestrictedDataset -> assertConstantLinearity
-    RestrictedParameter {} -> assertConstantLinearity
-    RestrictedProperty {} -> const return
-  solveInstance = solveLinearityConstraint
+  restrictDeclType = restrictLinearityDeclType
+  isAuxiliaryConstraint _ = True
+  solveAuxiliaryInstanceConstraint = solveLinearityConstraint
   addAuxiliaryInputOutputConstraints = addFunctionAuxiliaryInputOutputConstraints (LinearityRelation . FunctionLinearity)
-  generateDefaultConstraint _ _ = return False
+  generateDefaultAuxiliaryConstraint _ = return False
 
 freshLinearityMeta :: (MonadTypeChecker LinearityBuiltin m) => Provenance -> m (Expr LinearityBuiltin)
 freshLinearityMeta p = unnormalised <$> freshMetaExpr p (TypeUniverse p 0) mempty
@@ -146,19 +147,36 @@ convertToLinearityTypes p b args = case b of
       compilerDeveloperError $
         "Monomorphisation should have got rid of" <+> squotes name <+> "s but found" <+> prettyVerbose args
 
+restrictLinearityDeclType ::
+  forall m.
+  (MonadTypeChecker LinearityBuiltin m) =>
+  RestrictedDecl ->
+  DeclProvenance ->
+  Type LinearityBuiltin ->
+  m (Type LinearityBuiltin)
+restrictLinearityDeclType rDecl declProv declType = do
+  freeEnv <- getFreeEnv
+  let origin = InstanceTypeRestrictionOrigin $ TypeRestrictionOrigin freeEnv declProv rDecl declType
+  case rDecl of
+    RestrictedNetwork -> restrictLinearityNetworkType origin declProv declType
+    RestrictedDataset -> assertConstantLinearity origin declProv declType
+    RestrictedParameter {} -> assertConstantLinearity origin declProv declType
+    RestrictedProperty {} -> return declType
+
 restrictLinearityNetworkType ::
   forall m.
   (MonadTypeChecker LinearityBuiltin m) =>
+  InstanceConstraintOrigin LinearityBuiltin ->
   DeclProvenance ->
   Type LinearityBuiltin ->
   m (Type LinearityBuiltin)
-restrictLinearityNetworkType (ident, p) networkType = do
+restrictLinearityNetworkType origin (ident, p) networkType = do
   inputLin <- freshLinearityMeta p
   outputLin <- freshLinearityMeta p
 
   let inputLinBinder = Binder p (BinderDisplayForm OnlyType False) Explicit Relevant inputLin
   let functionNetworkType = Pi p inputLinBinder outputLin
-  createFreshUnificationConstraint p mempty CheckingAuxiliary networkType functionNetworkType
+  createFreshUnificationConstraint p mempty (CheckingInstanceType origin) networkType functionNetworkType
 
   -- The linearity of the output of a network is the max of 1) Linear (as outputs
   -- are also variables) and 2) the linearity of its input. So prepend this
@@ -173,11 +191,12 @@ restrictLinearityNetworkType (ident, p) networkType = do
 
 assertConstantLinearity ::
   (MonadTypeChecker LinearityBuiltin m) =>
+  InstanceConstraintOrigin LinearityBuiltin ->
   DeclProvenance ->
   Type LinearityBuiltin ->
   m (Type LinearityBuiltin)
-assertConstantLinearity (_, p) t = do
-  createFreshUnificationConstraint p mempty CheckingAuxiliary (LinearityExpr p Constant) t
+assertConstantLinearity origin (_, p) t = do
+  createFreshUnificationConstraint p mempty (CheckingInstanceType origin) (LinearityExpr p Constant) t
   return t
 
 -------------------------------------------------------------------------------
@@ -185,14 +204,11 @@ assertConstantLinearity (_, p) t = do
 
 instance HasTypeSystem PolarityBuiltin where
   convertFromStandardBuiltins = convertToPolarityTypes
-  restrictDeclType = \case
-    RestrictedNetwork -> restrictPolarityNetworkType
-    RestrictedDataset -> assertUnquantifiedPolarity
-    RestrictedParameter {} -> assertUnquantifiedPolarity
-    RestrictedProperty -> const return
-  solveInstance = solvePolarityConstraint
+  restrictDeclType = restrictDeclPolarityType
+  isAuxiliaryConstraint _ = True
+  solveAuxiliaryInstanceConstraint = solvePolarityConstraint
   addAuxiliaryInputOutputConstraints = addFunctionAuxiliaryInputOutputConstraints (PolarityRelation . FunctionPolarity)
-  generateDefaultConstraint _ _ = return False
+  generateDefaultAuxiliaryConstraint _ = return False
 
 freshPolarityMeta :: (MonadTypeChecker PolarityBuiltin m) => Provenance -> m (Expr PolarityBuiltin)
 freshPolarityMeta p = unnormalised <$> freshMetaExpr p (TypeUniverse p 0) mempty
@@ -225,26 +241,45 @@ convertToPolarityTypes p b args = case b of
       compilerDeveloperError $
         "Monomorphisation should have got rid of partially applied" <+> name <+> "types but found" <+> prettyVerbose args
 
+restrictDeclPolarityType ::
+  forall m.
+  (MonadTypeChecker PolarityBuiltin m) =>
+  RestrictedDecl ->
+  DeclProvenance ->
+  Type PolarityBuiltin ->
+  m (Type PolarityBuiltin)
+restrictDeclPolarityType rDecl declProv declType = do
+  freeEnv <- getFreeEnv
+  let origin = InstanceTypeRestrictionOrigin $ TypeRestrictionOrigin freeEnv declProv rDecl declType
+
+  case rDecl of
+    RestrictedNetwork -> restrictPolarityNetworkType origin declProv declType
+    RestrictedDataset -> assertUnquantifiedPolarity origin declProv declType
+    RestrictedParameter {} -> assertUnquantifiedPolarity origin declProv declType
+    RestrictedProperty -> return declType
+
 restrictPolarityNetworkType ::
   forall m.
   (MonadTypeChecker PolarityBuiltin m) =>
+  InstanceConstraintOrigin PolarityBuiltin ->
   DeclProvenance ->
   Type PolarityBuiltin ->
   m (Type PolarityBuiltin)
-restrictPolarityNetworkType (_, p) networkType = do
+restrictPolarityNetworkType origin (_, p) networkType = do
   let inputPol = PolarityExpr p Unquantified
   let outputPol = PolarityExpr p Unquantified
 
   let inputPolBinder = Binder p (BinderDisplayForm OnlyType False) Explicit Relevant inputPol
   let functionNetworkType = Pi p inputPolBinder outputPol
-  createFreshUnificationConstraint p mempty CheckingAuxiliary networkType functionNetworkType
+  createFreshUnificationConstraint p mempty (CheckingInstanceType origin) networkType functionNetworkType
   return networkType
 
 assertUnquantifiedPolarity ::
   (MonadTypeChecker PolarityBuiltin m) =>
+  InstanceConstraintOrigin PolarityBuiltin ->
   DeclProvenance ->
   Type PolarityBuiltin ->
   m (Type PolarityBuiltin)
-assertUnquantifiedPolarity (_, p) t = do
-  createFreshUnificationConstraint p mempty CheckingAuxiliary (PolarityExpr p Unquantified) t
+assertUnquantifiedPolarity origin (_, p) t = do
+  createFreshUnificationConstraint p mempty (CheckingInstanceType origin) (PolarityExpr p Unquantified) t
   return t
diff --git a/vehicle/src/Vehicle/Data/Builtin/Interface.hs b/vehicle/src/Vehicle/Data/Builtin/Interface.hs
index ca4fc35c4..238b33960 100644
--- a/vehicle/src/Vehicle/Data/Builtin/Interface.hs
+++ b/vehicle/src/Vehicle/Data/Builtin/Interface.hs
@@ -84,13 +84,6 @@ class BuiltinHasStandardData builtin where
   mkBuiltinFunction :: BuiltinFunction -> builtin
   getBuiltinFunction :: builtin -> Maybe BuiltinFunction
 
-  getBuiltinTypeClassOp :: builtin -> Maybe TypeClassOp
-
-  isTypeClassOp :: builtin -> Bool
-  isTypeClassOp b = case getBuiltinTypeClassOp b of
-    Just {} -> True
-    Nothing -> False
-
 --------------------------------------------------------------------------------
 -- BuiltinHasStandardTypes
 
diff --git a/vehicle/src/Vehicle/Data/Builtin/Linearity.hs b/vehicle/src/Vehicle/Data/Builtin/Linearity.hs
index 487b7e871..6233b4553 100644
--- a/vehicle/src/Vehicle/Data/Builtin/Linearity.hs
+++ b/vehicle/src/Vehicle/Data/Builtin/Linearity.hs
@@ -154,8 +154,6 @@ instance BuiltinHasStandardData LinearityBuiltin where
     LinearityConstructor c -> Just c
     _ -> Nothing
 
-  getBuiltinTypeClassOp = const Nothing
-
 instance BuiltinHasBoolLiterals LinearityBuiltin where
   mkBoolBuiltinLit b = LinearityConstructor (LBool b)
   getBoolBuiltinLit = \case
diff --git a/vehicle/src/Vehicle/Data/Builtin/Polarity.hs b/vehicle/src/Vehicle/Data/Builtin/Polarity.hs
index 8fa94e904..2e62fe836 100644
--- a/vehicle/src/Vehicle/Data/Builtin/Polarity.hs
+++ b/vehicle/src/Vehicle/Data/Builtin/Polarity.hs
@@ -135,8 +135,6 @@ instance BuiltinHasStandardData PolarityBuiltin where
     PolarityConstructor c -> Just c
     _ -> Nothing
 
-  getBuiltinTypeClassOp = const Nothing
-
 instance BuiltinHasBoolLiterals PolarityBuiltin where
   mkBoolBuiltinLit b = PolarityConstructor (LBool b)
   getBoolBuiltinLit = \case
diff --git a/vehicle/src/Vehicle/Data/Builtin/Standard.hs b/vehicle/src/Vehicle/Data/Builtin/Standard.hs
index fa8be6559..b1a0d1ac9 100644
--- a/vehicle/src/Vehicle/Data/Builtin/Standard.hs
+++ b/vehicle/src/Vehicle/Data/Builtin/Standard.hs
@@ -85,7 +85,3 @@ instance BuiltinHasStandardData Builtin where
   getBuiltinConstructor = \case
     BuiltinConstructor c -> Just c
     _ -> Nothing
-
-  getBuiltinTypeClassOp = \case
-    TypeClassOp op -> Just op
-    _ -> Nothing
diff --git a/vehicle/src/Vehicle/Data/Code/Expr.hs b/vehicle/src/Vehicle/Data/Code/Expr.hs
index 0327c0a96..bd0a6fe61 100644
--- a/vehicle/src/Vehicle/Data/Code/Expr.hs
+++ b/vehicle/src/Vehicle/Data/Code/Expr.hs
@@ -323,12 +323,6 @@ instance (BuiltinHasStandardData builtin) => HasStandardData (Expr builtin) wher
     Just (p, ident, args) -> Just (p, ident, args)
     _ -> Nothing
 
-  getTypeClassOp e = case getBuiltinApp e of
-    Just (p, b, args) -> case getBuiltinTypeClassOp b of
-      Just f -> Just (p, f, args)
-      Nothing -> Nothing
-    _ -> Nothing
-
 instance (BuiltinHasBoolLiterals builtin) => HasBoolLits (Expr builtin) where
   getBoolLit e = case e of
     Builtin _ (getBoolBuiltinLit -> Just b) -> Just (mempty, b)
diff --git a/vehicle/src/Vehicle/Data/Code/Interface.hs b/vehicle/src/Vehicle/Data/Code/Interface.hs
index 3fd69f23b..5c89dfa08 100644
--- a/vehicle/src/Vehicle/Data/Code/Interface.hs
+++ b/vehicle/src/Vehicle/Data/Code/Interface.hs
@@ -140,8 +140,6 @@ class HasStandardData expr where
   mkFreeVar :: Provenance -> Identifier -> [GenericArg expr] -> expr
   getFreeVar :: expr -> Maybe (Provenance, Identifier, [GenericArg expr])
 
-  getTypeClassOp :: expr -> Maybe (Provenance, TypeClassOp, [GenericArg expr])
-
 --------------------------------------------------------------------------------
 -- BuiltinHasStandardTypes
 
diff --git a/vehicle/src/Vehicle/Data/Code/Value.hs b/vehicle/src/Vehicle/Data/Code/Value.hs
index 43afbd384..9b59df3bb 100644
--- a/vehicle/src/Vehicle/Data/Code/Value.hs
+++ b/vehicle/src/Vehicle/Data/Code/Value.hs
@@ -183,12 +183,6 @@ instance (BuiltinHasStandardData builtin) => HasStandardData (Value builtin) whe
     VFreeVar ident args -> Just (mempty, ident, args)
     _ -> Nothing
 
-  getTypeClassOp e = case e of
-    VBuiltin b args -> case getBuiltinTypeClassOp b of
-      Just op -> Just (mempty, op, args)
-      Nothing -> Nothing
-    _ -> Nothing
-
 instance (BuiltinHasBoolLiterals builtin) => HasBoolLits (Value builtin) where
   getBoolLit = \case
     VBuiltin (getBoolBuiltinLit -> Just b) [] -> Just (mempty, b)