fix

src/Juvix/Compiler/Builtins/Eq.hs

@@ -1,10 +1,25 @@
 module Juvix.Compiler.Builtins.Eq where
 
+import Juvix.Compiler.Internal.Builtins
 import Juvix.Compiler.Internal.Extra
 import Juvix.Prelude
+import Juvix.Prelude.Pretty
 
-checkEqDef :: InductiveDef -> Sem r ()
-checkEqDef _ = return ()
+checkEqDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
+checkEqDef d = do
+  let err :: forall a. Text -> Sem r a
+      err = builtinsErrorText (getLoc d)
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "Lists should be in the small universe")
+  let eqTxt = prettyText BuiltinEq
+  case d ^. inductiveParameters of
+    [_] -> return ()
+    _ -> err (eqTxt <> "should have exactly one type parameter")
+  case d ^. inductiveConstructors of
+    [c1] -> checkMkEq c1
+    _ -> err (eqTxt <> "should have exactly two constructors")
+
+checkMkEq :: ConstructorDef -> Sem r ()
+checkMkEq _ = return ()
 
 checkIsEq :: FunctionDef -> Sem r ()
 checkIsEq _ = return ()

src/Juvix/Compiler/Concrete/Extra.hs

@@ -112,8 +112,8 @@ isBodyExpression = \case
   SigBodyClauses {} -> False
 
 isLhsFunctionLike :: FunctionLhs 'Parsed -> Bool
-isLhsFunctionLike FunctionLhs {..} = not (null _funLhsArgs)
+isLhsFunctionLike FunctionLhs {..} = notNull _funLhsArgs
 
 isFunctionLike :: FunctionDef 'Parsed -> Bool
 isFunctionLike d@FunctionDef {..} =
-   isLhsFunctionLike (functionDefLhs d) || (not . isBodyExpression) _signBody
+  isLhsFunctionLike (functionDefLhs d) || (not . isBodyExpression) _signBody

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -353,7 +353,7 @@ getReservedDefinitionSymbol ::
 getReservedDefinitionSymbol s = do
   m <- gets (^. scopeLocalSymbols)
   let s' = fromMaybe err (m ^. at s)
-      err = error ("impossible. Contents of scope:\n" <> ppTrace (toList m))
+      err = impossibleError ("Symbol " <> ppTrace s <> " not found in the scope. Contents of scope:\n" <> ppTrace (toList m))
   return s'
 
 ignoreSyntax :: Sem (State ScoperSyntax ': r) a -> Sem r a
@@ -1070,10 +1070,12 @@ checkDeriving ::
   ) =>
   Deriving 'Parsed ->
   Sem r (Deriving 'Scoped)
-checkDeriving Deriving {..} = withLocalScope $ do
+checkDeriving Deriving {..} = do
   let lhs@FunctionLhs {..} = _derivingFunLhs
-  args' <- mapM checkSigArg _funLhsArgs
-  ret' <- mapM checkParseExpressionAtoms _funLhsRetType
+  (args', ret') <- withLocalScope $ do
+    args' <- mapM checkSigArg _funLhsArgs
+    ret' <- mapM checkParseExpressionAtoms _funLhsRetType
+    return (args', ret')
   name' <-
     if
         | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol _funLhsName
@@ -1085,7 +1087,6 @@ checkDeriving Deriving {..} = withLocalScope $ do
             _funLhsName = name',
             ..
           }
-
   return
     Deriving
       { _derivingFunLhs = lhs',

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -453,6 +453,22 @@ recoverStashes r = do
     put j
   return res
 
+derivingInstance ::
+  (Members '[ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) =>
+  ParsecS r (Deriving 'Parsed)
+derivingInstance = do
+  _derivingKw <- kw kwDeriving
+  let opts =
+        FunctionSyntaxOptions
+          { _funAllowOmitType = False,
+            _funAllowInstance = True
+          }
+  off <- P.getOffset
+  _derivingFunLhs <- functionDefinitionLhs opts Nothing
+  unless (isJust (_derivingFunLhs ^. funLhsInstance)) $
+    parseFailure off "Expected `deriving instance`"
+  return Deriving {..}
+
 statement :: (Members '[Error ParserError, ParserResultBuilder, PragmasStash, Error ParserError, JudocStash] r) => ParsecS r (Statement 'Parsed)
 statement = P.label "<top level statement>" $ do
   optional_ stashJudoc
@@ -465,6 +481,7 @@ statement = P.label "<top level statement>" $ do
   ms <-
     optional
       ( StatementImport <$> import_
+          <|> StatementDeriving <$> derivingInstance
           <|> StatementOpenModule <$> openModule
           <|> StatementSyntax <$> syntaxDef
           <|> StatementInductive <$> inductiveDef Nothing
@@ -1282,11 +1299,7 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
   unless (allowInstance || isNothing _funLhsCoercion) $
     parseFailure off "coercion not allowed here"
   off0 <- P.getOffset
-  _funLhsDeriving <- optional (kw kwDeriving)
-  _funLhsInstance <-
-    if
-        | isJust _funLhsDeriving -> Just <$> kw kwInstance
-        | otherwise -> optional (kw kwInstance)
+  _funLhsInstance <- optional (kw kwInstance)
   unless (allowInstance || isNothing _funLhsInstance) $
     parseFailure off0 "instance not allowed here"
   when (isJust _funLhsCoercion && isNothing _funLhsInstance) $

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -530,19 +530,21 @@ deriveEq ::
   [Internal.FunctionParameter] ->
   (Internal.InductiveName, [Internal.ApplicationArg]) ->
   Sem r Internal.FunctionDef
-deriveEq name funParams (eqName, args) = do
+deriveEq instanceName funParams (eqName, args) = do
   arg <- getArg
-  argsInfo <- goArgsInfo name
-  body <- eqLambda arg
-  let ty = Internal.foldFunType funParams (Internal.foldApplication (Internal.toExpression eqName) args)
+  argsInfo <- goArgsInfo instanceName
+  lam <- eqLambda arg
+  mkEq <- getBuiltin (getLoc eqName) BuiltinMkEq
+  let body = mkEq Internal.@@ lam
+      ty = Internal.foldFunType funParams (Internal.foldApplication (Internal.toExpression eqName) args)
   return
     Internal.FunctionDef
       { _funDefTerminating = False,
         _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance,
         _funDefPragmas = mempty,
         _funDefArgsInfo = argsInfo,
         _funDefDocComment = Nothing,
-        _funDefName = name,
+        _funDefName = instanceName,
         _funDefType = ty,
         _funDefBody = body,
         _funDefBuiltin = Nothing
@@ -558,12 +560,13 @@ deriveEq name funParams (eqName, args) = do
         err = error "TODO wrong form"
 
     {- \lambda {
-      (c1 x .. xn) (c1 y .. yn) -> x == y && .. xn == yn
+      (c1 x .. xn) (c1 y .. yn) -> x == y && .. && xn == yn
       ..
      }
     -}
     eqLambda :: Internal.InductiveInfo -> Sem r Internal.Expression
     eqLambda d = do
+      let loc = getLoc eqName
       band <- getBuiltin loc BuiltinBoolAnd
       btrue <- getBuiltin loc BuiltinBoolTrue
       bisEqual <- getBuiltin loc BuiltinIsEqual
@@ -579,7 +582,6 @@ deriveEq name funParams (eqName, args) = do
                   }
             )
       where
-        loc = getLoc d
         lambdaClause ::
           Internal.FunctionName ->
           Internal.FunctionName ->
@@ -589,7 +591,7 @@ deriveEq name funParams (eqName, args) = do
         lambdaClause band btrue bisEqual c = do
           numArgs :: Int <- getNumArgs
           let mkpat = do
-                xs <- mapM (Internal.freshVar loc) (Stream.take numArgs allWords)
+                xs <- mapM (Internal.freshVar (getLoc instanceName)) (Stream.take numArgs allWords)
                 return (xs, Internal.mkConstructorVarPattern Explicit c ((Explicit,) <$> xs))
           (v1, p1) <- mkpat
           (v2, p2) <- mkpat

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs

@@ -52,25 +52,32 @@ newtype LhsTooManyPatterns = LhsTooManyPatterns
 makeLenses ''LhsTooManyPatterns
 
 instance ToGenericError LhsTooManyPatterns where
-  genericError e =
-    return
-      GenericError
-        { _genericErrorLoc = i,
-          _genericErrorMessage = ppOutput msg,
-          _genericErrorIntervals = [i]
-        }
+  genericError e = genErr <$> ask
     where
-      i = getLocSpan (e ^. lhsTooManyPatternsRemaining)
-      n = length (e ^. lhsTooManyPatternsRemaining)
-      howMany =
-        "The last" <+> case n of
-          1 -> "pattern"
-          _ -> pretty n <+> "patterns"
-      msg =
-        howMany <+> "on the left hand side of the function clause" <+> wasWere <+> "not expected"
-      wasWere
-        | n == 1 = "was"
-        | otherwise = "were"
+      genErr opts =
+        GenericError
+          { _genericErrorLoc = i,
+            _genericErrorMessage = ppOutput msg,
+            _genericErrorIntervals = [i]
+          }
+        where
+          opts' = fromGenericOptions opts
+          i = getLocSpan (e ^. lhsTooManyPatternsRemaining)
+          n = length (e ^. lhsTooManyPatternsRemaining)
+          howMany =
+            "The last" <+> case n of
+              1 -> "pattern"
+              _ -> pretty n <+> "patterns"
+          msg =
+            howMany
+              <+> "on the left hand side of the function clause"
+              <+> wasWere
+              <+> "not expected"
+                <> line
+                <> itemize (ppCode opts' <$> (e ^. lhsTooManyPatternsRemaining))
+          wasWere
+            | n == 1 = "was"
+            | otherwise = "were"
 
 data WrongPatternIsImplicit = WrongPatternIsImplicit
   { _wrongPatternIsImplicitExpected :: IsImplicit,