Reuse instance search for checking parameter/dataset/network/property types (#868)

* Use instances for declaration restrictions

* Fix formatting

* Fix

Author: MatthewDaggitt

CONTRIBUTING.md

@@ -466,12 +466,12 @@ We recommend you install Python using [pyenv].
 
 1. Install [pyenv] following the instructions on the website: <https://github.com/pyenv/pyenv#installation>
 
-2. Install the latest release of each supported Python version. Currently, those are 3.7, 3.8, 3.9, 3.10, and 3.11.
+2. Install the latest release of each supported Python version.
 
    Run the following command:
 
    ```sh
-   pyenv install 3.7 3.8 3.9 3.10 3.11
+   pyenv install 3.9 3.10 3.11 3.12 3.13
    ```
 
 3. Check if your installation was successful.

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

@@ -1,6 +1,7 @@
 module Vehicle.Syntax.AST.Decl where
 
 import Control.DeepSeq (NFData)
+import Data.Hashable (Hashable)
 import Data.Serialize (Serialize)
 import GHC.Generics (Generic)
 import Prettyprinter (Pretty (..))
@@ -97,12 +98,14 @@ isAbstractDecl = \case
 data ParameterSort
   = Inferable
   | NonInferable
-  deriving (Eq, Show, Generic)
+  deriving (Eq, Ord, Show, Generic)
 
 instance NFData ParameterSort
 
 instance Serialize ParameterSort
 
+instance Hashable ParameterSort
+
 instance Pretty ParameterSort where
   pretty = \case
     Inferable -> "(infer=True)"

vehicle-syntax/src/Vehicle/Syntax/Builtin/TypeClass.hs

@@ -5,6 +5,7 @@ import Data.Hashable (Hashable (..))
 import Data.Serialize (Serialize)
 import GHC.Generics (Generic)
 import Prettyprinter (Pretty (..), (<+>))
+import Vehicle.Syntax.AST.Decl (ParameterSort)
 import Vehicle.Syntax.Builtin.BasicOperations
 
 --------------------------------------------------------------------------------
@@ -27,6 +28,13 @@ data TypeClass
     HasNatLits
   | HasRatLits
   | HasVecLits
+  | -- Declaration type restrictions
+    ValidPropertyType
+  | ValidParameterType ParameterSort
+  | ValidNetworkType
+  | ValidNetworkTensorType
+  | ValidDatasetType
+  | ValidDatasetElementType
   deriving (Eq, Ord, Generic, Show)
 
 instance NFData TypeClass
@@ -51,6 +59,12 @@ instance Pretty TypeClass where
     HasNatLits -> "HasNatLiterals"
     HasRatLits -> "HasRatLiterals"
     HasVecLits -> "HasVecLiterals"
+    ValidPropertyType -> "ValidPropertyType"
+    ValidParameterType {} -> "ValidParameterType"
+    ValidNetworkType -> "ValidNetworkType"
+    ValidNetworkTensorType -> "ValidNetworkTensorType"
+    ValidDatasetType -> "ValidDatasetType"
+    ValidDatasetElementType -> "ValidDatasetElementType"
 
 -- Builtin operations for type-classes
 data TypeClassOp

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

@@ -514,6 +514,12 @@ compileBuiltin _p b args = case b of
     HasFold -> unsupportedError
     HasMap -> unsupportedError
     HasQuantifierIn {} -> unsupportedError
+    ValidPropertyType -> unsupportedError
+    ValidParameterType {} -> unsupportedError
+    ValidNetworkType {} -> unsupportedError
+    ValidNetworkTensorType {} -> unsupportedError
+    ValidDatasetType {} -> unsupportedError
+    ValidDatasetElementType {} -> unsupportedError
   TypeClassOp op -> case op of
     QuantifierTC q -> case reverse args of
       (ExplicitArg _ _ (Lam _ binder body)) : _ -> compileTypeLevelQuantifier q [binder] body

vehicle/src/Vehicle/Compile/Error.hs

@@ -6,10 +6,13 @@ import Control.Exception (IOException)
 import Control.Monad.Except (MonadError, throwError)
 import Data.List.NonEmpty (NonEmpty)
 import Data.Map qualified as Map
+import Data.Text (Text)
+import Data.Typeable (Proxy)
 import Data.Void (Void)
 import Prettyprinter (list)
 import Vehicle.Backend.LossFunction.Core (BooleanDifferentiableLogicField, TensorDifferentiableLogicField)
 import Vehicle.Backend.Prelude
+import Vehicle.Compile.Normalise.Builtin (NormalisableBuiltin)
 import Vehicle.Compile.Prelude
 import Vehicle.Compile.Print (PrettyFriendly)
 import Vehicle.Compile.Print.Builtin
@@ -32,6 +35,56 @@ type MonadCompile m =
     MonadError CompileError m
   )
 
+--------------------------------------------------------------------------------
+-- Typing errors
+
+data MissingExplicitArgError builtin = MissingExplicitArgError
+  { _ctx :: NamedBoundCtx,
+    explicitBinder :: Binder builtin,
+    nonExplicitArg :: Arg builtin
+  }
+  deriving (Show)
+
+data RelevantUseOfIrrelevantVariableError builtin = RelevantUseOfIrrelevantVariableError
+  { _proxy :: Proxy builtin,
+    _provenance :: Provenance,
+    irrelevantVariableName :: Name
+  }
+  deriving (Show)
+
+data FunctionTypeMismatchError builtin = FunctionTypeMismatchError
+  { _ctx :: NamedBoundCtx,
+    originalFunction :: Expr builtin,
+    currentExpectedType :: Expr builtin,
+    currentUncheckedArgs :: [Arg builtin]
+  }
+  deriving (Show)
+
+newtype FailedUnificationConstraintsError builtin = FailedUnificationConstraintsError
+  { failedConstraints :: NonEmpty (WithContext (UnificationConstraint builtin))
+  }
+  deriving (Show)
+
+data FailedInstanceConstraintError builtin = FailedInstanceConstraintError
+  { _freeEnv :: FreeEnv builtin,
+    failedConstraint :: WithContext (InstanceConstraint builtin),
+    exploredCandidates :: [(WithContext (InstanceCandidate builtin), UnAnnDoc)]
+  }
+  deriving (Show)
+
+-- | Errors thrown during type-checking
+data TypingError builtin
+  = MissingExplicitArg (MissingExplicitArgError builtin)
+  | FunctionTypeMismatch (FunctionTypeMismatchError builtin)
+  | RelevantUseOfIrrelevantVariable (RelevantUseOfIrrelevantVariableError builtin)
+  | FailedUnificationConstraints (FailedUnificationConstraintsError builtin)
+  | FailedInstanceConstraint (FailedInstanceConstraintError builtin)
+  | FailedIndexConstraintTooBig (ConstraintContext builtin) Int Int
+  | FailedIndexConstraintUnknown (ConstraintContext builtin) (Value builtin) (VType builtin)
+  | UnsolvedConstraints (NonEmpty (WithContext (Constraint builtin)))
+  | UnsolvedMetas (Proxy builtin) (NonEmpty (MetaID, Provenance))
+  deriving (Show)
+
 --------------------------------------------------------------------------------
 -- Compilation errors
 
@@ -45,12 +98,9 @@ data CompileError
   | DeclarationBoundShadowing Provenance Name
   | MissingPrunedName Name
   | -- Type checking errors
-    UnresolvedHole Provenance Name
-  | forall builtin.
-    (PrintableBuiltin builtin, Show builtin) =>
+    forall builtin.
+    (Eq builtin, PrintableBuiltin builtin, NormalisableBuiltin builtin, Show builtin) =>
     TypingError (TypingError builtin)
-  | UnsolvedMetas (NonEmpty (MetaID, Provenance))
-  | RelevantUseOfIrrelevantVariable Provenance Name
   | -- Resource loading errors
     ResourceNotProvided DeclProvenance ExternalResource
   | ResourceIOError DeclProvenance ExternalResource IOException
@@ -59,32 +109,23 @@ data CompileError
   | -- Unsupported networks
     NetworkTypeHasVariableSizeTensor DeclProvenance (GluedType Builtin) (VType Builtin) InputOrOutput
   | NetworkTypeHasImplicitSizeTensor DeclProvenance (GluedType Builtin) Identifier InputOrOutput
-  | NetworkTypeIsNotAFunction DeclProvenance (GluedType Builtin)
-  | NetworkTypeIsNotOverTensors DeclProvenance (GluedType Builtin) (VType Builtin) InputOrOutput
-  | NetworkTypeHasNonExplicitArguments DeclProvenance (GluedType Builtin) (VBinder Builtin)
-  | NetworkTypeHasUnsupportedElementType DeclProvenance (GluedType Builtin) (VType Builtin) InputOrOutput
   | -- Unsupported datasets
-    DatasetTypeUnsupportedContainer DeclProvenance (GluedType Builtin)
-  | DatasetTypeUnsupportedElement DeclProvenance (GluedType Builtin) (VType Builtin)
-  | DatasetVariableSizeTensor DeclProvenance (GluedType Builtin) (VType Builtin)
+    DatasetVariableSizeTensor DeclProvenance (GluedType Builtin) (VType Builtin)
   | DatasetDimensionSizeMismatch DeclProvenance FilePath Int Int TensorShape TensorShape
   | DatasetDimensionsMismatch DeclProvenance FilePath (GluedExpr Builtin) TensorShape
   | DatasetTypeMismatch DeclProvenance FilePath (GluedType Builtin) (VType Builtin) (Doc Void)
   | DatasetInvalidIndex DeclProvenance FilePath Int Int
   | DatasetInvalidNat DeclProvenance FilePath Int
   | -- Unsupported parameters
-    ParameterTypeUnsupported DeclProvenance (GluedType Builtin)
-  | ParameterTypeVariableSizeIndex DeclProvenance (GluedType Builtin)
+    ParameterTypeVariableSizeIndex DeclProvenance (GluedType Builtin)
   | ParameterTypeInferableParameterIndex DeclProvenance Identifier
   | ParameterValueUnparsable DeclProvenance String BuiltinType
   | ParameterValueInvalidIndex DeclProvenance Int Int
   | ParameterValueInvalidNat DeclProvenance Int
-  | InferableParameterTypeUnsupported DeclProvenance (GluedType Builtin)
   | InferableParameterContradictory Identifier (DeclProvenance, ExternalResource, Int) (DeclProvenance, ExternalResource, Int)
   | InferableParameterUninferrable DeclProvenance
   | -- Unsupported properties
-    PropertyTypeUnsupported DeclProvenance (GluedType Builtin)
-  | NoPropertiesFound
+    NoPropertiesFound
   | -- Verification backend errors
     forall builtin.
     (PrintableBuiltin builtin, Eq builtin, PrettyFriendly (Contextualised (VType builtin) NamedBoundCtx)) =>
@@ -183,3 +224,37 @@ lookupInFreeCtx ::
 lookupInFreeCtx pass ident ctx = case Map.lookup ident ctx of
   Nothing -> internalScopingError pass ident
   Just x -> return x
+
+--------------------------------------------------------------------------------
+-- The final error type
+
+-- | Errors from external code that we have no control over.
+--  These may be either user or developer errors but in general we
+--  can't distinguish between the two.
+newtype ExternalError = ExternalError Text
+
+-- | Errors that are the user's responsibility to fix.
+data UserError = UserError
+  { provenance :: Provenance,
+    problem :: UnAnnDoc,
+    fix :: Maybe UnAnnDoc
+  }
+
+data VehicleError
+  = UError UserError
+  | EError ExternalError
+  | DError (Doc ())
+
+instance Pretty VehicleError where
+  pretty (UError (UserError p prob probFix)) =
+    unAnnotate $
+      "Error in"
+        <+> pretty p
+        <> ":"
+          <+> prob
+        <> maybe "" (\fix -> line <> fixText fix) probFix
+  pretty (EError (ExternalError text)) = pretty text
+  pretty (DError text) = unAnnotate text
+
+fixText :: Doc ann -> Doc ann
+fixText t = "Fix:" <+> t

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

@@ -6,7 +6,6 @@ module Vehicle.Compile.Normalise.Builtin where
 
 import Control.Monad (zipWithM)
 import Data.Foldable (foldrM)
-import Vehicle.Compile.Error (MonadCompile)
 import Vehicle.Compile.Prelude
 import Vehicle.Compile.Print.Builtin
 import Vehicle.Data.Builtin.Core
@@ -44,15 +43,15 @@ import Vehicle.Data.Tensor (Tensor, foldTensor, mapTensor, zipWithTensor)
 -- Differential logics all normalise to the same type but have different
 -- methods of normalisation.
 type EvalBuiltinApp m builtin =
-  (MonadCompile m) =>
+  (MonadLogger m) =>
   EvalApp (Value builtin) m ->
   Eval builtin m ->
   builtin ->
   [Arg builtin] ->
   m (Value builtin)
 
 type Eval builtin m =
-  (MonadCompile m) =>
+  (MonadLogger m) =>
   Expr builtin ->
   m (Value builtin)
 

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

@@ -5,7 +5,7 @@ import Vehicle.Data.Builtin.Linearity (LinearityBuiltin (..))
 import Vehicle.Data.Builtin.Loss (LossTensorBuiltin (..))
 import Vehicle.Data.Builtin.Polarity (PolarityBuiltin (..))
 import Vehicle.Data.Builtin.Tensor (TensorBuiltin (..))
-import Vehicle.Data.Code.Expr (Expr (..), mapBuiltins, normAppList, pattern BuiltinExpr)
+import Vehicle.Data.Code.Expr (Expr (..), mapBuiltins, normAppList, pattern App, pattern BuiltinExpr)
 import Vehicle.Data.Code.Interface (tensorToExpr)
 import Vehicle.Libraries.StandardLibrary.Definitions (StdLibFunction (..))
 import Vehicle.Prelude
@@ -153,3 +153,9 @@ instance PrintableBuiltin TensorBuiltin where
 
 instance PrintableBuiltin LossTensorBuiltin where
   isCoercion = const False
+
+isCoercionExpr :: (PrintableBuiltin builtin) => Expr builtin -> Bool
+isCoercionExpr = \case
+  Builtin _ b -> isCoercion b
+  App (Builtin _ b) _ -> isCoercion b
+  _ -> False