Treat holes as non-rigid meta-variables during instance search

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

@@ -45,18 +45,18 @@ makeRigidParam p = case p of
   InstanceParamMeta v ->
     InstanceParamVar v
 
-paramToExpression :: InstanceParam -> Expression
+paramToExpression :: (Member NameIdGen r) => InstanceParam -> Sem r Expression
 paramToExpression = \case
   InstanceParamVar v ->
-    ExpressionIden (IdenVar v)
+    return $ ExpressionIden (IdenVar v)
   InstanceParamApp InstanceApp {..} ->
-    _instanceAppExpression
+    return _instanceAppExpression
   InstanceParamFun InstanceFun {..} ->
-    _instanceFunExpression
+    return _instanceFunExpression
   InstanceParamHole h ->
-    ExpressionHole h
+    return $ ExpressionHole h
   InstanceParamMeta v ->
-    ExpressionIden (IdenVar v)
+    ExpressionHole . mkHole (getLoc v) <$> freshNameId
 
 paramFromExpression :: HashSet VarName -> Expression -> Maybe InstanceParam
 paramFromExpression metaVars e = case e of

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

@@ -19,8 +19,8 @@ import Juvix.Prelude
 
 type SubsI = HashMap VarName InstanceParam
 
-subsIToE :: SubsI -> Subs
-subsIToE = fmap paramToExpression
+subsIToE :: (Member NameIdGen r) => SubsI -> Sem r Subs
+subsIToE = mapM paramToExpression
 
 type CoercionChain = [(CoercionInfo, SubsI)]
 
@@ -41,8 +41,9 @@ resolveTraitInstance TypedHole {..} = do
   ty <- strongNormalize _typedHoleType
   is <- lookupInstance ctab tab (ty ^. normalizedExpression)
   case is of
-    [(cs, ii, subs)] ->
-      expandArity' loc (subsIToE subs) (ii ^. instanceInfoArgs) (ii ^. instanceInfoResult)
+    [(cs, ii, subs)] -> do
+      subs' <- subsIToE subs
+      expandArity' loc subs' (ii ^. instanceInfoArgs) (ii ^. instanceInfoResult)
         >>= applyCoercions loc cs
     [] ->
       throw (ErrNoInstance (NoInstance ty loc))
@@ -58,7 +59,7 @@ subsumingInstances ::
   InstanceInfo ->
   Sem r [(InstanceInfo)]
 subsumingInstances tab InstanceInfo {..} = do
-  is <- lookupInstance' [] False mempty tab _instanceInfoInductive (map makeRigidParam _instanceInfoParams)
+  is <- lookupInstance' [] mempty tab _instanceInfoInductive (map makeRigidParam _instanceInfoParams)
   return $
     map snd3 $
       filter (\(_, x, _) -> x ^. instanceInfoResult /= _instanceInfoResult) is
@@ -72,7 +73,8 @@ substitutionI subs p = case p of
   InstanceParamVar {} -> return p
   InstanceParamApp InstanceApp {..} -> do
     args <- mapM (substitutionI subs) _instanceAppArgs
-    e <- substitutionE (subsIToE subs) _instanceAppExpression
+    subs' <- subsIToE subs
+    e <- substitutionE subs' _instanceAppExpression
     return $
       InstanceParamApp
         InstanceApp
@@ -83,15 +85,21 @@ substitutionI subs p = case p of
   InstanceParamFun InstanceFun {..} -> do
     l <- substitutionI subs _instanceFunLeft
     r <- substitutionI subs _instanceFunRight
-    e <- substitutionE (subsIToE subs) _instanceFunExpression
+    subs' <- subsIToE subs
+    e <- substitutionE subs' _instanceFunExpression
     return $
       InstanceParamFun
         InstanceFun
           { _instanceFunLeft = l,
             _instanceFunRight = r,
             _instanceFunExpression = e
           }
-  InstanceParamHole {} -> return p
+  InstanceParamHole h
+    | Just p' <- HashMap.lookup (varFromHole h) subs ->
+        -- we don't need to clone here because `InstanceParam` doesn't have binders
+        return p'
+    | otherwise ->
+        return p
   InstanceParamMeta v
     | Just p' <- HashMap.lookup v subs ->
         -- we don't need to clone here because `InstanceParam` doesn't have binders
@@ -134,7 +142,8 @@ applyCoercion ::
   Expression ->
   Sem r Expression
 applyCoercion loc (CoercionInfo {..}, subs) e = do
-  e' <- expandArity' loc (subsIToE subs) _coercionInfoArgs _coercionInfoResult
+  subs' <- subsIToE subs
+  e' <- expandArity' loc subs' _coercionInfoArgs _coercionInfoResult
   return $
     ExpressionApplication (Application e' e ImplicitInstance)
 
@@ -180,15 +189,14 @@ expandArity loc subs params e = case params of
 
 lookupInstance' ::
   forall r.
-  (Members '[Inference, NameIdGen] r) =>
+  (Members '[NameIdGen] r) =>
   [Name] ->
-  Bool ->
   CoercionTable ->
   InstanceTable ->
   Name ->
   [InstanceParam] ->
   Sem r [(CoercionChain, InstanceInfo, SubsI)]
-lookupInstance' visited canFillHoles ctab tab name params
+lookupInstance' visited ctab tab name params
   | name `elem` visited = return []
   | otherwise = do
       let is = fromMaybe [] $ lookupInstanceTable tab name
@@ -221,7 +229,7 @@ lookupInstance' visited canFillHoles ctab tab name params
             if
                 | _coercionInfoDecreasing -> visited
                 | otherwise -> name : visited
-      is <- lookupInstance' visited' canFillHoles ctab tab name' args'
+      is <- lookupInstance' visited' ctab tab name' args'
       return $ map (first3 ((ci, si) :)) is
 
     goMatch :: InstanceParam -> InstanceParam -> Sem (State SubsI ': Fail ': r) Bool
@@ -230,23 +238,11 @@ lookupInstance' visited canFillHoles ctab tab name params
         goMatchMeta v t
       (_, InstanceParamMeta v) ->
         goMatchMeta v pat
+      (_, InstanceParamHole h) ->
+        goMatchMeta (varFromHole h) pat
       (InstanceParamVar v1, InstanceParamVar v2)
         | v1 == v2 ->
             return True
-      (InstanceParamHole h, _)
-        | canFillHoles && checkNoMeta t -> do
-            m <- matchTypes (ExpressionHole h) (paramToExpression t)
-            case m of
-              Just {} -> return False
-              Nothing -> return True
-        | otherwise ->
-            return False
-      (_, InstanceParamHole h)
-        | canFillHoles && checkNoMeta pat -> do
-            m <- matchTypes (paramToExpression pat) (ExpressionHole h)
-            case m of
-              Just {} -> return False
-              Nothing -> return True
       (InstanceParamApp app1, InstanceParamApp app2)
         | app1 ^. instanceAppHead == app2 ^. instanceAppHead -> do
             and <$> sequence (zipWithExact goMatch (app1 ^. instanceAppArgs) (app2 ^. instanceAppArgs))
@@ -257,13 +253,14 @@ lookupInstance' visited canFillHoles ctab tab name params
       (InstanceParamVar {}, _) -> return False
       (InstanceParamApp {}, _) -> return False
       (InstanceParamFun {}, _) -> return False
+      (InstanceParamHole {}, _) -> 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)
+          goMatch t' t
         Nothing -> do
           modify (HashMap.insert v t)
           return True
@@ -278,6 +275,6 @@ lookupInstance ::
 lookupInstance ctab tab ty =
   case traitFromExpression mempty ty of
     Just InstanceApp {..} ->
-      lookupInstance' [] False ctab tab _instanceAppHead _instanceAppArgs
+      lookupInstance' [] ctab tab _instanceAppHead _instanceAppArgs
     _ ->
       return []

tests/Compilation/positive/out/test061.out

@@ -14,3 +14,4 @@ abba3
 a :: b :: c :: d :: nil
 \{ true := false | false := true }
 3, 1 :: 2 :: nil
+6

tests/Compilation/positive/test061.juvix

@@ -104,4 +104,9 @@ 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 + T.a 0]));
+    >>> printStringLn (Show.show (3, [1; 2 + T.a 0]))
+    >>> (for (acc := 0) ((x, _) in [1, 1; 2, 2; 3, 3]) {
+          acc + x
+         }
+         |> Show.show
+         |> printStringLn);

tests/Compilation/positive/test091.juvix

@@ -233,7 +233,7 @@ Identity-Monad : Monad Identity :=
 
 readAndAdd {E : Type -> Type} {{Monad E}} {{Reader Nat E}} {{State Nat E}} : E Nat :=
   do {
-    s <- Reader.ask {Nat};
+    s <- Reader.ask;
     modify ((+) s);
     State.get
   };