140 Support holes in type signatures (#141)

src/MiniJuvix/Syntax/MicroJuvix/Error.hs

@@ -14,8 +14,8 @@ data TypeCheckerError
   | ErrWrongConstructorType WrongConstructorType
   | ErrWrongConstructorAppArgs WrongConstructorAppArgs
   | ErrWrongType WrongType
+  | ErrUnsolvedMeta UnsolvedMeta
   | ErrExpectedFunctionType ExpectedFunctionType
-  deriving stock (Show)
 
 instance ToGenericError TypeCheckerError where
   genericError :: TypeCheckerError -> GenericError
@@ -24,4 +24,5 @@ instance ToGenericError TypeCheckerError where
     ErrWrongConstructorType e -> genericError e
     ErrWrongConstructorAppArgs e -> genericError e
     ErrWrongType e -> genericError e
+    ErrUnsolvedMeta e -> genericError e
     ErrExpectedFunctionType e -> genericError e

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

@@ -35,6 +35,24 @@ instance ToGenericError WrongConstructorType where
           <> line
           <> indent' (ppCode (e ^. wrongCtorTypeExpected))
 
+newtype UnsolvedMeta = UnsolvedMeta
+  { _unsolvedMeta :: Hole
+  }
+
+makeLenses ''UnsolvedMeta
+
+instance ToGenericError UnsolvedMeta where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      i = getLoc (e ^. unsolvedMeta)
+      msg :: Doc a
+      msg = "Unable to infer the hole"
+
 -- | The arguments of a constructor pattern do not match
 -- the expected arguments of the constructor
 data WrongConstructorAppArgs = WrongConstructorAppArgs

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

@@ -149,6 +149,17 @@ typeAsExpression = go
     goFunction :: Function -> FunctionExpression
     goFunction (Function l r) = FunctionExpression (go l) (go r)
 
+fillHolesFunctionDef :: HashMap Hole Type -> FunctionDef -> FunctionDef
+fillHolesFunctionDef m d =
+  FunctionDef
+    { _funDefName = d ^. funDefName,
+      _funDefType = fillHolesType m (d ^. funDefType),
+      _funDefClauses = fmap (fillHolesClause m) (d ^. funDefClauses)
+    }
+
+fillHolesClause :: HashMap Hole Type -> FunctionClause -> FunctionClause
+fillHolesClause m = over clauseBody (fillHoles m)
+
 fillHoles :: HashMap Hole Type -> Expression -> Expression
 fillHoles m = goe
   where

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -75,8 +75,9 @@ checkFunctionDef ::
   Members '[Reader InfoTable, Error TypeCheckerError] r =>
   FunctionDef ->
   Sem r FunctionDef
-checkFunctionDef FunctionDef {..} = do
+checkFunctionDef FunctionDef {..} = runInferenceDef $ do
   info <- lookupFunction _funDefName
+  checkFunctionDefType _funDefType
   _funDefClauses' <- mapM (checkFunctionClause info) _funDefClauses
   return
     FunctionDef
@@ -84,15 +85,34 @@ checkFunctionDef FunctionDef {..} = do
         ..
       }
 
+checkFunctionDefType :: forall r. Members '[Inference] r => Type -> Sem r ()
+checkFunctionDefType = go
+  where
+    go :: Type -> Sem r ()
+    go t = case t of
+      TypeHole h -> void (freshMetavar h)
+      TypeIden {} -> return ()
+      TypeApp a -> goApp a
+      TypeFunction f -> goFunction f
+      TypeAbs f -> goAbs f
+      TypeAny -> return ()
+      TypeUniverse -> return ()
+    goApp :: TypeApplication -> Sem r ()
+    goApp (TypeApplication a b) = go a >> go b
+    goFunction :: Function -> Sem r ()
+    goFunction (Function a b) = go a >> go b
+    goAbs :: TypeAbstraction -> Sem r ()
+    goAbs (TypeAbstraction _ b) = go b
+
 checkExpression ::
   Members '[Reader InfoTable, Error TypeCheckerError, Reader LocalVars, Inference] r =>
   Type ->
   Expression ->
   Sem r Expression
-checkExpression t e = do
+checkExpression expectedTy e = do
   e' <- inferExpression' e
   let inferredType = e' ^. typedType
-  unlessM (matchTypes t inferredType) (throw (err inferredType))
+  unlessM (matchTypes expectedTy inferredType) (throw (err inferredType))
   return (ExpressionTyped e')
   where
     err infTy =
@@ -100,7 +120,7 @@ checkExpression t e = do
         ( WrongType
             { _wrongTypeExpression = e,
               _wrongTypeInferredType = infTy,
-              _wrongTypeExpectedType = t
+              _wrongTypeExpectedType = expectedTy
             }
         )
 
@@ -141,16 +161,16 @@ constructorArgTypes i =
   )
 
 checkFunctionClauseBody ::
-  Members '[Reader InfoTable, Error TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, Inference] r =>
   LocalVars ->
   Type ->
   Expression ->
   Sem r Expression
 checkFunctionClauseBody locals expectedTy body =
-  runInference (runReader locals (checkExpression expectedTy body))
+  runReader locals (checkExpression expectedTy body)
 
 checkFunctionClause ::
-  Members '[Reader InfoTable, Error TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, Inference] r =>
   FunctionInfo ->
   FunctionClause ->
   Sem r FunctionClause

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

@@ -38,7 +38,7 @@ closeState = \case
       where
         goHole :: Hole -> MetavarState -> Sem r' Type
         goHole h = \case
-          Fresh -> throw @TypeCheckerError (error "unsolved meta")
+          Fresh -> throw (ErrUnsolvedMeta (UnsolvedMeta h))
           Refined t -> do
             s <- gets @(HashMap Hole Type) (^. at h)
             case s of
@@ -68,7 +68,7 @@ closeState = \case
 getMetavar :: Member (State InferenceState) r => Hole -> Sem r MetavarState
 getMetavar h = gets (fromJust . (^. inferenceMap . at h))
 
-re :: Member (Error TypeCheckerError) r => Sem (Inference ': r) Expression -> Sem (State InferenceState ': r) Expression
+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
@@ -85,21 +85,16 @@ re = reinterpret $ \case
             _typedType = TypeUniverse
           }
 
-    refineMetavar' ::
+    refineFreshMetavar ::
       Members '[Error TypeCheckerError, State InferenceState] r =>
       Hole ->
       Type ->
       Sem r ()
-    refineMetavar' h t = do
+    refineFreshMetavar h t = do
       s <- gets (fromJust . (^. inferenceMap . at h))
       case s of
         Fresh -> modify (over inferenceMap (HashMap.insert h (Refined t)))
-        Refined r -> goRefine r t
-
-    goRefine :: Members '[Error TypeCheckerError, State InferenceState] r => Type -> Type -> Sem r ()
-    goRefine r t = do
-      eq <- matchTypes' r t
-      unless eq (error "type error: cannot match types")
+        Refined {} -> impossible
 
     metavarType :: MetavarState -> Maybe Type
     metavarType = \case
@@ -136,7 +131,7 @@ re = reinterpret $ \case
             goHole h t = do
               r <- queryMetavar' h
               case r of
-                Nothing -> refineMetavar' h t $> True
+                Nothing -> refineFreshMetavar h t $> True
                 Just ht -> matchTypes' t ht
             goIden :: TypeIden -> TypeIden -> Sem r Bool
             goIden ia ib = case (ia, ib) of
@@ -158,3 +153,8 @@ runInference :: Member (Error TypeCheckerError) r => Sem (Inference ': r) Expres
 runInference a = do
   (subs, expr) <- runState iniState (re a) >>= firstM closeState
   return (fillHoles subs expr)
+
+runInferenceDef :: Member (Error TypeCheckerError) r => Sem (Inference ': r) FunctionDef -> Sem r FunctionDef
+runInferenceDef a = do
+  (subs, expr) <- runState iniState (re a) >>= firstM closeState
+  return (fillHolesFunctionDef subs expr)

test/TypeCheck/Negative.hs

@@ -77,6 +77,13 @@ tests =
       $ \case
         ErrTooManyPatterns {} -> Nothing
         _ -> wrongError,
+    NegTest
+      "Unsolved hole"
+      "MicroJuvix"
+      "UnsolvedMeta.mjuvix"
+      $ \case
+        ErrUnsolvedMeta {} -> Nothing
+        _ -> wrongError,
     NegTest
       "Multiple type errors are captured"
       "MicroJuvix"

test/TypeCheck/Positive.hs

@@ -67,6 +67,10 @@ tests =
       "Operators"
       "."
       "Operators.mjuvix",
+    PosTest
+      "Holes in type signature"
+      "MicroJuvix"
+      "HoleInSignature.mjuvix",
     PosTest
       "Polymorphism and higher rank functions"
       "."

tests/negative/MicroJuvix/UnsolvedMeta.mjuvix

@@ -0,0 +1,10 @@
+module UnsolvedMeta;
+
+inductive Proxy (A : Type) {
+  x : Proxy A;
+};
+
+t : Proxy _;
+t ≔ x _;
+
+end;

tests/positive/MicroJuvix/HoleInSignature.mjuvix

@@ -0,0 +1,17 @@
+module HoleInSignature;
+inductive Pair (A : Type) (B : Type) {
+  mkPair : A → B → Pair A B;
+};
+
+inductive Bool {
+  true : Bool;
+  false : Bool;
+};
+
+p : Pair _ _;
+p := mkPair _ _ true false;
+
+p2 : (A : Type) → (B : Type) → _ → B → Pair A _;
+p2 _ _ a b ≔ mkPair _ _ a b;
+
+end;

tests/positive/PolymorphismHoles.mjuvix

@@ -68,7 +68,7 @@ filter _ f nil ≔ nil _;
 filter _ f (cons x xs) ≔ ite _ (f x) (cons _ x (filter _ f xs)) (filter _ f xs);
 
 map : (A : Type) → (B : Type) →
-  (A → B) → List A → List B;
+  (A → B) → List _ → List _;
 map _ _ f nil ≔ nil _;
 map _ _ f (cons x xs) ≔ cons _ (f x) (map _ _ f xs);