Make meta-variables introduced by coercion resolution non-rigid (#3290)

* Closes #3283 
* If a meta-variable of a coercion does not occur on the right, it is
introduced as a non-rigid meta-variable that can be substituted in
subsequent instance search.

---------

Co-authored-by: Jan Mas Rovira <[email protected]>

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

@@ -25,6 +25,26 @@ updateInstanceTable tab ii@InstanceInfo {..} =
 lookupInstanceTable :: InstanceTable -> Name -> Maybe [InstanceInfo]
 lookupInstanceTable tab name = HashMap.lookup name (tab ^. instanceTableMap)
 
+makeRigidParam :: InstanceParam -> InstanceParam
+makeRigidParam p = case p of
+  InstanceParamVar {} ->
+    p
+  InstanceParamApp app@InstanceApp {..} ->
+    InstanceParamApp $
+      app
+        { _instanceAppArgs = map makeRigidParam _instanceAppArgs
+        }
+  InstanceParamFun fn@InstanceFun {..} ->
+    InstanceParamFun $
+      fn
+        { _instanceFunLeft = makeRigidParam _instanceFunLeft,
+          _instanceFunRight = makeRigidParam _instanceFunRight
+        }
+  InstanceParamHole {} ->
+    p
+  InstanceParamMeta v ->
+    InstanceParamVar v
+
 paramToExpression :: InstanceParam -> Expression
 paramToExpression = \case
   InstanceParamVar v ->

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -14,6 +14,7 @@ import Juvix.Compiler.Internal.Pretty.Options
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New
 import Juvix.Compiler.Store.Internal.Data.InfoTable
+import Juvix.Compiler.Store.Internal.Data.InstanceInfo
 import Juvix.Data.CodeAnn
 import Juvix.Data.Keyword.All qualified as Kw
 import Juvix.Prelude
@@ -39,6 +40,26 @@ instance PrettyCode Name where
     showNameId <- asks (^. optShowNameIds)
     return (prettyName showNameId n)
 
+instance PrettyCode InstanceFun where
+  ppCode InstanceFun {..} = do
+    l' <- ppCode _instanceFunLeft
+    r' <- ppCode _instanceFunRight
+    return $ l' <+> kwArrow <+> r'
+
+instance PrettyCode InstanceApp where
+  ppCode InstanceApp {..} = do
+    h' <- ppCode _instanceAppHead
+    args' <- mapM ppCode _instanceAppArgs
+    return $ h' <+> hsep args'
+
+instance PrettyCode InstanceParam where
+  ppCode = \case
+    InstanceParamVar v -> ppCode v
+    InstanceParamApp a -> ppCode a
+    InstanceParamFun f -> ppCode f
+    InstanceParamHole h -> ppCode h
+    InstanceParamMeta m -> ppCode m
+
 instance PrettyCode DerivingTrait where
   ppCode = return . ppCodeAnn
 

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

@@ -58,7 +58,7 @@ subsumingInstances ::
   InstanceInfo ->
   Sem r [(InstanceInfo)]
 subsumingInstances tab InstanceInfo {..} = do
-  is <- lookupInstance' [] False mempty tab _instanceInfoInductive _instanceInfoParams
+  is <- lookupInstance' [] False mempty tab _instanceInfoInductive (map makeRigidParam _instanceInfoParams)
   return $
     map snd3 $
       filter (\(_, x, _) -> x ^. instanceInfoResult /= _instanceInfoResult) is
@@ -226,22 +226,15 @@ lookupInstance' visited canFillHoles ctab tab name params
 
     goMatch :: InstanceParam -> InstanceParam -> Sem (State SubsI ': Fail ': r) Bool
     goMatch pat t = case (pat, t) of
-      (InstanceParamMeta v, _) -> do
-        m <- gets (HashMap.lookup v)
-        case m of
-          Just t'
-            | t' == t ->
-                return True
-            | otherwise ->
-                return False
-          Nothing -> do
-            modify (HashMap.insert v t)
-            return True
+      (InstanceParamMeta v, _) ->
+        goMatchMeta v t
+      (_, InstanceParamMeta v) ->
+        goMatchMeta v pat
       (InstanceParamVar v1, InstanceParamVar v2)
         | v1 == v2 ->
             return True
       (InstanceParamHole h, _)
-        | canFillHoles -> do
+        | canFillHoles && checkNoMeta t -> do
             m <- matchTypes (ExpressionHole h) (paramToExpression t)
             case m of
               Just {} -> return False
@@ -265,6 +258,16 @@ lookupInstance' visited canFillHoles ctab tab name params
       (InstanceParamApp {}, _) -> return False
       (InstanceParamFun {}, _) -> return False
 
+    goMatchMeta :: VarName -> InstanceParam -> Sem (State SubsI ': Fail ': r) Bool
+    goMatchMeta v t = do
+      m <- gets (HashMap.lookup v)
+      case m of
+        Just t' ->
+          return (t' == t)
+        Nothing -> do
+          modify (HashMap.insert v t)
+          return True
+
 lookupInstance ::
   forall r.
   (Members '[Error TypeCheckerError, Inference, NameIdGen] r) =>

tests/Compilation/positive/out/test063.out

@@ -6,3 +6,4 @@ e
 f
 g
 h
+a

tests/Compilation/positive/test063.juvix

@@ -75,6 +75,33 @@ g {A} {{U1 A}} : A -> A := f;
 
 h {A} {{U2 A}} : A -> A := f;
 
+trait
+type W1 A := mkW1;
+
+trait
+type W2 A B := mkW2;
+
+coercion instance
+fromW2toW1 {A B} {{W2 A B}} : W1 A := mkW1;
+
+instance
+instW2 : W2 String Nat := mkW2;
+
+wid {A} {{W1 A}} : A -> A := id;
+
+trait
+type T A B := mkT;
+
+instance
+inst1 {A} : T A String := mkT;
+
+instance
+inst2 {B} : T String B := mkT;
+
+idT {{T String Nat}} : String -> String := id;
+
+idT' {{T String String}} : String -> String := id;
+
 main : IO :=
   printStringLn (T1.pp "a")
     >>> printStringLn (T2.pp "b")
@@ -83,4 +110,5 @@ main : IO :=
     >>> printStringLn (U.pp "e")
     >>> printStringLn (f "f")
     >>> printStringLn (g {{mkU1 id}} "g")
-    >>> printStringLn (h "h");
+    >>> printStringLn (h "h")
+    >>> printStringLn (wid (idT "a"));