Error for an instance subsumed by other instances

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -214,14 +214,17 @@ checkDefType ty = checkIsType loc ty
 
 checkInstanceType ::
   forall r.
-  (Members '[Error TypeCheckerError, Reader InfoTable] r) =>
+  (Members '[Error TypeCheckerError, Reader InfoTable, Inference] r) =>
   FunctionDef ->
   Sem r ()
 checkInstanceType FunctionDef {..} = case mi of
   Just ii@InstanceInfo {..} -> do
     tab <- ask
     unless (isTrait tab _instanceInfoInductive) $
       throw (ErrTargetNotATrait (TargetNotATrait _funDefType))
+    is <- map fst <$> subsumingInstances (tab ^. infoInstances) ii
+    unless (null is) $
+      throw (ErrSubsumedInstance (SubsumedInstance ii is (getLoc _funDefName)))
     let metaVars = HashSet.fromList $ mapMaybe (^. paramName) _instanceInfoArgs
     mapM_ (checkArg tab metaVars ii) _instanceInfoArgs
   Nothing ->

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs

@@ -28,6 +28,7 @@ data TypeCheckerError
   | ErrNotATrait NotATrait
   | ErrNoInstance NoInstance
   | ErrAmbiguousInstances AmbiguousInstances
+  | ErrSubsumedInstance SubsumedInstance
   | ErrExplicitInstanceArgument ExplicitInstanceArgument
   | ErrTraitNotTerminating TraitNotTerminating
 
@@ -50,5 +51,6 @@ instance ToGenericError TypeCheckerError where
     ErrNotATrait e -> genericError e
     ErrNoInstance e -> genericError e
     ErrAmbiguousInstances e -> genericError e
+    ErrSubsumedInstance e -> genericError e
     ErrExplicitInstanceArgument e -> genericError e
     ErrTraitNotTerminating e -> genericError e

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

@@ -464,6 +464,35 @@ instance ToGenericError AmbiguousInstances where
                 <> line
                 <> indent' locs
 
+data SubsumedInstance = SubsumedInstance
+  { _subsumedInstance :: InstanceInfo,
+    _subsumedInstanceParents :: [InstanceInfo],
+    _subsumedInstanceLoc :: Interval
+  }
+
+makeLenses ''SubsumedInstance
+
+instance ToGenericError SubsumedInstance where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [i]
+            }
+        where
+          opts' = fromGenericOptions opts
+          i = e ^. subsumedInstanceLoc
+          locs = itemize $ map (pretty . getLoc . (^. instanceInfoResult)) (e ^. subsumedInstanceParents)
+          msg =
+            "The instance"
+              <+> ppCode opts' (e ^. subsumedInstance . instanceInfoResult)
+              <+> "is subsumed by instances at:"
+                <> line
+                <> indent' locs
+
 newtype ExplicitInstanceArgument = ExplicitInstanceArgument
   { _explicitInstanceArgumentParameter :: FunctionParameter
   }

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs

@@ -78,11 +78,12 @@ expandArity loc subs params e = case params of
 lookupInstance' ::
   forall r.
   (Member Inference r) =>
+  Bool ->
   InstanceTable ->
   Name ->
   [InstanceParam] ->
   Sem r [(InstanceInfo, SubsI)]
-lookupInstance' tab name params = do
+lookupInstance' canFillHoles tab name params = do
   let is = fromMaybe [] $ lookupInstanceTable tab name
   mapMaybeM matchInstance is
   where
@@ -111,13 +112,16 @@ lookupInstance' tab name params = do
       (InstanceParamVar v1, InstanceParamVar v2)
         | v1 == v2 ->
             return True
-      (InstanceParamHole h, _) -> do
-        m <- matchTypes (ExpressionHole h) (paramToExpression t)
-        case m of
-          Just {} -> return False
-          Nothing -> return True
+      (InstanceParamHole h, _)
+        | canFillHoles -> do
+            m <- matchTypes (ExpressionHole h) (paramToExpression t)
+            case m of
+              Just {} -> return False
+              Nothing -> return True
+        | otherwise ->
+            return False
       (_, InstanceParamHole h)
-        | checkNoMeta pat -> do
+        | canFillHoles && checkNoMeta pat -> do
             m <- matchTypes (paramToExpression pat) (ExpressionHole h)
             case m of
               Just {} -> return False
@@ -137,10 +141,21 @@ lookupInstance ::
 lookupInstance tab ty = do
   case traitFromExpression mempty ty of
     Just InstanceApp {..} ->
-      lookupInstance' tab _instanceAppHead _instanceAppArgs
+      lookupInstance' True tab _instanceAppHead _instanceAppArgs
     _ ->
       throw (ErrNotATrait (NotATrait ty))
 
+subsumingInstances ::
+  forall r.
+  (Members '[Error TypeCheckerError, Inference] r) =>
+  InstanceTable ->
+  InstanceInfo ->
+  Sem r [(InstanceInfo, SubsI)]
+subsumingInstances tab InstanceInfo {..} = do
+  is <- lookupInstance' False tab _instanceInfoInductive _instanceInfoParams
+  return $
+    filter (\(x, _) -> x ^. instanceInfoResult /= _instanceInfoResult) is
+
 instanceFromTypedExpression' :: InfoTable -> TypedExpression -> Maybe InstanceInfo
 instanceFromTypedExpression' tbl e = do
   ii@InstanceInfo {..} <- instanceFromTypedExpression e

test/Typecheck/Negative.hs

@@ -181,6 +181,13 @@ tests =
       $ \case
         ErrAmbiguousInstances {} -> Nothing
         _ -> wrongError,
+    NegTest
+      "Subsumed instance"
+      $(mkRelDir "Internal")
+      $(mkRelFile "SubsumedInstance.juvix")
+      $ \case
+        ErrSubsumedInstance {} -> Nothing
+        _ -> wrongError,
     NegTest
       "Explicit instance argument"
       $(mkRelDir "Internal")

tests/negative/Internal/AmbiguousInstances.juvix

@@ -2,21 +2,21 @@ module AmbiguousInstances;
 
 type Unit := unit;
 
-type Box A := box A;
+type Box A B := box A B;
 
 trait
 type T A := mkT { pp : A → A };
 
 instance
 unitT : T Unit := mkT (pp := λ{_ := unit});
 
-ppBox {A} {{T A}} : Box A → Box A
-  | (box x) := box (T.pp x);
+ppBox {A B} {{T A}} : Box A B → Box A B
+  | (box x y) := box (T.pp x) y;
 
 instance
-boxT {A} {{T A}} : T (Box A) := mkT (pp := ppBox);
+boxT {A} {{T A}} : T (Box A Unit) := mkT (pp := ppBox);
 
 instance
-boxTUnit : T (Box Unit) := mkT (pp := λ{x := x});
+boxTUnit {B} : T (Box Unit B) := mkT (pp := λ{x := x});
 
-main : Box Unit := T.pp (box unit);
+main : Box Unit Unit := T.pp (box unit unit);

tests/negative/Internal/SubsumedInstance.juvix

@@ -0,0 +1,22 @@
+module SubsumedInstance;
+
+type Unit := unit;
+
+type Box A := box A;
+
+trait
+type T A := mkT { pp : A → A };
+
+instance
+unitT : T Unit := mkT (pp := λ{_ := unit});
+
+ppBox {A} {{T A}} : Box A → Box A
+  | (box x) := box (T.pp x);
+
+instance
+boxT {A} {{T A}} : T (Box A) := mkT (pp := ppBox);
+
+instance
+boxTUnit : T (Box Unit) := mkT (pp := λ{x := x});
+
+main : Box Unit := T.pp (box unit);