Fix bug in instance termination checking (#2423)

* Closes #2421

src/Juvix/Compiler/Internal/Data/InstanceInfo.hs

@@ -82,9 +82,10 @@ paramToExpression = \case
     _instanceAppExpression
   InstanceParamFun InstanceFun {..} ->
     _instanceFunExpression
-  InstanceParamHole h -> ExpressionHole h
-  InstanceParamMeta {} ->
-    impossible
+  InstanceParamHole h ->
+    ExpressionHole h
+  InstanceParamMeta v ->
+    ExpressionIden (IdenVar v)
 
 paramFromExpression :: HashSet VarName -> Expression -> Maybe InstanceParam
 paramFromExpression metaVars e = case e of

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

@@ -27,6 +27,9 @@ checkStrictSubterm :: InstanceParam -> InstanceParam -> Bool
 checkStrictSubterm p1 p2 = case p2 of
   InstanceParamApp InstanceApp {..} ->
     any (checkSubterm p1) _instanceAppArgs
+  InstanceParamFun InstanceFun {..} ->
+    checkSubterm p1 _instanceFunLeft
+      || checkSubterm p1 _instanceFunRight
   _ ->
     False
 

tests/Compilation/positive/test061.juvix

@@ -66,6 +66,15 @@ instance
 showPairI {A B} {{Show A}} {{Show B}} : Show (A × B) :=
   mkShow λ {(x, y) := Show.show x ++str ", " ++str Show.show y};
 
+trait
+type T A := mkT { a : A };
+
+instance
+tNatI : T Nat := mkT 0;
+
+instance
+tFunI {A} {{T A}} : T (A -> A) := mkT \ { a := a };
+
 main : IO :=
   printStringLn (Show.show true) >>
   printStringLn (f false) >>
@@ -82,4 +91,4 @@ main : IO :=
   printStringLn (f5 "abba" 3) >>
   printStringLn (Show.show {{_}} ["a"; "b"; "c"; "d"]) >>
   printStringLn (Show.show (λ{x := not x})) >>
-  printStringLn (Show.show (3, [1; 2]));
+  printStringLn (Show.show (3, [1; 2 + T.a 0]));