Refine hole in type signature to function type (#1379)

* infer hole in type from pattern

* Refine hole in signature when patterns are found

* fix

src/Juvix/Syntax/MicroJuvix/Error/Types.hs

@@ -9,8 +9,8 @@ import Juvix.Syntax.MicroJuvix.Language
 -- not match the type of the inductive being matched
 data WrongConstructorType = WrongConstructorType
   { _wrongCtorTypeName :: Name,
-    _wrongCtorTypeExpected :: Name,
-    _wrongCtorTypeActual :: Name,
+    _wrongCtorTypeExpected :: InductiveName,
+    _wrongCtorTypeActual :: InductiveName,
     _wrongCtorTypeFunName :: Name
   }
 

src/Juvix/Syntax/MicroJuvix/Language/Extra.hs

@@ -8,6 +8,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Juvix.Prelude
 import Juvix.Syntax.MicroJuvix.Language
+import Juvix.Syntax.MicroJuvix.LocalVars
 
 data Caller
   = CallerInductive InductiveName
@@ -192,7 +193,12 @@ typeAbstraction :: IsImplicit -> Name -> FunctionParameter
 typeAbstraction i var = FunctionParameter (Just var) i (ExpressionUniverse (SmallUniverse (getLoc var)))
 
 unnamedParameter :: Expression -> FunctionParameter
-unnamedParameter = FunctionParameter Nothing Explicit
+unnamedParameter ty =
+  FunctionParameter
+    { _paramName = Nothing,
+      _paramImplicit = Explicit,
+      _paramType = ty
+    }
 
 renameToSubsE :: Rename -> SubsE
 renameToSubsE = fmap (ExpressionIden . IdenVar)
@@ -272,6 +278,9 @@ substitutionApp (mv, ty) = case mv of
   Nothing -> id
   Just v -> substitutionE (HashMap.singleton v ty)
 
+localsToSubsE :: LocalVars -> SubsE
+localsToSubsE l = ExpressionIden . IdenVar <$> l ^. localTyMap
+
 substitutionE :: SubsE -> Expression -> Expression
 substitutionE m = go
   where

src/Juvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -89,7 +89,7 @@ checkFunctionDefType :: forall r. Members '[Inference] r => Expression -> Sem r
 checkFunctionDefType = traverseOf_ (leafExpressions . _ExpressionHole) go
   where
     go :: Hole -> Sem r ()
-    go h = void (freshMetavar h)
+    go h = freshMetavar h
 
 checkExpression ::
   Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
@@ -138,38 +138,45 @@ checkFunctionClauseBody locals expectedTy body =
   runReader locals (checkExpression expectedTy body)
 
 checkFunctionClause ::
+  forall r.
   Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, Inference] r =>
   FunctionInfo ->
   FunctionClause ->
   Sem r FunctionClause
 checkFunctionClause info FunctionClause {..} = do
-  let (argTys, rty) = unfoldFunType (info ^. functionInfoDef . funDefType)
-      (patTys, restTys) = splitAt (length _clausePatterns) argTys
-      bodyTy = foldFunType restTys rty
-  if
-      | length patTys /= length _clausePatterns -> impossible
-      | otherwise -> do
-          locals <- checkPatterns _clauseName (zipExact patTys _clausePatterns)
-          let bodyTy' =
-                substitutionE
-                  ( fmap
-                      (ExpressionIden . IdenVar)
-                      (locals ^. localTyMap)
-                  )
-                  bodyTy
-          _clauseBody' <- checkFunctionClauseBody locals bodyTy' _clauseBody
-          return
-            FunctionClause
-              { _clauseBody = _clauseBody',
-                ..
-              }
-
-checkPatterns ::
-  Members '[Reader InfoTable, Error TypeCheckerError, Inference, NameIdGen] r =>
-  FunctionName ->
-  [(FunctionParameter, Pattern)] ->
-  Sem r LocalVars
-checkPatterns name = execState emptyLocalVars . mapM_ (uncurry (checkPattern name))
+  (locals, bodyTy) <- helper _clausePatterns clauseType
+  let bodyTy' = substitutionE (localsToSubsE locals) bodyTy
+  _clauseBody' <- checkFunctionClauseBody locals bodyTy' _clauseBody
+  return
+    FunctionClause
+      { _clauseBody = _clauseBody',
+        ..
+      }
+  where
+    clauseType :: Expression
+    clauseType = info ^. functionInfoDef . funDefType
+    helper :: [Pattern] -> Expression -> Sem r (LocalVars, Expression)
+    helper pats ty = runState emptyLocalVars (go pats ty)
+    go :: [Pattern] -> Expression -> Sem (State LocalVars ': r) Expression
+    go pats bodyTy = case pats of
+      [] -> return bodyTy
+      (p : ps) -> case bodyTy of
+        ExpressionHole h -> do
+          s <- queryMetavar h
+          case s of
+            Just h' -> go pats h'
+            Nothing -> do
+              freshMetavar h
+              l <- ExpressionHole <$> freshHole (getLoc h)
+              r <- ExpressionHole <$> freshHole (getLoc h)
+              let fun = ExpressionFunction (Function (unnamedParameter l) r)
+              whenJustM (matchTypes (ExpressionHole h) fun) impossible
+              go pats fun
+        _ -> case unfoldFunType bodyTy of
+          ([], _) -> error "too many patterns"
+          (par : pars, ret) -> do
+            checkPattern _clauseName par p
+            go ps (foldFunType pars ret)
 
 typeOfArg :: FunctionParameter -> Expression
 typeOfArg = (^. paramType)
@@ -303,7 +310,7 @@ freshHole :: Members '[Inference, NameIdGen] r => Interval -> Sem r Hole
 freshHole l = do
   uid <- freshNameId
   let h = Hole uid l
-  void (freshMetavar h)
+  freshMetavar h
   return h
 
 -- | Returns {A : Expression} → A
@@ -345,9 +352,18 @@ inferExpression' e = case e of
   ExpressionApplication a -> inferApplication a
   ExpressionLiteral l -> goLiteral l
   ExpressionFunction f -> goExpressionFunction f
-  ExpressionHole h -> freshMetavar h
+  ExpressionHole h -> inferHole h
   ExpressionUniverse u -> goUniverse u
   where
+    inferHole :: Hole -> Sem r TypedExpression
+    inferHole h = do
+      freshMetavar h
+      return
+        TypedExpression
+          { _typedExpression = ExpressionHole h,
+            _typedType = ExpressionUniverse (SmallUniverse (getLoc h))
+          }
+
     goUniverse :: SmallUniverse -> Sem r TypedExpression
     goUniverse u =
       return

src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs

@@ -18,7 +18,6 @@ data MatchError = MatchError
 makeLenses ''MatchError
 
 data Inference m a where
-  FreshMetavar :: Hole -> Inference m TypedExpression
   MatchTypes :: Expression -> Expression -> Inference m (Maybe MatchError)
   QueryMetavar :: Hole -> Inference m (Maybe Expression)
   NormalizeType :: Expression -> Inference m Expression
@@ -93,29 +92,25 @@ normalizeType' = go
         Fresh -> return (ExpressionHole h)
         Refined r -> go r
 
+freshMetavar :: Members '[Inference] r => Hole -> Sem r ()
+freshMetavar = void . queryMetavar
+
+queryMetavar' :: Members '[State InferenceState] r => Hole -> Sem r (Maybe Expression)
+queryMetavar' h = do
+  m <- gets (^. inferenceMap . at h)
+  case m of
+    Nothing -> do
+      modify (over inferenceMap (HashMap.insert h Fresh))
+      return Nothing
+    Just Fresh -> return Nothing
+    Just (Refined e) -> return (Just e)
+
 re :: Member (Error TypeCheckerError) r => Sem (Inference ': r) a -> Sem (State InferenceState ': r) a
 re = reinterpret $ \case
-  FreshMetavar h -> freshMetavar' h
   MatchTypes a b -> matchTypes' a b
   QueryMetavar h -> queryMetavar' h
   NormalizeType t -> normalizeType' t
   where
-    queryMetavar' :: Members '[State InferenceState] r => Hole -> Sem r (Maybe Expression)
-    queryMetavar' h = do
-      s <- getMetavar h
-      case s of
-        Fresh -> return Nothing
-        Refined t -> return (Just t)
-
-    freshMetavar' :: Members '[State InferenceState] r => Hole -> Sem r TypedExpression
-    freshMetavar' h = do
-      modify (over inferenceMap (HashMap.insert h Fresh))
-      return
-        TypedExpression
-          { _typedExpression = ExpressionHole h,
-            _typedType = ExpressionUniverse (SmallUniverse (getLoc h))
-          }
-
     refineFreshMetavar ::
       Members '[Error TypeCheckerError, State InferenceState] r =>
       Hole ->

test/TypeCheck/Positive.hs

@@ -87,6 +87,10 @@ tests =
       "Implicit arguments"
       "MicroJuvix"
       "Implicit.juvix",
+    PosTest
+      "Refine hole in type signature"
+      "272"
+      "M.juvix",
     PosTest
       "Pattern match a hole type"
       "265"

tests/positive/272/M.juvix

@@ -0,0 +1,28 @@
+module M;
+
+inductive Bool {
+  false : Bool;
+  true : Bool;
+};
+
+inductive T {
+t : T;
+};
+
+inductive Nat {
+  zero : Nat;
+  suc : Nat → Nat;
+};
+
+f : _;
+f false false ≔ true;
+f true _ ≔ false;
+
+inductive Pair (A : Type) (B : Type) {
+  mkPair : A → B → Pair A B;
+};
+
+g : _;
+g (mkPair (mkPair zero false) true) ≔ mkPair false zero;
+
+end;