Reorganised arg insertion problem (#867)

Author: MatthewDaggitt

vehicle-syntax/src/Vehicle/Syntax/AST/Relevance.hs

@@ -5,6 +5,7 @@ import Data.Aeson (ToJSON)
 import Data.Hashable (Hashable)
 import Data.Serialize (Serialize)
 import GHC.Generics (Generic)
+import Prettyprinter (Pretty (..))
 
 --------------------------------------------------------------------------------
 -- Data
@@ -29,6 +30,11 @@ instance Semigroup Relevance where
 instance Monoid Relevance where
   mempty = Relevant
 
+instance Pretty Relevance where
+  pretty = \case
+    Relevant -> "relevant"
+    Irrelevant -> "irrelevant"
+
 --------------------------------------------------------------------------------
 -- Type class
 

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

@@ -9,6 +9,7 @@ module Vehicle.Compile.Normalise.NBE
     normaliseClosure,
     eval,
     evalApp,
+    evalClosure,
     traverseClosure,
     traverseClosureGeneric,
   )

vehicle/src/Vehicle/Compile/Print.hs

@@ -24,7 +24,7 @@ import Data.IntMap (IntMap)
 import Data.IntMap qualified as IntMap (assocs)
 import Data.Text (Text)
 import GHC.TypeLits (ErrorMessage (..), TypeError)
-import Prettyprinter (list)
+import Prettyprinter (fill, list)
 import Vehicle.Compile.Descope
 import Vehicle.Compile.Normalise.Quote (unnormalise)
 import Vehicle.Compile.Prelude
@@ -160,8 +160,10 @@ type family StrategyFor (tags :: Tags) a :: Strategy where
   -----------------
   -- Constraints --
   -----------------
+  StrategyFor tags (ArgInsertionProblem builtin `In` NamedBoundCtx) = StrategyFor tags (Expr builtin `In` NamedBoundCtx)
   StrategyFor tags (InstanceConstraint builtin `In` ConstraintContext builtin) = StrategyFor tags (Value builtin `In` NamedBoundCtx)
   StrategyFor tags (UnificationConstraint builtin `In` ConstraintContext builtin) = StrategyFor tags (Value builtin `In` NamedBoundCtx)
+  StrategyFor tags (ApplicationConstraint builtin `In` ConstraintContext builtin) = StrategyFor tags (Value builtin `In` NamedBoundCtx)
   StrategyFor tags (Constraint builtin `In` ConstraintContext builtin) = StrategyFor tags (Value builtin `In` NamedBoundCtx)
   ------------
   -- Pretty --
@@ -448,12 +450,37 @@ instance
     let e' = unnormalise @(Value builtin) @(Expr Builtin) (Lv $ length ctx) e
     prettyUsing @rest (e', ctx)
 
+instance
+  (PrettyUsing rest (Arg builtin `In` NamedBoundCtx), ConvertableBuiltin builtin Builtin) =>
+  PrettyUsing ('QuoteValue rest) (Arg builtin `In` NamedBoundCtx)
+  where
+  prettyUsing (e, ctx) = prettyUsing @rest (e, ctx)
+
+instance
+  (PrettyUsing rest (Expr builtin `In` NamedBoundCtx), ConvertableBuiltin builtin Builtin) =>
+  PrettyUsing ('QuoteValue rest) (Expr builtin `In` NamedBoundCtx)
+  where
+  prettyUsing (e, ctx) = prettyUsing @rest (e, ctx)
+
 instance PrettyUsing rest (GenericBinder ()) where
   prettyUsing b = maybe "_" pretty (nameOf b)
 
 --------------------------------------------------------------------------------
 -- Instances for constraints
 
+instance
+  ( PrettyUsing rest (Expr builtin `In` NamedBoundCtx),
+    PrettyUsing rest (Arg builtin `In` NamedBoundCtx)
+  ) =>
+  PrettyUsing rest (ArgInsertionProblem builtin `In` NamedBoundCtx)
+  where
+  prettyUsing (problem, ctx) = do
+    let checkedExpr = solutionSoFar problem
+    let checkedExprDoc = prettyUsing @rest (checkedExpr, ctx)
+    let expectedTypeDoc = prettyUsing @rest (currentExpectedType problem, ctx)
+    let uncheckedArgsDoc = prettyUsing @rest (uncheckedArgs problem, ctx)
+    parens (checkedExprDoc <+> ":" <+> expectedTypeDoc) <+> "@" <+> uncheckedArgsDoc
+
 prettyConstraintContext :: ConstraintContext builtin -> Doc a
 prettyConstraintContext ctx =
   "#" <> pretty (constraintID ctx) <> ". " -- <+> pretty ctx
@@ -475,15 +502,25 @@ instance
     let expr' = prettyUsing @rest (expr, namedBoundCtxOf ctx)
     prettyConstraintContext ctx <+> pretty m <+> "<=" <+> expr'
 
+instance
+  (PrettyUsing rest (ArgInsertionProblem builtin `In` NamedBoundCtx)) =>
+  PrettyUsing rest (ApplicationConstraint builtin `In` ConstraintContext builtin)
+  where
+  prettyUsing (InferArgs {..}, ctx) = do
+    let problemDoc = prettyUsing @rest (argInsertionProblem, namedBoundCtxOf ctx)
+    prettyConstraintContext ctx <+> parens (pretty exprSolutionMeta <+> "=" <+> problemDoc) <+> ":" <+> pretty typeSolutionMeta
+
 instance
   ( PrettyUsing rest (UnificationConstraint builtin `In` ctx),
-    PrettyUsing rest (InstanceConstraint builtin `In` ctx)
+    PrettyUsing rest (InstanceConstraint builtin `In` ctx),
+    PrettyUsing rest (ApplicationConstraint builtin `In` ctx)
   ) =>
   PrettyUsing rest (Constraint builtin `In` ctx)
   where
   prettyUsing (c, ctx) = case c of
     UnificationConstraint uc -> prettyUsing @rest (uc, ctx)
     InstanceConstraint tc -> prettyUsing @rest (tc, ctx)
+    ApplicationConstraint tc -> prettyUsing @rest (tc, ctx)
 
 --------------------------------------------------------------------------------
 -- Assertions
@@ -545,7 +582,7 @@ instance
 instance (PrettyUsing rest (a `In` ctx)) => PrettyUsing rest (MetaMap a `In` ctx) where
   prettyUsing (MetaMap m, ctx) = prettyMapEntries entries
     where
-      entries = fmap (bimap MetaID (prettyUsing @rest . (,ctx))) (IntMap.assocs m)
+      entries = fmap (bimap (fill 3 . pretty . MetaID) (prettyUsing @rest . (,ctx))) (IntMap.assocs m)
 
 instance (PrettyUsing rest (a `In` ctx)) => PrettyUsing rest (MaybeTrivial a `In` ctx) where
   prettyUsing (e, ctx) = case e of

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

@@ -405,6 +405,8 @@ instance MeaningfulError CompileError where
           InstanceConstraint (Resolve InstanceConstraintOrigin {..} _ _ _) ->
             "insufficient information to find a valid type for the overloaded expression"
               <+> squotes (prettyTypeClassConstraintOriginExpr ctx checkedInstanceOp checkedInstanceOpArgs)
+          ApplicationConstraint {} ->
+            "unsolved application constraint: " <+> prettyFriendly (WithContext constraint ctx)
     UnsolvedMetas ms ->
       UError $
         UserError

vehicle/src/Vehicle/Compile/Type.hs

@@ -1,6 +1,6 @@
 module Vehicle.Compile.Type
   ( typeCheckProg,
-    typeCheckExpr,
+    typeCheckSolitaryExpr,
   )
 where
 
@@ -15,6 +15,7 @@ import Vehicle.Compile.Normalise.Builtin (NormalisableBuiltin)
 import Vehicle.Compile.Prelude
 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.UnificationSolver
 import Vehicle.Compile.Type.Core
@@ -43,17 +44,17 @@ typeCheckProg instanceCandidates freeCtx (Main uncheckedProg) =
       xs <- typeCheckDecls uncheckedProg
       return $ Main xs
 
-typeCheckExpr ::
+typeCheckSolitaryExpr ::
   forall builtin m.
   (HasTypeSystem builtin, NormalisableBuiltin builtin, MonadCompile m) =>
   InstanceDatabase builtin ->
   FreeCtx builtin ->
   Expr Builtin ->
   m (Expr builtin)
-typeCheckExpr instanceCandidates freeCtx expr1 = do
+typeCheckSolitaryExpr instanceCandidates freeCtx expr1 = do
   runTypeCheckerTInitially freeCtx instanceCandidates $ do
     expr2 <- convertExprFromStandardTypes expr1
-    (expr3, _exprType) <- runMonadBidirectional (Proxy @builtin) $ inferExpr expr2
+    (expr3, _exprType) <- inferExprType mempty Relevant expr2
     solveConstraints @builtin Nothing
     expr4 <- substMetas expr3
     checkAllUnknownsSolved (Proxy @builtin)
@@ -134,8 +135,9 @@ typeCheckFunction p ident anns typ body = do
 
   -- Type check the body.
   let pass = bidirectionalPassDoc <+> "body of" <+> quotePretty ident
-  checkedBody <- logCompilerPass MidDetail pass $ do
-    runMonadBidirectional (Proxy @builtin) $ checkExpr checkedType body
+  checkedBody <-
+    logCompilerPass MidDetail pass $
+      checkExprType mempty Relevant checkedType body
 
   -- Reconstruct the function.
   let checkedDecl = DefFunction p ident anns checkedType checkedBody
@@ -167,7 +169,7 @@ checkDeclType :: forall builtin m. (TCM builtin m) => Identifier -> Expr builtin
 checkDeclType ident declType = do
   let pass = bidirectionalPassDoc <+> "type of" <+> quotePretty ident
   logCompilerPass MidDetail pass $ do
-    runMonadBidirectional (Proxy @builtin) $ checkExpr (TypeUniverse mempty 0) declType
+    checkExprType mempty Relevant (TypeUniverse mempty 0) declType
 
 restrictAbstractDefType ::
   (TCM builtin m) =>
@@ -216,16 +218,21 @@ solveConstraints d = logCompilerPass MidDetail "constraint solving" $ 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
+
               metasSolvedDuringUnification <-
                 trackSolvedMetas (Proxy @builtin) $
-                  runUnificationSolver (Proxy @builtin) recentlySolvedMetas
+                  runUnificationSolver (Proxy @builtin) (metasSolvedDuringApplications <> recentlySolvedMetas)
 
               logUnsolvedUnknowns updatedDecl (Just recentlySolvedMetas)
 
               metasSolvedDuringInstanceResolution <-
                 trackSolvedMetas (Proxy @builtin) $
-                  runInstanceSolver (Proxy @builtin) metasSolvedDuringUnification
-              return metasSolvedDuringInstanceResolution
+                  runInstanceSolver (Proxy @builtin) (metasSolvedDuringUnification <> metasSolvedDuringApplications)
+
+              return (metasSolvedDuringInstanceResolution <> metasSolvedDuringUnification)
 
             loopOverConstraints newMetasSolved (loopNumber + 1) updatedDecl
 
@@ -318,7 +325,7 @@ logUnsolvedUnknowns maybeDecl maybeSolvedMetas = do
     return $
       "current-solution:"
         <> line
-        <> prettyVerbose (fmap unnormalised updatedSubst)
+        <> indent 2 (prettyVerbose (fmap unnormalised updatedSubst))
         <> line
         <> "unsolved-metas:"
         <> line