Locate invalid datatype premises

6 files changed, 105 insertions, 40 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index f0074ff..ed5731a 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -1053,7 +1053,10 @@ checkDatatype context datatype = do
             (canonicalizeWithAt context structContext)
             datatype
             >>= either
-                (throwIO . checkingErrorAt context)
+                ( throwIO
+                    . checkingErrorAt context
+                    . Datatype.renderDatatypeValidationError
+                )
                 pure
     st <- get
     committed <-
diff --git a/source/Checking/Datatype.hs b/source/Checking/Datatype.hs
index 1f98f79..d694ec8 100644
--- a/source/Checking/Datatype.hs
+++ b/source/Checking/Datatype.hs
@@ -3,6 +3,9 @@
 
 module Checking.Datatype
     ( CheckedDatatype
+    , DatatypeValidationError
+    , datatypeValidationErrorLocation
+    , renderDatatypeValidationError
     , prepareCheckedDatatype
     , checkedDatatypeHeadSymbol
     , checkedDatatypeConstructorSymbols
@@ -44,6 +47,28 @@ data CheckedDatatypePremise
     = RecursiveDatatypePremise !VarSymbol !Expr
     | NonRecursiveDatatypePremise !VarSymbol !Expr
 
+data DatatypeValidationError
+    = InvalidDatatype !Text
+    | InvalidDatatypePremise !Location !Text
+    deriving (Show, Eq)
+
+datatypeValidationErrorLocation
+    :: DatatypeValidationError
+    -> Maybe Location
+datatypeValidationErrorLocation = \case
+    InvalidDatatype _message -> Nothing
+    InvalidDatatypePremise location _message -> Just location
+
+renderDatatypeValidationError :: DatatypeValidationError -> Text
+renderDatatypeValidationError = \case
+    InvalidDatatype message -> message
+    InvalidDatatypePremise _location message -> message
+
+data CanonicalDatatypeClause = CanonicalDatatypeClause
+    { canonicalDatatypeClauseConstructor :: !SymbolPattern
+    , canonicalDatatypeClausePremises :: ![(VarSymbol, Location, Expr)]
+    }
+
 -- | Read-only normalized clause data for exact typed lowering.
 data CheckedDatatypeClauseView = CheckedDatatypeClauseView
     { checkedDatatypeClauseViewConstructor :: !FunctionSymbol
@@ -62,24 +87,33 @@ prepareCheckedDatatype
     :: Monad m
     => (Expr -> m Expr)
     -> Datatype
-    -> m (Either Text CheckedDatatype)
+    -> m (Either DatatypeValidationError CheckedDatatype)
 prepareCheckedDatatype canonicalizeDomain Datatype{datatypeHead, datatypeClauses} = do
     canonicalClauses <- traverse canonicalizeClause datatypeClauses
     pure (validateDatatype datatypeHead canonicalClauses)
   where
-    canonicalizeClause clause@DatatypeClause{datatypeClausePremises} = do
+    canonicalizeClause DatatypeClause
+            { datatypeClauseConstructor
+            , datatypeClausePremises
+            } = do
         premises <-
             traverse
                 (\(var, domain) ->
-                    (\canonicalDomain -> (var, canonicalDomain))
+                    (\canonicalDomain ->
+                        (var, exprLocation domain, canonicalDomain))
                         <$> canonicalizeDomain domain)
                 datatypeClausePremises
-        pure clause{datatypeClausePremises = premises}
+        pure
+            CanonicalDatatypeClause
+                { canonicalDatatypeClauseConstructor =
+                    datatypeClauseConstructor
+                , canonicalDatatypeClausePremises = premises
+                }
 
 validateDatatype
     :: SymbolPattern
-    -> NonEmpty DatatypeClause
-    -> Either Text CheckedDatatype
+    -> NonEmpty CanonicalDatatypeClause
+    -> Either DatatypeValidationError CheckedDatatype
 validateDatatype
     (SymbolPattern datatypeSymbol datatypeArgs)
     datatypeClauses = do
@@ -88,8 +122,8 @@ validateDatatype
             "datatype head must be nullary"
         let constructorSymbols =
                 [ constructorSymbol
-                | DatatypeClause
-                    { datatypeClauseConstructor =
+                | CanonicalDatatypeClause
+                    { canonicalDatatypeClauseConstructor =
                         SymbolPattern constructorSymbol _
                     } <- NonEmpty.toList datatypeClauses
                 ]
@@ -110,14 +144,14 @@ validateDatatype
 
 validateDatatypeClause
     :: FunctionSymbol
-    -> DatatypeClause
-    -> Either Text CheckedDatatypeClause
+    -> CanonicalDatatypeClause
+    -> Either DatatypeValidationError CheckedDatatypeClause
 validateDatatypeClause
     datatypeSymbol
-    DatatypeClause
-        { datatypeClauseConstructor =
+    CanonicalDatatypeClause
+        { canonicalDatatypeClauseConstructor =
             SymbolPattern constructorSymbol constructorArgs
-        , datatypeClausePremises
+        , canonicalDatatypeClausePremises
         } = do
         require
             (constructorSymbol /= ApplySymbol)
@@ -131,7 +165,9 @@ validateDatatypeClause
                 ( "datatype constructor arguments must be linear: "
                     <> formatVars duplicateConstructorArgs
                 )
-        let premiseVars = fst <$> datatypeClausePremises
+        let premiseVars =
+                (\(variable, _location, _domain) -> variable)
+                    <$> canonicalDatatypeClausePremises
             duplicatePremiseVars = duplicateVars premiseVars
         require
             (Set.null duplicatePremiseVars)
@@ -149,7 +185,7 @@ validateDatatypeClause
         checkedDatatypeClausePremises <-
             traverse
                 (validateDatatypePremise datatypeSymbol)
-                datatypeClausePremises
+                canonicalDatatypeClausePremises
         pure
             CheckedDatatypeClause
                 { checkedDatatypeClauseConstructor = constructorSymbol
@@ -160,11 +196,11 @@ validateDatatypeClause
 
 validateDatatypePremise
     :: FunctionSymbol
-    -> (VarSymbol, Expr)
-    -> Either Text CheckedDatatypePremise
-validateDatatypePremise datatypeSymbol (var, domain) = do
+    -> (VarSymbol, Location, Expr)
+    -> Either DatatypeValidationError CheckedDatatypePremise
+validateDatatypePremise datatypeSymbol (var, location, domain) = do
     let domainFreeVars = freeVars domain
-    require
+    requirePremise location
         (Set.null domainFreeVars)
             ( "datatype premise domains must be closed terms: "
                 <> formatVars domainFreeVars
@@ -173,7 +209,7 @@ validateDatatypePremise datatypeSymbol (var, domain) = do
         then
             Right (RecursiveDatatypePremise var domain)
         else do
-            require
+            requirePremise location
                 ( SymbolMixfix datatypeSymbol
                     `Set.notMember` mentionedSymbols domain
                 )
@@ -183,12 +219,23 @@ validateDatatypePremise datatypeSymbol (var, domain) = do
     datatypeCarrier =
         TermSymbol Nowhere (SymbolMixfix datatypeSymbol) []
 
-require :: Bool -> Text -> Either Text ()
+require :: Bool -> Text -> Either DatatypeValidationError ()
 require condition message
     | condition =
         Right ()
     | otherwise =
-        Left message
+        Left (InvalidDatatype message)
+
+requirePremise
+    :: Location
+    -> Bool
+    -> Text
+    -> Either DatatypeValidationError ()
+requirePremise location condition message
+    | condition =
+        Right ()
+    | otherwise =
+        Left (InvalidDatatypePremise location message)
 
 checkedDatatypeHeadSymbol :: CheckedDatatype -> Symbol
 checkedDatatypeHeadSymbol =
diff --git a/source/Checking/Exact/Datatype.hs b/source/Checking/Exact/Datatype.hs
index 8e0b907..01cde88 100644
--- a/source/Checking/Exact/Datatype.hs
+++ b/source/Checking/Exact/Datatype.hs
@@ -245,6 +245,17 @@ type Prepare failure =
 
 type SourceOccurrence = (Location, Raw.Marker, CanonicalLexicalEntry)
 
+exactDatatypeInvalid
+    :: Location
+    -> Datatype.DatatypeValidationError
+    -> ExactDatatypeError
+exactDatatypeInvalid declarationLocation failure =
+    ExactDatatypeInvalid
+        (fromMaybe
+            declarationLocation
+            (Datatype.datatypeValidationErrorLocation failure))
+        (Datatype.renderDatatypeValidationError failure)
+
 prepareExactDatatype
     :: Raw.Block
     -> [SourceOccurrence]
@@ -276,7 +287,7 @@ prepareExactDatatype block occurrences =
             Except.lift
                 (Datatype.prepareCheckedDatatype pure internal)
                 >>= Except.liftEither
-                    . first (ExactDatatypeInvalid location)
+                    . first (exactDatatypeInvalid location)
         let symbols =
                 Datatype.checkedDatatypeHeadSymbol checked
                     :| toList
diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs
index 4a9b4e8..c3f281c 100644
--- a/source/Checking/Exact/Inductive.hs
+++ b/source/Checking/Exact/Inductive.hs
@@ -635,18 +635,4 @@ orderedUnique =
             (Set.insert value seen, value : values)
 
 termLocation :: Internal.Expr -> Location
-termLocation = \case
-    Internal.TermVar variable -> locate variable
-    Internal.TermSymbol location _symbol _arguments -> location
-    Internal.TermSymbolStruct _symbol expression ->
-        maybe Nowhere termLocation expression
-    Internal.Apply function _arguments -> termLocation function
-    Internal.TermSep variable _bound _predicate -> locate variable
-    Internal.ReplacePred value _domain _bound _predicate -> locate value
-    Internal.ReplaceFun ((variable, _domain) :| _remaining) _value _condition ->
-        locate variable
-    Internal.Connected _connective left _right -> termLocation left
-    Internal.Lambda{} -> Nowhere
-    Internal.Quantified{} -> Nowhere
-    Internal.PropositionalConstant{} -> Nowhere
-    Internal.Not location _term -> location
+termLocation = Internal.exprLocation
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index e46826f..84baa12 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -171,6 +171,24 @@ data ExprOf a
     | Not Location (ExprOf a)
     deriving (Functor, Foldable, Traversable)
 
+-- | Best source location carried by an elaborated expression.
+exprLocation :: Expr -> Location
+exprLocation = \case
+    TermVar variable -> locate variable
+    TermSymbol location _symbol _arguments -> location
+    TermSymbolStruct _symbol expression ->
+        maybe Nowhere exprLocation expression
+    Apply function _arguments -> exprLocation function
+    TermSep variable _bound _predicate -> locate variable
+    ReplacePred value _domain _bound _predicate -> locate value
+    ReplaceFun ((variable, _domain) :| _remaining) _value _condition ->
+        locate variable
+    Connected _connective left _right -> exprLocation left
+    Lambda{} -> Nowhere
+    Quantified{} -> Nowhere
+    PropositionalConstant{} -> Nowhere
+    Not location _term -> location
+
 data ReplacementVar = ReplacementDomVar | ReplacementRangeVar deriving (Show, Eq, Ord, Generic, Hashable)
 
 makeBound ''ExprOf
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index d95880a..e2b5691 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -1251,7 +1251,7 @@ compilesAndReusesExactDatatypes =
                                 location _message)))
                     prefix -> do
                 assertEqual "nested datatype failure line"
-                    1
+                    4
                     (locLine location)
                 assertBool "nested datatype publishes no prefix"
                     (null